changeset 63455 | 019856db2bb6 |
parent 63347 | e344dc82f6c2 |
child 63474 | f66e3c3b0fb1 |
--- a/src/Tools/jEdit/etc/options Tue Jul 12 11:12:07 2016 +0200 +++ b/src/Tools/jEdit/etc/options Tue Jul 12 11:51:05 2016 +0200 @@ -40,6 +40,12 @@ -- "default threshold for timing display (seconds)" +section "Indentation" + +public option jedit_indent_newline : bool = true + -- "indentation of Isabelle keywords on ENTER (action isabelle.newline)" + + section "Completion" public option jedit_completion : bool = true