src/Tools/jEdit/src/jEdit.props
changeset 54318 1bdd8f541a06
parent 54306 2828f17fa41a
child 54365 5d45c985974a
equal deleted inserted replaced
54317:da932f511746 54318:1bdd8f541a06
     7 buffer.maxLineLen=100
     7 buffer.maxLineLen=100
     8 buffer.noTabs=true
     8 buffer.noTabs=true
     9 buffer.sidekick.keystroke-parse=false
     9 buffer.sidekick.keystroke-parse=false
    10 buffer.tabSize=2
    10 buffer.tabSize=2
    11 close-docking-area.shortcut2=C+e C+CIRCUMFLEX
    11 close-docking-area.shortcut2=C+e C+CIRCUMFLEX
       
    12 complete-word.shortcut=
    12 console.dock-position=floating
    13 console.dock-position=floating
    13 console.encoding=UTF-8
    14 console.encoding=UTF-8
    14 console.font=IsabelleText
    15 console.font=IsabelleText
    15 console.fontsize=14
    16 console.fontsize=14
    16 delete-line.shortcut=A+d
    17 delete-line.shortcut=A+d
   188 isabelle-output.height=174
   189 isabelle-output.height=174
   189 isabelle-output.width=412
   190 isabelle-output.width=412
   190 isabelle-sledgehammer.dock-position=bottom
   191 isabelle-sledgehammer.dock-position=bottom
   191 isabelle-symbols.dock-position=bottom
   192 isabelle-symbols.dock-position=bottom
   192 isabelle-theories.dock-position=right
   193 isabelle-theories.dock-position=right
   193 isabelle.complete.label=Complete text
   194 isabelle.complete.label=Complete Isabelle text
   194 isabelle.complete.shortcut=C+b
   195 isabelle.complete.shortcut2=C+b
   195 isabelle.control-bold.label=Control bold
   196 isabelle.control-bold.label=Control bold
   196 isabelle.control-bold.shortcut=C+e RIGHT
   197 isabelle.control-bold.shortcut=C+e RIGHT
   197 isabelle.control-reset.label=Control reset
   198 isabelle.control-reset.label=Control reset
   198 isabelle.control-reset.shortcut=C+e LEFT
   199 isabelle.control-reset.shortcut=C+e LEFT
   199 isabelle.control-sub.label=Control subscript
   200 isabelle.control-sub.label=Control subscript