src/Pure/Isar/outer_syntax.scala
changeset 58703 883efcc7a50d
parent 58700 4717d18cc619
child 58706 70a947611792
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 22:02:10 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 22:41:36 2014 +0200
     1.3 @@ -168,13 +168,16 @@
     1.4  
     1.5      val (span_depth1, after_span_depth1) =
     1.6        ((struct.span_depth, struct.after_span_depth) /: tokens) {
     1.7 -        case ((d0, d), tok) =>
     1.8 -          if (command_kind(tok, Keyword.theory_goal)) (2, 1)
     1.9 -          else if (command_kind(tok, Keyword.theory)) (1, 0)
    1.10 -          else if (command_kind(tok, Keyword.proof_goal)) (d + 2, d + 1)
    1.11 -          else if (command_kind(tok, Keyword.qed)) (d + 1, d - 1)
    1.12 -          else if (command_kind(tok, Keyword.qed_global)) (1, 0)
    1.13 -          else (d0, d)
    1.14 +        case ((x, y), tok) =>
    1.15 +          if (tok.is_command) {
    1.16 +            if (command_kind(tok, Keyword.theory_goal)) (2, 1)
    1.17 +            else if (command_kind(tok, Keyword.theory)) (1, 0)
    1.18 +            else if (command_kind(tok, Keyword.proof_goal) || tok.source == "{") (y + 2, y + 1)
    1.19 +            else if (command_kind(tok, Keyword.qed) || tok.source == "}") (y + 1, y - 1)
    1.20 +            else if (command_kind(tok, Keyword.qed_global)) (1, 0)
    1.21 +            else (x, y)
    1.22 +          }
    1.23 +          else (x, y)
    1.24        }
    1.25  
    1.26      Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)