src/Tools/jEdit/dist-template/properties/jedit.props
changeset 34556 09a5984250a2
parent 34512 14d70378f1c7
child 34613 71fb6ab6ec57
equal deleted inserted replaced
34555:7c001369956a 34556:09a5984250a2
    23 view.gutter.fontsize=12
    23 view.gutter.fontsize=12
    24 view.middleMousePaste=true
    24 view.middleMousePaste=true
    25 view.showToolbar=false
    25 view.showToolbar=false
    26 buffer.sidekick.keystroke-parse=true
    26 buffer.sidekick.keystroke-parse=true
    27 sidekick.buffer-save-parse=true
    27 sidekick.buffer-save-parse=true
       
    28 mode.isabelle.sidekick.showStatusWindow.label=true
    28 sidekick-tree.dock-position=right
    29 sidekick-tree.dock-position=right
    29 isabelle-state.dock-position=bottom
    30 isabelle-state.dock-position=bottom