# HG changeset patch
# User wenzelm
# Date 1413664896 -7200
# Node ID 883efcc7a50d34e06e19045e93438e28e85bc575
# Parent  39866de9d9884e448b269ce9ff74c39a8f4a68d7
more folds;

diff -r 39866de9d988 -r 883efcc7a50d src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 22:02:10 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 22:41:36 2014 +0200
@@ -168,13 +168,16 @@
 
     val (span_depth1, after_span_depth1) =
       ((struct.span_depth, struct.after_span_depth) /: tokens) {
-        case ((d0, d), tok) =>
-          if (command_kind(tok, Keyword.theory_goal)) (2, 1)
-          else if (command_kind(tok, Keyword.theory)) (1, 0)
-          else if (command_kind(tok, Keyword.proof_goal)) (d + 2, d + 1)
-          else if (command_kind(tok, Keyword.qed)) (d + 1, d - 1)
-          else if (command_kind(tok, Keyword.qed_global)) (1, 0)
-          else (d0, d)
+        case ((x, y), tok) =>
+          if (tok.is_command) {
+            if (command_kind(tok, Keyword.theory_goal)) (2, 1)
+            else if (command_kind(tok, Keyword.theory)) (1, 0)
+            else if (command_kind(tok, Keyword.proof_goal) || tok.source == "{") (y + 2, y + 1)
+            else if (command_kind(tok, Keyword.qed) || tok.source == "}") (y + 1, y - 1)
+            else if (command_kind(tok, Keyword.qed_global)) (1, 0)
+            else (x, y)
+          }
+          else (x, y)
       }
 
     Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)