Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal;
authorwenzelm
Wed, 13 Jul 2016 19:10:35 +0200
changeset 63478 37a3fc20154d
parent 63477 f5c81436b930
child 63479 464ef556bd21
clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal;
src/Tools/jEdit/src/text_structure.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:04:49 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:10:35 2016 +0200
@@ -141,7 +141,9 @@
                     keywords.is_before_command(tok) ||
                     keywords.is_command(tok, Keyword.theory)) 0
                 else if (keywords.is_command(tok, Keyword.PRF_SCRIPT == _))
-                  indent_structure + script_indent(range)
+                  (indent_structure + script_indent(range)) max indent_size
+                else if (keywords.is_command(tok, Keyword.proof))
+                  (indent_structure - indent_offset(tok)) max indent_size
                 else if (tok.is_command) indent_structure - indent_offset(tok)
                 else {
                   prev_line_command match {
isabelle