# HG changeset patch
# User wenzelm
# Date 1468432856 -7200
# Node ID cf2d332acb7c6c28fe636d175f37505de6a465de
# Parent  cbc71faf7673a36c2a6c473841be4f5e980a484c
clarified indentation (amending 37a3fc20154d);

diff -r cbc71faf7673 -r cf2d332acb7c src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:57:30 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 20:00:56 2016 +0200
@@ -141,6 +141,8 @@
                 if (tok.is_begin ||
                     keywords.is_before_command(tok) ||
                     keywords.is_command(tok, Keyword.theory)) 0
+                else if (keywords.is_command(tok, Keyword.proof_enclose))
+                  indent_structure + script_indent(info) - indent_offset(tok)
                 else if (keywords.is_command(tok, Keyword.proof))
                   (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
                 else if (tok.is_command) indent_structure - indent_offset(tok)