equal
deleted
inserted
replaced
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 sidekick.complete-delay=300 |
28 mode.isabelle.sidekick.showStatusWindow.label=true |
29 mode.isabelle.sidekick.showStatusWindow.label=true |
29 sidekick-tree.dock-position=right |
30 sidekick-tree.dock-position=right |
30 isabelle-state.dock-position=bottom |
31 isabelle-state.dock-position=bottom |