src/Tools/jEdit/src/jEdit.props
changeset 69343 395c4fb15ea2
parent 68080 17f79ae49401
child 69643 83f15deb2d36
equal deleted inserted replaced
69342:fa981730b964 69343:395c4fb15ea2
    10 buffer.undoCount=1000
    10 buffer.undoCount=1000
    11 close-docking-area.shortcut2=C+e C+CIRCUMFLEX
    11 close-docking-area.shortcut2=C+e C+CIRCUMFLEX
    12 complete-word.shortcut=
    12 complete-word.shortcut=
    13 console.dock-position=floating
    13 console.dock-position=floating
    14 console.encoding=UTF-8
    14 console.encoding=UTF-8
    15 console.font=IsabelleText
    15 console.font=Isabelle DejaVu Sans Mono
    16 console.fontsize=14
    16 console.fontsize=14
    17 delete-line.shortcut=A+d
    17 delete-line.shortcut=A+d
    18 delete.shortcut2=C+d
    18 delete.shortcut2=C+d
    19 encoding.opt-out.Big5-HKSCS=true
    19 encoding.opt-out.Big5-HKSCS=true
    20 encoding.opt-out.Big5=true
    20 encoding.opt-out.Big5=true
   181 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
   181 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
   182 firstTime=false
   182 firstTime=false
   183 focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
   183 focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
   184 foldPainter=Circle
   184 foldPainter=Circle
   185 gatchan.highlight.overview=false
   185 gatchan.highlight.overview=false
       
   186 helpviewer.font=Isabelle DejaVu Serif
   186 home.shortcut=
   187 home.shortcut=
   187 insert-newline-indent.shortcut=
   188 insert-newline-indent.shortcut=
   188 insert-newline.shortcut=
   189 insert-newline.shortcut=
   189 isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
   190 isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
   190 isabelle-debugger.dock-position=floating
   191 isabelle-debugger.dock-position=floating
   249 line-end.shortcut=END
   250 line-end.shortcut=END
   250 line-home.shortcut=HOME
   251 line-home.shortcut=HOME
   251 logo.icon.medium=32x32/apps/isabelle.gif
   252 logo.icon.medium=32x32/apps/isabelle.gif
   252 lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
   253 lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
   253 match-bracket.shortcut2=C+9
   254 match-bracket.shortcut2=C+9
       
   255 metal.primary.font=Isabelle DejaVu Sans
       
   256 metal.secondary.font=Isabelle DejaVu Sans
   254 navigator.showOnToolbar=true
   257 navigator.showOnToolbar=true
   255 next-bracket.shortcut2=C+e C+9
   258 next-bracket.shortcut2=C+e C+9
   256 options.shortcuts.deletekeymap.label=Delete
   259 options.shortcuts.deletekeymap.label=Delete
   257 options.shortcuts.duplicatekeymap.dialog.title=Keymap name
   260 options.shortcuts.duplicatekeymap.dialog.title=Keymap name
   258 options.shortcuts.duplicatekeymap.label=Duplicate
   261 options.shortcuts.duplicatekeymap.label=Duplicate
   259 options.shortcuts.resetkeymap.dialog.title=Reset keymap
   262 options.shortcuts.resetkeymap.dialog.title=Reset keymap
   260 options.shortcuts.resetkeymap.label=Reset
   263 options.shortcuts.resetkeymap.label=Reset
   261 options.textarea.lineSpacing=-2
   264 options.textarea.lineSpacing=0
   262 plugin-blacklist.MacOSX.jar=true
   265 plugin-blacklist.MacOSX.jar=true
   263 plugin.MacOSXPlugin.altDispatcher=false
   266 plugin.MacOSXPlugin.altDispatcher=false
   264 plugin.MacOSXPlugin.disableOption=true
   267 plugin.MacOSXPlugin.disableOption=true
   265 prev-bracket.shortcut2=C+e C+8
   268 prev-bracket.shortcut2=C+e C+8
   266 print.font=IsabelleText
   269 print.font=Isabelle DejaVu Sans Mono
   267 print.glyphVector=true
   270 print.glyphVector=true
   268 recent-buffer.shortcut2=C+CIRCUMFLEX
   271 recent-buffer.shortcut2=C+CIRCUMFLEX
   269 restore.remote=false
   272 restore.remote=false
   270 restore=false
   273 restore=false
   271 search.subdirs.toggle=true
   274 search.subdirs.toggle=true
   298 view.blockCaret=true
   301 view.blockCaret=true
   299 view.caretBlink=false
   302 view.caretBlink=false
   300 view.docking.framework=PIDE
   303 view.docking.framework=PIDE
   301 view.eolMarkers=false
   304 view.eolMarkers=false
   302 view.extendedState=0
   305 view.extendedState=0
   303 view.font=IsabelleText
   306 view.font=Isabelle DejaVu Sans Mono
   304 view.fontsize=18
   307 view.fontsize=18
   305 view.fracFontMetrics=false
   308 view.fracFontMetrics=false
       
   309 view.gutter.font=Isabelle DejaVu Sans Mono
   306 view.gutter.fontsize=12
   310 view.gutter.fontsize=12
   307 view.gutter.lineNumbers=false
   311 view.gutter.lineNumbers=false
   308 view.gutter.selectionAreaWidth=18
   312 view.gutter.selectionAreaWidth=18
   309 view.height=787
   313 view.height=787
   310 view.middleMousePaste=true
   314 view.middleMousePaste=true