# HG changeset patch # User wenzelm # Date 1413897704 -7200 # Node ID 8f92f17d8781f4e15b8c49be1e44e953746c3f49 # Parent c680f181b32efe7d8a82bb500d65d56e34ab69b9 support for structure matching; misc tuning; diff -r c680f181b32e -r 8f92f17d8781 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Tue Oct 21 13:56:42 2014 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Tue Oct 21 15:21:44 2014 +0200 @@ -216,11 +216,7 @@ } } - def scan_line( - input: CharSequence, - context: Scan.Line_Context, - structure: Outer_Syntax.Line_Structure) - : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Structure) = + def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) = { var in: Reader[Char] = new CharSequenceReader(input) val toks = new mutable.ListBuffer[Token] @@ -232,8 +228,7 @@ error("Unexpected failure of tokenizing input:\n" + rest.source.toString) } } - val tokens = toks.toList - (tokens, ctxt, line_structure(tokens, structure)) + (toks.toList, ctxt) } diff -r c680f181b32e -r 8f92f17d8781 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Oct 21 13:56:42 2014 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Oct 21 15:21:44 2014 +0200 @@ -46,6 +46,7 @@ "src/simplifier_trace_window.scala" "src/sledgehammer_dockable.scala" "src/spell_checker.scala" + "src/structure_matching.scala" "src/symbols_dockable.scala" "src/syslog_dockable.scala" "src/text_overview.scala" diff -r c680f181b32e -r 8f92f17d8781 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Tue Oct 21 13:56:42 2014 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Tue Oct 21 15:21:44 2014 +0200 @@ -251,6 +251,8 @@ text_area.addKeyListener(key_listener) text_area.addCaretListener(caret_listener) text_area.addLeftOfScrollBar(overview) + Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)). + foreach(text_area.addStructureMatcher(_)) session.raw_edits += main session.commands_changed += main } @@ -261,6 +263,8 @@ session.raw_edits -= main session.commands_changed -= main + Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)). + foreach(text_area.removeStructureMatcher(_)) text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke() text_area.removeCaretListener(caret_listener); delay_caret_update.revoke() text_area.removeKeyListener(key_listener) diff -r c680f181b32e -r 8f92f17d8781 src/Tools/jEdit/src/fold_handling.scala --- a/src/Tools/jEdit/src/fold_handling.scala Tue Oct 21 13:56:42 2014 +0200 +++ b/src/Tools/jEdit/src/fold_handling.scala Tue Oct 21 15:21:44 2014 +0200 @@ -29,16 +29,16 @@ } override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = - Token_Markup.buffer_line_structure(buffer, line).depth max 0 + Token_Markup.buffer_line_context(buffer, line).structure.depth max 0 override def getPrecedingFoldLevels( buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] = { - val struct = Token_Markup.buffer_line_structure(buffer, line) + val struct = Token_Markup.buffer_line_context(buffer, line).structure val result = if (line > 0 && struct.command) Range.inclusive(line - 1, 0, -1).iterator. - map(Token_Markup.buffer_line_structure(buffer, _)). + map(i => Token_Markup.buffer_line_context(buffer, i).structure). takeWhile(_.improper).map(_ => struct.depth max 0).toList else Nil diff -r c680f181b32e -r 8f92f17d8781 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Oct 21 13:56:42 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Oct 21 15:21:44 2014 +0200 @@ -15,7 +15,7 @@ import scala.swing.event.ButtonClicked import org.gjt.sp.jedit.{jEdit, View, Buffer} -import org.gjt.sp.jedit.textarea.JEditTextArea +import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher} import org.gjt.sp.jedit.syntax.TokenMarker import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord} import org.gjt.sp.jedit.options.PluginOptions @@ -73,6 +73,12 @@ def token_marker(name: String): Option[TokenMarker] = markers.get(name) + /* structure matchers */ + + def structure_matchers(name: String): List[StructureMatcher] = + if (name == "isabelle") List(Structure_Matching.Isabelle_Matcher) else Nil + + /* dockable windows */ private def wm(view: View): DockableWindowManager = view.getDockableWindowManager diff -r c680f181b32e -r 8f92f17d8781 src/Tools/jEdit/src/structure_matching.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/structure_matching.scala Tue Oct 21 15:21:44 2014 +0200 @@ -0,0 +1,42 @@ +/* Title: Tools/jEdit/src/structure_matching.scala + Author: Makarius + +Structure matcher for Isabelle/Isar outer syntax. +*/ + +package isabelle.jedit + + +import isabelle._ + +import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher} + + +object Structure_Matching +{ + object Isabelle_Matcher extends StructureMatcher + { + def getMatch(text_area: TextArea): StructureMatcher.Match = + { + val buffer = text_area.getBuffer + val caret_line = text_area.getCaretLine + + PIDE.session.recent_syntax match { + case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => + Token_Markup.buffer_line_tokens(syntax, buffer, caret_line) match { + case Some(tokens) => + // FIXME + null + case None => null + } + case _ => null + } + } + + def selectMatch(text_area: TextArea) + { + // FIXME + } + } +} + diff -r c680f181b32e -r 8f92f17d8781 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Tue Oct 21 13:56:42 2014 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Tue Oct 21 15:21:44 2014 +0200 @@ -177,6 +177,11 @@ private val context_rules = new ParserRuleSet("isabelle", "MAIN") + object Line_Context + { + val init = new Line_Context(Some(Scan.Finished), Outer_Syntax.Line_Structure.init) + } + class Line_Context( val context: Option[Scan.Line_Context], val structure: Outer_Syntax.Line_Structure) @@ -190,7 +195,7 @@ } } - def buffer_line_context(buffer: JEditBuffer, line: Int): Option[Line_Context] = + def buffer_line_context(buffer: JEditBuffer, line: Int): Line_Context = Untyped.get(buffer, "lineMgr") match { case line_mgr: LineManager => def context = @@ -198,18 +203,24 @@ case c: Line_Context => Some(c) case _ => None } - context orElse { + context getOrElse { buffer.markTokens(line, DummyTokenHandler.INSTANCE) - context + context getOrElse Line_Context.init } - case _ => None + case _ => Line_Context.init } - def buffer_line_structure(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Structure = - buffer_line_context(buffer, line) match { - case Some(c) => c.structure - case _ => Outer_Syntax.Line_Structure.init - } + def buffer_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int) + : Option[List[Token]] = + { + val line_context = + if (line == 0) Line_Context.init + else buffer_line_context(buffer, line - 1) + for { + ctxt <- line_context.context + text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line)) + } yield syntax.scan_line(text, ctxt)._1 + } /* token marker */ @@ -219,24 +230,22 @@ override def markTokens(context: TokenMarker.LineContext, handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext = { - val (opt_ctxt, structure) = - context match { - case c: Line_Context => (c.context, c.structure) - case _ => (Some(Scan.Finished), Outer_Syntax.Line_Structure.init) - } val line = if (raw_line == null) new Segment else raw_line + val line_context = context match { case c: Line_Context => c case _ => Line_Context.init } + val structure = line_context.structure val context1 = { val (styled_tokens, context1) = - (opt_ctxt, Isabelle.mode_syntax(mode)) match { + (line_context.context, 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), structure)) case (Some(ctxt), Some(syntax)) if syntax.has_tokens => - val (tokens, ctxt1, structure1) = syntax.scan_line(line, ctxt, structure) + val (tokens, ctxt1) = syntax.scan_line(line, ctxt) + val structure1 = syntax.line_structure(tokens, structure) val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source)) (styled_tokens, new Line_Context(Some(ctxt1), structure1))