equal
deleted
inserted
replaced
301 vfs.favorite.3=$JEDIT_SETTINGS |
301 vfs.favorite.3=$JEDIT_SETTINGS |
302 vfs.favorite.4.type=1 |
302 vfs.favorite.4.type=1 |
303 vfs.favorite.4=isabelle-export: |
303 vfs.favorite.4=isabelle-export: |
304 vfs.favorite.5.type=1 |
304 vfs.favorite.5.type=1 |
305 vfs.favorite.5=isabelle-session: |
305 vfs.favorite.5=isabelle-session: |
306 view.antiAlias=standard |
306 view.antiAlias=subpixel HRGB |
307 view.blockCaret=true |
307 view.blockCaret=true |
308 view.caretBlink=false |
308 view.caretBlink=false |
309 view.docking.framework=PIDE |
309 view.docking.framework=PIDE |
310 view.eolMarkers=false |
310 view.eolMarkers=false |
311 view.extendedState=0 |
311 view.extendedState=0 |