src/Tools/jEdit/src/jEdit.props
changeset 69343 395c4fb15ea2
parent 68080 17f79ae49401
child 69643 83f15deb2d36
--- a/src/Tools/jEdit/src/jEdit.props	Sat Nov 24 16:41:18 2018 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sat Nov 24 18:56:44 2018 +0100
@@ -12,7 +12,7 @@
 complete-word.shortcut=
 console.dock-position=floating
 console.encoding=UTF-8
-console.font=IsabelleText
+console.font=Isabelle DejaVu Sans Mono
 console.fontsize=14
 delete-line.shortcut=A+d
 delete.shortcut2=C+d
@@ -183,6 +183,7 @@
 focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
 foldPainter=Circle
 gatchan.highlight.overview=false
+helpviewer.font=Isabelle DejaVu Serif
 home.shortcut=
 insert-newline-indent.shortcut=
 insert-newline.shortcut=
@@ -251,6 +252,8 @@
 logo.icon.medium=32x32/apps/isabelle.gif
 lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
 match-bracket.shortcut2=C+9
+metal.primary.font=Isabelle DejaVu Sans
+metal.secondary.font=Isabelle DejaVu Sans
 navigator.showOnToolbar=true
 next-bracket.shortcut2=C+e C+9
 options.shortcuts.deletekeymap.label=Delete
@@ -258,12 +261,12 @@
 options.shortcuts.duplicatekeymap.label=Duplicate
 options.shortcuts.resetkeymap.dialog.title=Reset keymap
 options.shortcuts.resetkeymap.label=Reset
-options.textarea.lineSpacing=-2
+options.textarea.lineSpacing=0
 plugin-blacklist.MacOSX.jar=true
 plugin.MacOSXPlugin.altDispatcher=false
 plugin.MacOSXPlugin.disableOption=true
 prev-bracket.shortcut2=C+e C+8
-print.font=IsabelleText
+print.font=Isabelle DejaVu Sans Mono
 print.glyphVector=true
 recent-buffer.shortcut2=C+CIRCUMFLEX
 restore.remote=false
@@ -300,9 +303,10 @@
 view.docking.framework=PIDE
 view.eolMarkers=false
 view.extendedState=0
-view.font=IsabelleText
+view.font=Isabelle DejaVu Sans Mono
 view.fontsize=18
 view.fracFontMetrics=false
+view.gutter.font=Isabelle DejaVu Sans Mono
 view.gutter.fontsize=12
 view.gutter.lineNumbers=false
 view.gutter.selectionAreaWidth=18