# HG changeset patch
# User wenzelm
# Date 1251991585 -7200
# Node ID 0e1d098940a7b2a19146ebad2f7b94b1ac8ff4b0
# Parent  9a4e5f93ccb64b0bd4face9171642b1e30a13e58
tuned imports;

diff -r 9a4e5f93ccb6 -r 0e1d098940a7 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- 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)
diff -r 9a4e5f93ccb6 -r 0e1d098940a7 src/Tools/jEdit/src/prover/State.scala
--- 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