src/Tools/jEdit/dist-template/properties/jedit.props
author wenzelm
Fri, 26 Jun 2009 18:24:03 +0200
changeset 34623 a356a8ee6f00
parent 34619 e89b6ec97910
child 34626 7124433be8be
permissions -rw-r--r--
renamed UTF-8-isabelle to UTF-8-Isabelle;

#jEdit properties
buffer.deepIndent=false
buffer.encoding=UTF-8-Isabelle
buffer.indentSize=2
buffer.lineSeparator=\n
buffer.maxLineLen=100
buffer.noTabs=true
buffer.tabSize=2
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
tip.show=false
encodingDetectors=BOM XML-PI buffer-local-property
delete-line.shortcut=A+d
delete.shortcut2=C+d
view.antiAlias=standard
view.blockCaret=true
view.caretBlink=false
view.eolMarkers=false
view.extendedState=0
view.font=Lucida Sans Typewriter
view.fontsize=18
view.fracFontMetrics=true
view.gutter.fontsize=12
view.middleMousePaste=true
view.showToolbar=false
buffer.sidekick.keystroke-parse=true
sidekick.buffer-save-parse=true
sidekick.complete-delay=300
mode.isabelle.sidekick.showStatusWindow.label=true
sidekick-tree.dock-position=right
isabelle-state.dock-position=bottom