support line context with depth;
authorwenzelm
Thu Oct 16 12:09:57 2014 +0200 (2014-10-16)
changeset 58694983e98da2a42
parent 58693 4c9aa5f7bfa0
child 58695 91839729224e
support line context with depth;
basic setup for "isabelle" fold handling;
misc tuning;
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/fold_handling.scala
src/Tools/jEdit/src/services.xml
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 10:59:43 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 12:09:57 2014 +0200
     1.3 @@ -134,7 +134,8 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
     1.8 +  def scan_line(input: CharSequence, context: Scan.Line_Context, depth: Int)
     1.9 +    : (List[Token], Scan.Line_Context, Int) =
    1.10    {
    1.11      var in: Reader[Char] = new CharSequenceReader(input)
    1.12      val toks = new mutable.ListBuffer[Token]
    1.13 @@ -146,7 +147,9 @@
    1.14            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.15        }
    1.16      }
    1.17 -    (toks.toList, ctxt)
    1.18 +
    1.19 +    val depth1 = depth // FIXME
    1.20 +    (toks.toList, ctxt, depth1)
    1.21    }
    1.22  
    1.23  
     2.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Oct 16 10:59:43 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Oct 16 12:09:57 2014 +0200
     2.3 @@ -154,7 +154,7 @@
     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)
     2.8 +    extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context, 0)
     2.9  
    2.10  
    2.11    /* token marker */
     3.1 --- a/src/Tools/jEdit/src/fold_handling.scala	Thu Oct 16 10:59:43 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/fold_handling.scala	Thu Oct 16 12:09:57 2014 +0200
     3.3 @@ -16,6 +16,23 @@
     3.4  
     3.5  object Fold_Handling
     3.6  {
     3.7 +  /* input: dynamic line context  */
     3.8 +
     3.9 +  class Fold_Handler extends FoldHandler("isabelle")
    3.10 +  {
    3.11 +    override def equals(other: Any): Boolean =
    3.12 +      other match {
    3.13 +        case that: Fold_Handler => true
    3.14 +        case _ => false
    3.15 +      }
    3.16 +
    3.17 +    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
    3.18 +      Token_Markup.buffer_line_depth(buffer, line)
    3.19 +  }
    3.20 +
    3.21 +
    3.22 +  /* output: static document rendering */
    3.23 +
    3.24    class Document_Fold_Handler(private val rendering: Rendering)
    3.25      extends FoldHandler("isabelle-document")
    3.26    {
     4.1 --- a/src/Tools/jEdit/src/services.xml	Thu Oct 16 10:59:43 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/services.xml	Thu Oct 16 12:09:57 2014 +0200
     4.3 @@ -2,12 +2,15 @@
     4.4  <!DOCTYPE SERVICES SYSTEM "services.dtd">
     4.5  
     4.6  <SERVICES>
     4.7 +  <SERVICE CLASS="org.gjt.sp.jedit.buffer.FoldHandler" NAME="isabelle">
     4.8 +    new isabelle.jedit.Fold_Handling.Fold_Handler();
     4.9 +  </SERVICE>
    4.10    <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
    4.11      new isabelle.jedit.Context_Menu();
    4.12    </SERVICE>
    4.13 -	<SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
    4.14 -		new isabelle.jedit.PIDE_Docking_Framework();
    4.15 -	</SERVICE>
    4.16 +  <SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
    4.17 +    new isabelle.jedit.PIDE_Docking_Framework();
    4.18 +  </SERVICE>
    4.19    <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
    4.20      new isabelle.jedit.Isabelle_Encoding();
    4.21    </SERVICE>
     5.1 --- a/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 10:59:43 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 12:09:57 2014 +0200
     5.3 @@ -175,13 +175,17 @@
     5.4  
     5.5    /* line context */
     5.6  
     5.7 -  class Generic_Line_Context[C](rules: ParserRuleSet, val context: Option[C])
     5.8 +  class Generic_Line_Context[C](
     5.9 +      rules: ParserRuleSet,
    5.10 +      val context: Option[C],
    5.11 +      val depth: Int)
    5.12      extends TokenMarker.LineContext(rules, null)
    5.13    {
    5.14 -    override def hashCode: Int = context.hashCode
    5.15 +    override def hashCode: Int = (context, depth).hashCode
    5.16      override def equals(that: Any): Boolean =
    5.17        that match {
    5.18 -        case other: Generic_Line_Context[_] => context == other.context
    5.19 +        case other: Generic_Line_Context[_] =>
    5.20 +          context == other.context && depth == other.depth
    5.21          case _ => false
    5.22        }
    5.23    }
    5.24 @@ -190,58 +194,53 @@
    5.25      Untyped.get(buffer, "lineMgr") match {
    5.26        case line_mgr: LineManager =>
    5.27          line_mgr.getLineContext(line) match {
    5.28 -          case ctxt: Generic_Line_Context[C] => Some(ctxt)
    5.29 +          case c: Generic_Line_Context[C] => Some(c)
    5.30            case _ => None
    5.31          }
    5.32        case _ => None
    5.33      }
    5.34  
    5.35 +  def buffer_line_depth(buffer: JEditBuffer, line: Int): Int =
    5.36 +    buffer_line_context(buffer, line) match { case Some(c) => c.depth case None => 0 }
    5.37 +
    5.38 +
    5.39 +  /* token marker */
    5.40  
    5.41    private val context_rules = new ParserRuleSet("isabelle", "MAIN")
    5.42  
    5.43 -  private class Line_Context(context: Option[Scan.Line_Context])
    5.44 -    extends Generic_Line_Context[Scan.Line_Context](context_rules, context)
    5.45 -
    5.46 -
    5.47 -  /* token marker */
    5.48 +  private class Line_Context(context: Option[Scan.Line_Context], depth: Int)
    5.49 +    extends Generic_Line_Context[Scan.Line_Context](context_rules, context, depth)
    5.50  
    5.51    class Marker(mode: String) extends TokenMarker
    5.52    {
    5.53      override def markTokens(context: TokenMarker.LineContext,
    5.54          handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
    5.55      {
    5.56 -      val line_ctxt =
    5.57 +      val (opt_ctxt, depth) =
    5.58          context match {
    5.59 -          case c: Line_Context => c.context
    5.60 -          case _ => Some(Scan.Finished)
    5.61 +          case c: Line_Context => (c.context, c.depth)
    5.62 +          case _ => (Some(Scan.Finished), 0)
    5.63          }
    5.64        val line = if (raw_line == null) new Segment else raw_line
    5.65  
    5.66        val context1 =
    5.67        {
    5.68 -        def no_context =
    5.69 -        {
    5.70 -          val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
    5.71 -          (List(styled_token), new Line_Context(None))
    5.72 -        }
    5.73          val (styled_tokens, context1) =
    5.74 -          if (mode == "isabelle-ml" || mode == "sml") {
    5.75 -            if (line_ctxt.isDefined) {
    5.76 -              val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get)
    5.77 +          (opt_ctxt, Isabelle.mode_syntax(mode)) match {
    5.78 +            case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
    5.79 +              val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
    5.80                val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
    5.81 -              (styled_tokens, new Line_Context(Some(ctxt1)))
    5.82 -            }
    5.83 -            else no_context
    5.84 -          }
    5.85 -          else {
    5.86 -            Isabelle.mode_syntax(mode) match {
    5.87 -              case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
    5.88 -                val (tokens, ctxt1) = syntax.scan_line(line, line_ctxt.get)
    5.89 -                val styled_tokens =
    5.90 -                  tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
    5.91 -                (styled_tokens, new Line_Context(Some(ctxt1)))
    5.92 -              case _ => no_context
    5.93 -            }
    5.94 +              (styled_tokens, new Line_Context(Some(ctxt1), depth))
    5.95 +
    5.96 +            case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
    5.97 +              val (tokens, ctxt1, depth1) = syntax.scan_line(line, ctxt, depth)
    5.98 +              val styled_tokens =
    5.99 +                tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
   5.100 +              (styled_tokens, new Line_Context(Some(ctxt1), depth1))
   5.101 +
   5.102 +            case _ =>
   5.103 +              val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
   5.104 +              (List(styled_token), new Line_Context(None, 0))
   5.105            }
   5.106  
   5.107          val extended = extended_styles(line)
   5.108 @@ -267,6 +266,7 @@
   5.109          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   5.110          context1
   5.111        }
   5.112 +
   5.113        val context2 = context1.intern
   5.114        handler.setLineContext(context2)
   5.115        context2