src/Pure/Isar/outer_syntax.scala
changeset 58700 4717d18cc619
parent 58697 5bc1d6c4a499
child 58703 883efcc7a50d
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 11:19:34 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 20:56:16 2014 +0200
     1.3 @@ -43,10 +43,15 @@
     1.4  
     1.5    object Line_Structure
     1.6    {
     1.7 -    val init = Line_Structure(0, 0)
     1.8 +    val init = Line_Structure()
     1.9    }
    1.10  
    1.11 -  sealed case class Line_Structure(depth_before: Int, depth: Int)
    1.12 +  sealed case class Line_Structure(
    1.13 +    improper: Boolean = true,
    1.14 +    command: Boolean = false,
    1.15 +    depth: Int = 0,
    1.16 +    span_depth: Int = 0,
    1.17 +    after_span_depth: Int = 0)
    1.18  }
    1.19  
    1.20  final class Outer_Syntax private(
    1.21 @@ -150,21 +155,29 @@
    1.22  
    1.23    /* line-oriented structure */
    1.24  
    1.25 -  def line_structure(tokens: List[Token], depth: Int): Outer_Syntax.Line_Structure =
    1.26 +  def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure)
    1.27 +    : Outer_Syntax.Line_Structure =
    1.28    {
    1.29 +    val improper1 = tokens.forall(_.is_improper)
    1.30 +    val command1 = tokens.exists(_.is_command)
    1.31 +
    1.32      val depth1 =
    1.33        if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
    1.34 -      else depth
    1.35 -    val depth2 =
    1.36 -      (depth /: tokens) { case (d, tok) =>
    1.37 -        if (command_kind(tok, Keyword.theory_goal)) 1
    1.38 -        else if (command_kind(tok, Keyword.theory)) 0
    1.39 -        else if (command_kind(tok, Keyword.proof_goal)) d + 1
    1.40 -        else if (command_kind(tok, Keyword.qed)) d - 1
    1.41 -        else if (command_kind(tok, Keyword.qed_global)) 0
    1.42 -        else d
    1.43 +      else if (command1) struct.after_span_depth
    1.44 +      else struct.span_depth
    1.45 +
    1.46 +    val (span_depth1, after_span_depth1) =
    1.47 +      ((struct.span_depth, struct.after_span_depth) /: tokens) {
    1.48 +        case ((d0, d), tok) =>
    1.49 +          if (command_kind(tok, Keyword.theory_goal)) (2, 1)
    1.50 +          else if (command_kind(tok, Keyword.theory)) (1, 0)
    1.51 +          else if (command_kind(tok, Keyword.proof_goal)) (d + 2, d + 1)
    1.52 +          else if (command_kind(tok, Keyword.qed)) (d + 1, d - 1)
    1.53 +          else if (command_kind(tok, Keyword.qed_global)) (1, 0)
    1.54 +          else (d0, d)
    1.55        }
    1.56 -    Outer_Syntax.Line_Structure(depth1, depth2)
    1.57 +
    1.58 +    Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
    1.59    }
    1.60  
    1.61  
    1.62 @@ -197,7 +210,7 @@
    1.63        }
    1.64      }
    1.65      val tokens = toks.toList
    1.66 -    (tokens, ctxt, line_structure(tokens, structure.depth))
    1.67 +    (tokens, ctxt, line_structure(tokens, structure))
    1.68    }
    1.69  
    1.70