User Tools
jedit
Differences
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] (current) 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 | ||
jedit.1396442347.txt.gz ยท Last modified: 2014/04/02 14:39 by peter
Page Tools
