src/Pure/Isar/outer_syntax.scala
changeset 58696 6b7445774ce3
parent 58695 91839729224e
child 58697 5bc1d6c4a499
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 12:24:19 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 21:24:42 2014 +0200
     1.3 @@ -37,6 +37,16 @@
     1.4    val empty: Outer_Syntax = new Outer_Syntax()
     1.5  
     1.6    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     1.7 +
     1.8 +
     1.9 +  /* line nesting */
    1.10 +
    1.11 +  object Line_Nesting
    1.12 +  {
    1.13 +    val init = Line_Nesting(0, 0)
    1.14 +  }
    1.15 +
    1.16 +  sealed case class Line_Nesting(depth_before: Int, depth: Int)
    1.17  }
    1.18  
    1.19  final class Outer_Syntax private(
    1.20 @@ -66,6 +76,10 @@
    1.21        case None => false
    1.22      }
    1.23  
    1.24 +  def command_kind(token: Token, pred: String => Boolean): Boolean =
    1.25 +    token.is_command && is_command(token.source) &&
    1.26 +      pred(keyword_kind(token.source).get)
    1.27 +
    1.28  
    1.29    /* load commands */
    1.30  
    1.31 @@ -134,6 +148,26 @@
    1.32      heading_level(command.name)
    1.33  
    1.34  
    1.35 +  /* line nesting */
    1.36 +
    1.37 +  def line_nesting(tokens: List[Token], depth: Int): Outer_Syntax.Line_Nesting =
    1.38 +  {
    1.39 +    val depth1 =
    1.40 +      if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
    1.41 +      else depth
    1.42 +    val depth2 =
    1.43 +      (depth /: tokens) { case (d, tok) =>
    1.44 +        if (command_kind(tok, Keyword.theory_goal)) 1
    1.45 +        else if (command_kind(tok, Keyword.theory)) 0
    1.46 +        else if (command_kind(tok, Keyword.proof_goal)) d + 1
    1.47 +        else if (command_kind(tok, Keyword.qed)) d - 1
    1.48 +        else if (command_kind(tok, Keyword.qed_global)) 0
    1.49 +        else d
    1.50 +      }
    1.51 +    Outer_Syntax.Line_Nesting(depth1, depth2)
    1.52 +  }
    1.53 +
    1.54 +
    1.55    /* token language */
    1.56  
    1.57    def scan(input: CharSequence): List[Token] =
    1.58 @@ -146,8 +180,8 @@
    1.59      }
    1.60    }
    1.61  
    1.62 -  def scan_line(input: CharSequence, context: Scan.Line_Context, depth: Int)
    1.63 -    : (List[Token], Scan.Line_Context, Int) =
    1.64 +  def scan_line(input: CharSequence, context: Scan.Line_Context, nesting: Outer_Syntax.Line_Nesting)
    1.65 +    : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Nesting) =
    1.66    {
    1.67      var in: Reader[Char] = new CharSequenceReader(input)
    1.68      val toks = new mutable.ListBuffer[Token]
    1.69 @@ -159,9 +193,8 @@
    1.70            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.71        }
    1.72      }
    1.73 -
    1.74 -    val depth1 = depth // FIXME
    1.75 -    (toks.toList, ctxt, depth1)
    1.76 +    val tokens = toks.toList
    1.77 +    (tokens, ctxt, line_nesting(tokens, nesting.depth))
    1.78    }
    1.79  
    1.80