We are looking for some clarification on this question. Follow up questions: 

• Are users interested in choosing a font different than the default in PilotScript / Python / etc?
• What different fonts do you want to see?
• Are you interested in mixing fonts / fonts size within a single script? 
• Anything else we are missing on this topic?
• Somewhat related: will color coding syntax be useful? 
• Do you have suggestions for color coding schemes from other IDEs?

Thank you!

Ton van Daelen