--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Thu Sep 03 16:47:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Thu Sep 03 17:26:25 2009 +0200
@@ -7,7 +7,8 @@
package isabelle.jedit
-import isabelle.prover.{Command, MarkupNode, Prover}
+
+import isabelle.prover.Prover
import isabelle.Markup
import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -95,7 +96,9 @@
def is_outer(kind: String) = outer.contains(kind)
}
-class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker
+
+class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover)
+ extends TokenMarker
{
override def markTokens(prev: TokenMarker.LineContext,
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
@@ -142,8 +145,8 @@
handler.setLineContext(context)
return context
}
+}
-}
class IndexLineContext(val line: Int, prev: IndexLineContext)
extends TokenMarker.LineContext(new ParserRuleSet("isabelle", "MAIN"), prev)
--- a/src/Tools/jEdit/src/prover/State.scala Thu Sep 03 16:47:42 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala Thu Sep 03 17:26:25 2009 +0200
@@ -35,7 +35,6 @@
lazy val highlight_node: MarkupNode =
{
- import MarkupNode._
markup_root.filter(_.info match {
case RootInfo() | HighlightInfo(_) => true
case _ => false