src/Tools/jEdit/etc/options
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