--- 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)
}
--- 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"
--- 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)
--- 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
--- 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
--- /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
+ }
+ }
+}
+
--- 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))