more explicit Line_Nesting;
authorwenzelm
Thu Oct 16 21:24:42 2014 +0200 (2014-10-16)
changeset 586966b7445774ce3
parent 58695 91839729224e
child 58697 5bc1d6c4a499
more explicit Line_Nesting;
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/fold_handling.scala
src/Tools/jEdit/src/token_markup.scala
     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  
     2.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Oct 16 12:24:19 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Oct 16 21:24:42 2014 +0200
     2.3 @@ -154,7 +154,8 @@
     2.4    private val context_rules = new ParserRuleSet("bibtex", "MAIN")
     2.5  
     2.6    private class Line_Context(context: Option[Bibtex.Line_Context])
     2.7 -    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context, 0)
     2.8 +    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](
     2.9 +      context_rules, context, Outer_Syntax.Line_Nesting.init)
    2.10  
    2.11  
    2.12    /* token marker */
     3.1 --- a/src/Tools/jEdit/src/fold_handling.scala	Thu Oct 16 12:24:19 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/fold_handling.scala	Thu Oct 16 21:24:42 2014 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4        }
     3.5  
     3.6      override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
     3.7 -      Token_Markup.buffer_line_depth(buffer, line)
     3.8 +      Token_Markup.buffer_line_nesting(buffer, line).depth_before
     3.9    }
    3.10  
    3.11  
     4.1 --- a/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 12:24:19 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 21:24:42 2014 +0200
     4.3 @@ -178,14 +178,14 @@
     4.4    class Generic_Line_Context[C](
     4.5        rules: ParserRuleSet,
     4.6        val context: Option[C],
     4.7 -      val depth: Int)
     4.8 +      val nesting: Outer_Syntax.Line_Nesting)
     4.9      extends TokenMarker.LineContext(rules, null)
    4.10    {
    4.11 -    override def hashCode: Int = (context, depth).hashCode
    4.12 +    override def hashCode: Int = (context, nesting).hashCode
    4.13      override def equals(that: Any): Boolean =
    4.14        that match {
    4.15          case other: Generic_Line_Context[_] =>
    4.16 -          context == other.context && depth == other.depth
    4.17 +          context == other.context && nesting == other.nesting
    4.18          case _ => false
    4.19        }
    4.20    }
    4.21 @@ -200,26 +200,29 @@
    4.22        case _ => None
    4.23      }
    4.24  
    4.25 -  def buffer_line_depth(buffer: JEditBuffer, line: Int): Int =
    4.26 -    buffer_line_context(buffer, line) match { case Some(c) => c.depth case None => 0 }
    4.27 +  def buffer_line_nesting(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Nesting =
    4.28 +    buffer_line_context(buffer, line) match {
    4.29 +      case Some(c) => c.nesting
    4.30 +      case None => Outer_Syntax.Line_Nesting.init
    4.31 +    }
    4.32  
    4.33  
    4.34    /* token marker */
    4.35  
    4.36    private val context_rules = new ParserRuleSet("isabelle", "MAIN")
    4.37  
    4.38 -  private class Line_Context(context: Option[Scan.Line_Context], depth: Int)
    4.39 -    extends Generic_Line_Context[Scan.Line_Context](context_rules, context, depth)
    4.40 +  private class Line_Context(context: Option[Scan.Line_Context], nesting: Outer_Syntax.Line_Nesting)
    4.41 +    extends Generic_Line_Context[Scan.Line_Context](context_rules, context, nesting)
    4.42  
    4.43    class Marker(mode: String) extends TokenMarker
    4.44    {
    4.45      override def markTokens(context: TokenMarker.LineContext,
    4.46          handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
    4.47      {
    4.48 -      val (opt_ctxt, depth) =
    4.49 +      val (opt_ctxt, nesting) =
    4.50          context match {
    4.51 -          case c: Line_Context => (c.context, c.depth)
    4.52 -          case _ => (Some(Scan.Finished), 0)
    4.53 +          case c: Line_Context => (c.context, c.nesting)
    4.54 +          case _ => (Some(Scan.Finished), Outer_Syntax.Line_Nesting.init)
    4.55          }
    4.56        val line = if (raw_line == null) new Segment else raw_line
    4.57  
    4.58 @@ -230,17 +233,17 @@
    4.59              case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
    4.60                val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
    4.61                val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
    4.62 -              (styled_tokens, new Line_Context(Some(ctxt1), depth))
    4.63 +              (styled_tokens, new Line_Context(Some(ctxt1), nesting))
    4.64  
    4.65              case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
    4.66 -              val (tokens, ctxt1, depth1) = syntax.scan_line(line, ctxt, depth)
    4.67 +              val (tokens, ctxt1, nesting1) = syntax.scan_line(line, ctxt, nesting)
    4.68                val styled_tokens =
    4.69                  tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
    4.70 -              (styled_tokens, new Line_Context(Some(ctxt1), depth1))
    4.71 +              (styled_tokens, new Line_Context(Some(ctxt1), nesting1))
    4.72  
    4.73              case _ =>
    4.74                val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
    4.75 -              (List(styled_token), new Line_Context(None, 0))
    4.76 +              (List(styled_token), new Line_Context(None, nesting))
    4.77            }
    4.78  
    4.79          val extended = extended_styles(line)