# HG changeset patch
# User wenzelm
# Date 1468429835 -7200
# Node ID 37a3fc20154d5ae17664241c2be41e8668298167
# Parent  f5c81436b93020ce708faa2f11b88a5cee9bdc86
clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal;

diff -r f5c81436b930 -r 37a3fc20154d src/Tools/jEdit/src/text_structure.scala
--- 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 {