This shows you the differences between two versions of the page.
jedit [2014/04/02 14:39] peter created |
jedit [2014/04/02 14:43] peter |
||
---|---|---|---|
Line 3: | Line 3: | ||
* Enable brackets mode: Start isabelle with "isabelle jedit -m brackets" | * Enable brackets mode: Start isabelle with "isabelle jedit -m brackets" | ||
* Change the font size: Utilities -> Global Options -> jEdit -> Text Area -> Text font | * Change the font size: Utilities -> Global Options -> jEdit -> Text Area -> Text font | ||
+ | * Change Look&Feel: Utilities -> Global Options -> jEdit -> Appearance |