# HG changeset patch # User wenzelm # Date 1413454197 -7200 # Node ID 983e98da2a42a13b669b8ab5c6d7f9416287cbd8 # Parent 4c9aa5f7bfa0fadd2ce104c38069119d2a08d391 support line context with depth; basic setup for "isabelle" fold handling; misc tuning; diff -r 4c9aa5f7bfa0 -r 983e98da2a42 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Thu Oct 16 10:59:43 2014 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Thu Oct 16 12:09:57 2014 +0200 @@ -134,7 +134,8 @@ } } - def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) = + def scan_line(input: CharSequence, context: Scan.Line_Context, depth: Int) + : (List[Token], Scan.Line_Context, Int) = { var in: Reader[Char] = new CharSequenceReader(input) val toks = new mutable.ListBuffer[Token] @@ -146,7 +147,9 @@ error("Unexpected failure of tokenizing input:\n" + rest.source.toString) } } - (toks.toList, ctxt) + + val depth1 = depth // FIXME + (toks.toList, ctxt, depth1) } diff -r 4c9aa5f7bfa0 -r 983e98da2a42 src/Tools/jEdit/src/bibtex_jedit.scala --- a/src/Tools/jEdit/src/bibtex_jedit.scala Thu Oct 16 10:59:43 2014 +0200 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala Thu Oct 16 12:09:57 2014 +0200 @@ -154,7 +154,7 @@ private val context_rules = new ParserRuleSet("bibtex", "MAIN") private class Line_Context(context: Option[Bibtex.Line_Context]) - extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context) + extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context, 0) /* token marker */ diff -r 4c9aa5f7bfa0 -r 983e98da2a42 src/Tools/jEdit/src/fold_handling.scala --- a/src/Tools/jEdit/src/fold_handling.scala Thu Oct 16 10:59:43 2014 +0200 +++ b/src/Tools/jEdit/src/fold_handling.scala Thu Oct 16 12:09:57 2014 +0200 @@ -16,6 +16,23 @@ object Fold_Handling { + /* input: dynamic line context */ + + class Fold_Handler extends FoldHandler("isabelle") + { + override def equals(other: Any): Boolean = + other match { + case that: Fold_Handler => true + case _ => false + } + + override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = + Token_Markup.buffer_line_depth(buffer, line) + } + + + /* output: static document rendering */ + class Document_Fold_Handler(private val rendering: Rendering) extends FoldHandler("isabelle-document") { diff -r 4c9aa5f7bfa0 -r 983e98da2a42 src/Tools/jEdit/src/services.xml --- a/src/Tools/jEdit/src/services.xml Thu Oct 16 10:59:43 2014 +0200 +++ b/src/Tools/jEdit/src/services.xml Thu Oct 16 12:09:57 2014 +0200 @@ -2,12 +2,15 @@ + + new isabelle.jedit.Fold_Handling.Fold_Handler(); + new isabelle.jedit.Context_Menu(); - - new isabelle.jedit.PIDE_Docking_Framework(); - + + new isabelle.jedit.PIDE_Docking_Framework(); + new isabelle.jedit.Isabelle_Encoding(); diff -r 4c9aa5f7bfa0 -r 983e98da2a42 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Thu Oct 16 10:59:43 2014 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Thu Oct 16 12:09:57 2014 +0200 @@ -175,13 +175,17 @@ /* line context */ - class Generic_Line_Context[C](rules: ParserRuleSet, val context: Option[C]) + class Generic_Line_Context[C]( + rules: ParserRuleSet, + val context: Option[C], + val depth: Int) extends TokenMarker.LineContext(rules, null) { - override def hashCode: Int = context.hashCode + override def hashCode: Int = (context, depth).hashCode override def equals(that: Any): Boolean = that match { - case other: Generic_Line_Context[_] => context == other.context + case other: Generic_Line_Context[_] => + context == other.context && depth == other.depth case _ => false } } @@ -190,58 +194,53 @@ Untyped.get(buffer, "lineMgr") match { case line_mgr: LineManager => line_mgr.getLineContext(line) match { - case ctxt: Generic_Line_Context[C] => Some(ctxt) + case c: Generic_Line_Context[C] => Some(c) case _ => None } case _ => None } + def buffer_line_depth(buffer: JEditBuffer, line: Int): Int = + buffer_line_context(buffer, line) match { case Some(c) => c.depth case None => 0 } + + + /* token marker */ private val context_rules = new ParserRuleSet("isabelle", "MAIN") - private class Line_Context(context: Option[Scan.Line_Context]) - extends Generic_Line_Context[Scan.Line_Context](context_rules, context) - - - /* token marker */ + private class Line_Context(context: Option[Scan.Line_Context], depth: Int) + extends Generic_Line_Context[Scan.Line_Context](context_rules, context, depth) class Marker(mode: String) extends TokenMarker { override def markTokens(context: TokenMarker.LineContext, handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext = { - val line_ctxt = + val (opt_ctxt, depth) = context match { - case c: Line_Context => c.context - case _ => Some(Scan.Finished) + case c: Line_Context => (c.context, c.depth) + case _ => (Some(Scan.Finished), 0) } val line = if (raw_line == null) new Segment else raw_line val context1 = { - def no_context = - { - val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) - (List(styled_token), new Line_Context(None)) - } val (styled_tokens, context1) = - if (mode == "isabelle-ml" || mode == "sml") { - if (line_ctxt.isDefined) { - val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get) + (opt_ctxt, Isabelle.mode_syntax(mode)) match { + case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" => + val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt) val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source)) - (styled_tokens, new Line_Context(Some(ctxt1))) - } - else no_context - } - else { - Isabelle.mode_syntax(mode) match { - case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined => - val (tokens, ctxt1) = syntax.scan_line(line, line_ctxt.get) - val styled_tokens = - tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source)) - (styled_tokens, new Line_Context(Some(ctxt1))) - case _ => no_context - } + (styled_tokens, new Line_Context(Some(ctxt1), depth)) + + case (Some(ctxt), Some(syntax)) if syntax.has_tokens => + val (tokens, ctxt1, depth1) = syntax.scan_line(line, ctxt, depth) + val styled_tokens = + tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source)) + (styled_tokens, new Line_Context(Some(ctxt1), depth1)) + + case _ => + val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) + (List(styled_token), new Line_Context(None, 0)) } val extended = extended_styles(line) @@ -267,6 +266,7 @@ handler.handleToken(line, JEditToken.END, line.count, 0, context1) context1 } + val context2 = context1.intern handler.setLineContext(context2) context2