misc modernization of names;
authorwenzelm
Tue, 08 Dec 2009 16:30:20 +0100
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34761 0ad6d8372f9d
misc modernization of names;
src/Tools/jEdit/dist-template/properties/jedit.props
src/Tools/jEdit/plugin/Isabelle.props
src/Tools/jEdit/plugin/actions.xml
src/Tools/jEdit/plugin/dockables.xml
src/Tools/jEdit/plugin/services.xml
src/Tools/jEdit/src/jedit/browse_version_dockable.scala
src/Tools/jEdit/src/jedit/document_overview.scala
src/Tools/jEdit/src/jedit/history_dockable.scala
src/Tools/jEdit/src/jedit/isabelle_encoding.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_options.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
src/Tools/jEdit/src/jedit/option_pane.scala
src/Tools/jEdit/src/jedit/plugin.scala
src/Tools/jEdit/src/jedit/prover_setup.scala
src/Tools/jEdit/src/jedit/raw_output_dockable.scala
src/Tools/jEdit/src/jedit/results_dockable.scala
src/Tools/jEdit/src/jedit/token_marker.scala
src/Tools/jEdit/src/proofdocument/command.scala
src/Tools/jEdit/src/proofdocument/markup_node.scala
src/Tools/jEdit/src/proofdocument/proof_document.scala
src/Tools/jEdit/src/proofdocument/prover.scala
src/Tools/jEdit/src/proofdocument/state.scala
src/Tools/jEdit/src/proofdocument/theory_view.scala
src/Tools/jEdit/src/proofdocument/token.scala
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Dec 08 16:30:20 2009 +0100
@@ -170,9 +170,9 @@
 encodingDetectors=BOM XML-PI buffer-local-property
 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
 firstTime=false
-isabelle-browser.dock-position=bottom
-isabelle-output.dock-position=bottom
-isabelle-state.dock-position=bottom
+isabelle-history.dock-position=bottom
+isabelle-raw-output.dock-position=bottom
+isabelle-results.dock-position=bottom
 isabelle.activate.shortcut=CS+ENTER
 mode.isabelle.sidekick.showStatusWindow.label=true
 sidekick-tree.dock-position=right
--- a/src/Tools/jEdit/plugin/Isabelle.props	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Tue Dec 08 16:30:20 2009 +0100
@@ -6,12 +6,11 @@
 plugin.isabelle.jedit.Plugin.name=Isabelle
 plugin.isabelle.jedit.Plugin.author=Johannes Hlzl, Fabian Immler, Makarius Wenzel
 plugin.isabelle.jedit.Plugin.version=0.0.1
-plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing
+plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof processing
 
 #system parameters
 plugin.isabelle.jedit.Plugin.activate=defer
 plugin.isabelle.jedit.Plugin.usePluginHome=false
-plugin.isabelle.jedit.Plugin.jars=
 
 #dependencies
 plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
@@ -23,23 +22,23 @@
 #options
 plugin.isabelle.jedit.Plugin.option-pane=isabelle
 options.isabelle.label=Isabelle
-options.isabelle.code=new isabelle.jedit.OptionPane();
+options.isabelle.code=new isabelle.jedit.Isabelle_Options();
 options.isabelle.logic.title=Logic
 options.isabelle.font-size.title=Font Size
 options.isabelle.font-size=14
 
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-state isabelle.show-output isabelle.show-browser
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-results isabelle.show-raw-output isabelle.show-history
 isabelle.activate.label=Activate current buffer
-isabelle.show-state.label=Show State
-isabelle.show-output.label=Show Output
-isabelle.show-browser.label=Show Version-Browser
+isabelle.show-results.label=Show Results
+isabelle.show-raw-output.label=Show Raw Output
+isabelle.show-history.label=Show History
 
 #dockables
-isabelle-output.title=Isabelle Output
-isabelle-state.title=Isabelle State
-isabelle-browser.title=Isabelle Browse-Version
+isabelle-results.title=Results
+isabelle-raw-output.title=Raw Output
+isabelle-history.title=History
 
 #SideKick
 sidekick.parser.isabelle.label=Isabelle
--- a/src/Tools/jEdit/plugin/actions.xml	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml	Tue Dec 08 16:30:20 2009 +0100
@@ -1,19 +1,7 @@
+<?xml version="1.0"?>
+<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
+
 <ACTIONS>
-	<ACTION NAME="isabelle.show-output">
-		<CODE>
-			wm.addDockableWindow("isabelle-output");
-		</CODE>
-	</ACTION>
-	<ACTION NAME="isabelle.show-state">
-		<CODE>
-			wm.addDockableWindow("isabelle-state");
-		</CODE>
-	</ACTION>
-  <ACTION NAME="isabelle.show-browser">
-		<CODE>
-			wm.addDockableWindow("isabelle-browser");
-		</CODE>
-	</ACTION>
   <ACTION NAME="isabelle.activate">
 		<CODE>
 			isabelle.jedit.Isabelle.plugin().switch_active(view);
@@ -22,4 +10,19 @@
 			return isabelle.jedit.Isabelle.plugin().is_active(view.getBuffer());
 		</IS_SELECTED>
 	</ACTION>
+	<ACTION NAME="isabelle.show-results">
+		<CODE>
+			wm.addDockableWindow("isabelle-results");
+		</CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.show-raw-output">
+		<CODE>
+			wm.addDockableWindow("isabelle-raw-output");
+		</CODE>
+	</ACTION>
+  <ACTION NAME="isabelle.show-history">
+		<CODE>
+			wm.addDockableWindow("isabelle-history");
+		</CODE>
+	</ACTION>
 </ACTIONS>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/dockables.xml	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/dockables.xml	Tue Dec 08 16:30:20 2009 +0100
@@ -1,15 +1,14 @@
 <?xml version="1.0"?>
-
 <!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
 
 <DOCKABLES>
-	<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
-		new isabelle.jedit.OutputDockable(view, position);
+	<DOCKABLE NAME="isabelle-results" MOVABLE="TRUE">
+		new isabelle.jedit.Results_Dockable(view, position).peer();
 	</DOCKABLE>
-	<DOCKABLE NAME="isabelle-state" MOVABLE="TRUE">
-		new isabelle.jedit.StateViewDockable(view, position);
+	<DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
+		new isabelle.jedit.Raw_Output_Dockable(view, position);
 	</DOCKABLE>
-	<DOCKABLE NAME="isabelle-browser" MOVABLE="TRUE">
-		new isabelle.jedit.BrowseVersionDockable(view, position).peer();
+	<DOCKABLE NAME="isabelle-history" MOVABLE="TRUE">
+		new isabelle.jedit.History_Dockable(view, position).peer();
 	</DOCKABLE>
 </DOCKABLES>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/services.xml	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/services.xml	Tue Dec 08 16:30:20 2009 +0100
@@ -1,13 +1,14 @@
 <?xml version="1.0"?>
 <!DOCTYPE SERVICES SYSTEM "services.dtd">
+
 <SERVICES>
 	<SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
 		new isabelle.jedit.Isabelle_Encoding();
 	</SERVICE>
 	<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
-		new isabelle.jedit.IsabelleSideKickParser();
+		new isabelle.jedit.Isabelle_Sidekick();
 	</SERVICE>
   <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
-    new isabelle.jedit.IsabelleHyperlinkSource();
+    new isabelle.jedit.Isabelle_Hyperlinks();
   </SERVICE>
 </SERVICES>
--- a/src/Tools/jEdit/src/jedit/browse_version_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-/*
- * Dockable window for navigating through the document-versions
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-import isabelle.proofdocument.Change
-
-import java.awt.Dimension
-import scala.swing.{ListView, FlowPanel}
-import scala.swing.event.ListSelectionChanged
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
-
-
-class BrowseVersionDockable(view: View, position: String) extends FlowPanel
-{
-  if (position == DockableWindowManager.FLOATING)
-    preferredSize = new Dimension(500, 250)
-
-  def prover_setup(): Option[ProverSetup] = Isabelle.prover_setup(view.getBuffer)
-  def get_versions() =
-    prover_setup() match {
-      case None => Nil
-      case Some(setup) => setup.theory_view.changes
-    }
-
-  val list = new ListView[Change]
-  list.fixedCellWidth = 500
-  list.listData = get_versions()
-  contents += list
-
-  listenTo(list.selection)
-  reactions += {
-    case ListSelectionChanged(source, range, false) =>
-        prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
-    }
-
-  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
-}
--- a/src/Tools/jEdit/src/jedit/document_overview.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_overview.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -6,8 +6,8 @@
 
 package isabelle.jedit
 
-import isabelle.prover.{Prover, Command}
-import isabelle.proofdocument.ProofDocument
+
+import isabelle.proofdocument.{Command, Proof_Document, Prover, Theory_View}
 
 import javax.swing.{JPanel, ToolTipManager}
 import java.awt.event.{MouseAdapter, MouseEvent}
@@ -21,7 +21,7 @@
 class Document_Overview(
     prover: Prover,
     text_area: JEditTextArea,
-    to_current: (ProofDocument, Int) => Int)
+    to_current: (Proof_Document, Int) => Int)
   extends JPanel(new BorderLayout)
 {
   private val WIDTH = 10
@@ -67,7 +67,7 @@
       val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
       val y = line_to_y(line1)
       val height = HEIGHT * (line2 - line1)
-      gfx.setColor(TheoryView.choose_color(command, doc))
+      gfx.setColor(Theory_View.choose_color(command, doc))
       gfx.fillRect(0, y, getWidth - 1, height)
     }
   }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/history_dockable.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -0,0 +1,44 @@
+/*
+ * Dockable window for navigating through the document history
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import isabelle.proofdocument.Change
+
+import java.awt.Dimension
+import scala.swing.{ListView, FlowPanel}
+import scala.swing.event.ListSelectionChanged
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+class History_Dockable(view: View, position: String) extends FlowPanel
+{
+  if (position == DockableWindowManager.FLOATING)
+    preferredSize = new Dimension(500, 250)
+
+  def prover_setup(): Option[Prover_Setup] = Isabelle.prover_setup(view.getBuffer)
+  def get_versions() =
+    prover_setup() match {
+      case None => Nil
+      case Some(setup) => setup.theory_view.changes
+    }
+
+  val list = new ListView[Change]
+  list.fixedCellWidth = 500
+  list.listData = get_versions()
+  contents += list
+
+  listenTo(list.selection)
+  reactions += {
+    case ListSelectionChanged(source, range, false) =>
+      prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
+  }
+
+  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
+}
--- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -6,6 +6,7 @@
 
 package isabelle.jedit
 
+
 import org.gjt.sp.jedit.io.Encoding
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -6,6 +6,7 @@
 
 package isabelle.jedit
 
+
 import java.io.File
 
 import gatchan.jedit.hyperlinks.Hyperlink
@@ -17,10 +18,10 @@
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.TextUtilities
 
-import isabelle.prover.Command
+import isabelle.proofdocument.Command
 
 
-class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
+private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
   extends AbstractHyperlink(start, end, line, "")
 {
   override def click(view: View) {
@@ -28,21 +29,22 @@
   }
 }
 
-class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
+class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
   extends AbstractHyperlink(start, end, line, "")
 {
   override def click(view: View) = {
     Isabelle.system.source_file(ref_file) match {
-      case None => System.err.println("Could not find source file " + ref_file)
+      case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
       case Some(file) =>
         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
     }
   }
 }
 
-class IsabelleHyperlinkSource extends HyperlinkSource
+class Isabelle_Hyperlinks extends HyperlinkSource
 {
-	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
+	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
+	{
     val prover = Isabelle.prover_setup(buffer).map(_.prover)
     val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
     if (prover.isEmpty || theory_view_opt.isEmpty) null
@@ -61,11 +63,11 @@
               val end = theory_view.to_current(document, command_start + ref.stop)
               ref.info match {
                 case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
-                  new ExternalHyperlink(begin, end, line, ref_file, ref_line)
+                  new External_Hyperlink(begin, end, line, ref_file, ref_line)
                 case Command.RefInfo(_, _, Some(id), Some(offset)) =>
                   prover.get.command(id) match {
                     case Some(ref_cmd) =>
-                      new InternalHyperlink(begin, end, line,
+                      new Internal_Hyperlink(begin, end, line,
                         theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
                     case None => null
                   }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -0,0 +1,44 @@
+/*
+ * Editor pane for plugin options
+ *
+ * @author Johannes Hölzl, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import javax.swing.{JComboBox, JSpinner}
+
+import org.gjt.sp.jedit.AbstractOptionPane
+
+
+class Isabelle_Options extends AbstractOptionPane("isabelle")
+{
+  private val logic_name = new JComboBox()
+  private val font_size = new JSpinner()
+
+  override def _init()
+  {
+    addComponent(Isabelle.Property("logic.title"), {
+      for (name <- Isabelle.system.find_logics()) {
+        logic_name.addItem(name)
+        if (name == Isabelle.Property("logic"))
+          logic_name.setSelectedItem(name)
+      }
+      logic_name
+    })
+    addComponent(Isabelle.Property("font-size.title"), {
+      font_size.setValue(Isabelle.Int_Property("font-size"))
+      font_size
+    })
+  }
+
+  override def _save()
+  {
+    val logic = logic_name.getSelectedItem.asInstanceOf[String]
+    Isabelle.Property("logic") = logic
+
+    val size = font_size.getValue().asInstanceOf[Int]
+    Isabelle.Int_Property("font-size") = size
+  }
+}
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -7,6 +7,7 @@
 
 package isabelle.jedit
 
+
 import scala.collection.Set
 import scala.collection.immutable.TreeSet
 
@@ -18,11 +19,10 @@
 import errorlist.DefaultErrorSource
 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
 
-import isabelle.prover.{Command, Markup_Node}
-import isabelle.proofdocument.ProofDocument
+import isabelle.proofdocument.{Command, Markup_Node, Proof_Document}
 
 
-class IsabelleSideKickParser extends SideKickParser("isabelle")
+class Isabelle_Sidekick extends SideKickParser("isabelle")
 {
   /* parsing */
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -0,0 +1,153 @@
+/*
+ * include isabelle's command- and keyword-declarations
+ * live in jEdits syntax-highlighting
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.jedit
+
+
+import isabelle.proofdocument.Prover
+import isabelle.Markup
+
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.syntax.{Token => JToken,
+  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
+
+import java.awt.Color
+import java.awt.Font
+import javax.swing.text.Segment;
+
+
+object Isabelle_Token_Marker
+{
+  /* line context */
+
+  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
+  private class LineContext(val line: Int, prev: LineContext)
+    extends TokenMarker.LineContext(rule_set, prev)
+
+
+  /* mapping to jEdit token types */
+  // TODO: as properties or CSS style sheet
+
+  private val choose_byte: Map[String, Byte] =
+  {
+    import JToken._
+    Map[String, Byte](
+      // logical entities
+      Markup.TCLASS -> LABEL,
+      Markup.TYCON -> LABEL,
+      Markup.FIXED_DECL -> LABEL,
+      Markup.FIXED -> LABEL,
+      Markup.CONST_DECL -> LABEL,
+      Markup.CONST -> LABEL,
+      Markup.FACT_DECL -> LABEL,
+      Markup.FACT -> LABEL,
+      Markup.DYNAMIC_FACT -> LABEL,
+      Markup.LOCAL_FACT_DECL -> LABEL,
+      Markup.LOCAL_FACT -> LABEL,
+      // inner syntax
+      Markup.TFREE -> LITERAL2,
+      Markup.FREE -> LITERAL2,
+      Markup.TVAR -> LITERAL3,
+      Markup.SKOLEM -> LITERAL3,
+      Markup.BOUND -> LITERAL3,
+      Markup.VAR -> LITERAL3,
+      Markup.NUM -> DIGIT,
+      Markup.FLOAT -> DIGIT,
+      Markup.XNUM -> DIGIT,
+      Markup.XSTR -> LITERAL4,
+      Markup.LITERAL -> LITERAL4,
+      Markup.INNER_COMMENT -> COMMENT1,
+      Markup.SORT -> FUNCTION,
+      Markup.TYP -> FUNCTION,
+      Markup.TERM -> FUNCTION,
+      Markup.PROP -> FUNCTION,
+      Markup.ATTRIBUTE -> FUNCTION,
+      Markup.METHOD -> FUNCTION,
+      // ML syntax
+      Markup.ML_KEYWORD -> KEYWORD2,
+      Markup.ML_IDENT -> NULL,
+      Markup.ML_TVAR -> LITERAL3,
+      Markup.ML_NUMERAL -> DIGIT,
+      Markup.ML_CHAR -> LITERAL1,
+      Markup.ML_STRING -> LITERAL1,
+      Markup.ML_COMMENT -> COMMENT1,
+      Markup.ML_MALFORMED -> INVALID,
+      // embedded source text
+      Markup.ML_SOURCE -> COMMENT4,
+      Markup.DOC_SOURCE -> COMMENT4,
+      Markup.ANTIQ -> COMMENT4,
+      Markup.ML_ANTIQ -> COMMENT4,
+      Markup.DOC_ANTIQ -> COMMENT4,
+      // outer syntax
+      Markup.IDENT -> NULL,
+      Markup.COMMAND -> OPERATOR,
+      Markup.KEYWORD -> KEYWORD4,
+      Markup.VERBATIM -> COMMENT3,
+      Markup.COMMENT -> COMMENT1,
+      Markup.CONTROL -> COMMENT3,
+      Markup.MALFORMED -> INVALID,
+      Markup.STRING -> LITERAL3,
+      Markup.ALTSTRING -> LITERAL1
+    ).withDefaultValue(NULL)
+  }
+
+  def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
+    styles(choose_byte(kind)).getForegroundColor
+}
+
+
+class Isabelle_Token_Marker(buffer: JEditBuffer, prover: Prover) extends TokenMarker
+{
+  override def markTokens(prev: TokenMarker.LineContext,
+      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
+  {
+    val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
+    val line = if (prev == null) 0 else previous.line + 1
+    val context = new Isabelle_Token_Marker.LineContext(line, previous)
+    val start = buffer.getLineStartOffset(line)
+    val stop = start + line_segment.count
+
+    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
+    val document = theory_view.current_document()
+    def to: Int => Int = theory_view.to_current(document, _)
+    def from: Int => Int = theory_view.from_current(document, _)
+
+    var next_x = start
+    var cmd = document.command_at(from(start))
+    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
+      val command = cmd.get
+      for {
+        markup <- command.highlight(document).flatten
+        command_start = command.start(document)
+        abs_start = to(command_start + markup.start)
+        abs_stop = to(command_start + markup.stop)
+        if (abs_stop > start)
+        if (abs_start < stop)
+        byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
+        token_start = (abs_start - start) max 0
+        token_length =
+          (abs_stop - abs_start) -
+          ((start - abs_start) max 0) -
+          ((abs_stop - stop) max 0)
+      } {
+        if (start + token_start > next_x)
+          handler.handleToken(line_segment, 1,
+            next_x - start, start + token_start - next_x, context)
+        handler.handleToken(line_segment, byte,
+          token_start, token_length, context)
+        next_x = start + token_start + token_length
+      }
+      cmd = document.commands.next(command)
+    }
+    if (next_x < stop)
+      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
+
+    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
+    handler.setLineContext(context)
+    return context
+  }
+}
--- a/src/Tools/jEdit/src/jedit/option_pane.scala	Tue Dec 08 14:49:01 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-/*
- * Editor pane for plugin options
- *
- * @author Johannes Hölzl, TU Munich
- */
-
-package isabelle.jedit
-
-import javax.swing.{JComboBox, JSpinner}
-
-import org.gjt.sp.jedit.AbstractOptionPane
-
-
-class OptionPane extends AbstractOptionPane("isabelle")
-{
-  private val logic_name = new JComboBox()
-  private val font_size = new JSpinner()
-
-  override def _init()
-  {
-    addComponent(Isabelle.Property("logic.title"), {
-      for (name <- Isabelle.system.find_logics()) {
-        logic_name.addItem(name)
-        if (name == Isabelle.Property("logic"))
-          logic_name.setSelectedItem(name)
-      }
-      logic_name
-    })
-    addComponent(Isabelle.Property("font-size.title"), {
-      font_size.setValue(Isabelle.Int_Property("font-size"))
-      font_size
-    })
-  }
-
-  override def _save()
-  {
-    val logic = logic_name.getSelectedItem.asInstanceOf[String]
-    Isabelle.Property("logic") = logic
-
-    val size = font_size.getValue().asInstanceOf[Int]
-    Isabelle.Int_Property("font-size") = size
-  }
-}
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -3,6 +3,7 @@
  *
  * @author Johannes Hölzl, TU Munich
  * @author Fabian Immler, TU Munich
+ * @author Makarius
  */
 
 package isabelle.jedit
@@ -14,8 +15,7 @@
 
 import scala.collection.mutable
 
-import isabelle.prover.{Prover, Command}
-import isabelle.proofdocument.ProofDocument
+import isabelle.proofdocument.{Command, Proof_Document, Prover}
 import isabelle.Isabelle_System
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
@@ -98,12 +98,12 @@
 
   /* mapping buffer <-> prover */
 
-  private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
+  private val mapping = new mutable.HashMap[JEditBuffer, Prover_Setup]
 
   private def install(view: View)
   {
     val buffer = view.getBuffer
-    val prover_setup = new ProverSetup(buffer)
+    val prover_setup = new Prover_Setup(buffer)
     mapping.update(buffer, prover_setup)
     prover_setup.activate(view)
   }
@@ -115,7 +115,7 @@
     if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
     else install(view)
 
-  def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
+  def prover_setup(buffer: JEditBuffer): Option[Prover_Setup] = mapping.get(buffer)
   def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
 
 
--- a/src/Tools/jEdit/src/jedit/prover_setup.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/prover_setup.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -9,18 +9,18 @@
 
 import org.gjt.sp.jedit.{Buffer, View}
 
-import isabelle.prover.Prover
+import isabelle.proofdocument.{Prover, Theory_View}
 
 
-class ProverSetup(buffer: Buffer)
+class Prover_Setup(buffer: Buffer)
 {
   var prover: Prover = null
-  var theory_view: TheoryView = null
+  var theory_view: Theory_View = null
 
   def activate(view: View)
   {
-    // TheoryView starts prover
-    theory_view = new TheoryView(view.getTextArea)
+    // Theory_View starts prover
+    theory_view = new Theory_View(view.getTextArea)
     prover = theory_view.prover
 
     theory_view.activate()
--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -15,8 +15,8 @@
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
-class OutputDockable(view : View, position : String) extends JPanel {
-
+class Raw_Output_Dockable(view: View, position: String) extends JPanel
+{
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
--- a/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -7,13 +7,14 @@
 
 package isabelle.jedit
 
+
 import isabelle.XML
 
+import scala.swing.{BorderPanel, Component}
+
 import java.io.StringReader
 import java.awt.{BorderLayout, Dimension}
-
 import javax.swing.{JButton, JPanel, JScrollPane}
-
 import java.util.logging.{Logger, Level}
 
 import org.lobobrowser.html.parser._
@@ -31,12 +32,12 @@
 import scala.io.Source
 
 
-class StateViewDockable(view : View, position : String) extends JPanel {
-
+class Results_Dockable(view : View, position : String) extends BorderPanel
+{
   // outer panel
+
   if (position == DockableWindowManager.FLOATING)
-    setPreferredSize(new Dimension(500, 250))
-  setLayout(new BorderLayout)
+    preferredSize = new Dimension(500, 250)
 
 
   // global logging
@@ -87,7 +88,8 @@
   doc.appendChild(empty_body)
 
   panel.setDocument(doc, rcontext)
-  add(panel, BorderLayout.CENTER)
+
+  add(Component.wrap(panel), BorderPanel.Position.Center)
 
   
   // register for state-view
--- a/src/Tools/jEdit/src/jedit/token_marker.scala	Tue Dec 08 14:49:01 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-/*
- * include isabelle's command- and keyword-declarations
- * live in jEdits syntax-highlighting
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-
-import isabelle.prover.Prover
-import isabelle.Markup
-
-import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.syntax.{Token => JToken,
-  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
-
-import java.awt.Color
-import java.awt.Font
-import javax.swing.text.Segment;
-
-
-object DynamicTokenMarker
-{
-  /* line context */
-
-  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
-  private class LineContext(val line: Int, prev: LineContext)
-    extends TokenMarker.LineContext(rule_set, prev)
-
-
-  /* mapping to jEdit token types */
-  // TODO: as properties or CSS style sheet
-
-  private val choose_byte: Map[String, Byte] =
-  {
-    import JToken._
-    Map[String, Byte](
-      // logical entities
-      Markup.TCLASS -> LABEL,
-      Markup.TYCON -> LABEL,
-      Markup.FIXED_DECL -> LABEL,
-      Markup.FIXED -> LABEL,
-      Markup.CONST_DECL -> LABEL,
-      Markup.CONST -> LABEL,
-      Markup.FACT_DECL -> LABEL,
-      Markup.FACT -> LABEL,
-      Markup.DYNAMIC_FACT -> LABEL,
-      Markup.LOCAL_FACT_DECL -> LABEL,
-      Markup.LOCAL_FACT -> LABEL,
-      // inner syntax
-      Markup.TFREE -> LITERAL2,
-      Markup.FREE -> LITERAL2,
-      Markup.TVAR -> LITERAL3,
-      Markup.SKOLEM -> LITERAL3,
-      Markup.BOUND -> LITERAL3,
-      Markup.VAR -> LITERAL3,
-      Markup.NUM -> DIGIT,
-      Markup.FLOAT -> DIGIT,
-      Markup.XNUM -> DIGIT,
-      Markup.XSTR -> LITERAL4,
-      Markup.LITERAL -> LITERAL4,
-      Markup.INNER_COMMENT -> COMMENT1,
-      Markup.SORT -> FUNCTION,
-      Markup.TYP -> FUNCTION,
-      Markup.TERM -> FUNCTION,
-      Markup.PROP -> FUNCTION,
-      Markup.ATTRIBUTE -> FUNCTION,
-      Markup.METHOD -> FUNCTION,
-      // ML syntax
-      Markup.ML_KEYWORD -> KEYWORD2,
-      Markup.ML_IDENT -> NULL,
-      Markup.ML_TVAR -> LITERAL3,
-      Markup.ML_NUMERAL -> DIGIT,
-      Markup.ML_CHAR -> LITERAL1,
-      Markup.ML_STRING -> LITERAL1,
-      Markup.ML_COMMENT -> COMMENT1,
-      Markup.ML_MALFORMED -> INVALID,
-      // embedded source text
-      Markup.ML_SOURCE -> COMMENT4,
-      Markup.DOC_SOURCE -> COMMENT4,
-      Markup.ANTIQ -> COMMENT4,
-      Markup.ML_ANTIQ -> COMMENT4,
-      Markup.DOC_ANTIQ -> COMMENT4,
-      // outer syntax
-      Markup.IDENT -> NULL,
-      Markup.COMMAND -> OPERATOR,
-      Markup.KEYWORD -> KEYWORD4,
-      Markup.VERBATIM -> COMMENT3,
-      Markup.COMMENT -> COMMENT1,
-      Markup.CONTROL -> COMMENT3,
-      Markup.MALFORMED -> INVALID,
-      Markup.STRING -> LITERAL3,
-      Markup.ALTSTRING -> LITERAL1
-    ).withDefaultValue(NULL)
-  }
-
-  def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
-    styles(choose_byte(kind)).getForegroundColor
-}
-
-
-class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover)
-  extends TokenMarker
-{
-  override def markTokens(prev: TokenMarker.LineContext,
-      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
-  {
-    val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext]
-    val line = if (prev == null) 0 else previous.line + 1
-    val context = new DynamicTokenMarker.LineContext(line, previous)
-    val start = buffer.getLineStartOffset(line)
-    val stop = start + line_segment.count
-
-    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
-    val document = theory_view.current_document()
-    def to: Int => Int = theory_view.to_current(document, _)
-    def from: Int => Int = theory_view.from_current(document, _)
-
-    var next_x = start
-    var cmd = document.command_at(from(start))
-    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
-      val command = cmd.get
-      for {
-        markup <- command.highlight(document).flatten
-        command_start = command.start(document)
-        abs_start = to(command_start + markup.start)
-        abs_stop = to(command_start + markup.stop)
-        if (abs_stop > start)
-        if (abs_start < stop)
-        byte = DynamicTokenMarker.choose_byte(markup.info.toString)
-        token_start = (abs_start - start) max 0
-        token_length =
-          (abs_stop - abs_start) -
-          ((start - abs_start) max 0) -
-          ((abs_stop - stop) max 0)
-      } {
-        if (start + token_start > next_x)
-          handler.handleToken(line_segment, 1,
-            next_x - start, start + token_start - next_x, context)
-        handler.handleToken(line_segment, byte,
-          token_start, token_length, context)
-        next_x = start + token_start + token_length
-      }
-      cmd = document.commands.next(command)
-    }
-    if (next_x < stop)
-      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
-
-    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
-    handler.setLineContext(context)
-    return context
-  }
-}
--- a/src/Tools/jEdit/src/proofdocument/command.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -5,14 +5,13 @@
  * @author Fabian Immler, TU Munich
  */
 
-package isabelle.prover
+package isabelle.proofdocument
 
 
 import scala.actors.Actor, Actor._
 
 import scala.collection.mutable
 
-import isabelle.proofdocument.{Token, ProofDocument}
 import isabelle.jedit.{Isabelle, Plugin}
 import isabelle.XML
 
@@ -70,8 +69,8 @@
   def content(i: Int, j: Int): String = content.substring(i, j)
   val symbol_index = new Symbol.Index(content)
 
-  def start(doc: ProofDocument) = doc.token_start(tokens.first)
-  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
+  def start(doc: Proof_Document) = doc.token_start(tokens.first)
+  def stop(doc: Proof_Document) = doc.token_start(tokens.last) + tokens.last.length
 
   def contains(p: Token) = tokens.contains(p)
 
@@ -93,15 +92,15 @@
   /* results, markup, ... */
 
   private val empty_cmd_state = new Command_State(this)
-  private def cmd_state(doc: ProofDocument) =
+  private def cmd_state(doc: Proof_Document) =
     doc.states.getOrElse(this, empty_cmd_state)
 
-  def status(doc: ProofDocument) = cmd_state(doc).state.status
-  def results(doc: ProofDocument) = cmd_state(doc).results
-  def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
-  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
-  def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
-  def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
+  def status(doc: Proof_Document) = cmd_state(doc).state.status
+  def results(doc: Proof_Document) = cmd_state(doc).results
+  def markup_root(doc: Proof_Document) = cmd_state(doc).markup_root
+  def highlight(doc: Proof_Document) = cmd_state(doc).highlight
+  def type_at(doc: Proof_Document, offset: Int) = cmd_state(doc).type_at(offset)
+  def ref_at(doc: Proof_Document, offset: Int) = cmd_state(doc).ref_at(offset)
 }
 
 
--- a/src/Tools/jEdit/src/proofdocument/markup_node.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/markup_node.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -2,14 +2,14 @@
  * Document markup nodes, with connection to Swing tree model
  *
  * @author Fabian Immler, TU Munich
+ * @author Makarius
  */
 
-package isabelle.prover
+package isabelle.proofdocument
 
 
 import javax.swing.tree.DefaultMutableTreeNode
 
-import isabelle.proofdocument.ProofDocument
 
 
 class Markup_Node(val start: Int, val stop: Int, val info: Any)
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -8,14 +8,13 @@
 
 package isabelle.proofdocument
 
+
 import scala.actors.Actor, Actor._
 
 import java.util.regex.Pattern
 
-import isabelle.prover.{Prover, Command, Command_State}
 
-
-object ProofDocument
+object Proof_Document
 {
   // Be careful when changing this regex. Not only must it handle the
   // spurious end of a token but also:  
@@ -34,14 +33,14 @@
       "[()\\[\\]{}:;]", Pattern.MULTILINE)
 
   val empty =
-    new ProofDocument(isabelle.jedit.Isabelle.system.id(),
+    new Proof_Document(isabelle.jedit.Isabelle.system.id(),
       Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
 
   type StructureChange = List[(Option[Command], Option[Command])]
 
 }
 
-class ProofDocument(
+class Proof_Document(
   val id: String,
   val tokens: Linear_Set[Token],
   val token_start: Map[Token, Int],
@@ -49,10 +48,10 @@
   var states: Map[Command, Command_State],   // FIXME immutable
   is_command_keyword: String => Boolean)
 {
-  import ProofDocument.StructureChange
+  import Proof_Document.StructureChange
 
-  def set_command_keyword(f: String => Boolean): ProofDocument =
-    new ProofDocument(id, tokens, token_start, commands, states, f)
+  def set_command_keyword(f: String => Boolean): Proof_Document =
+    new Proof_Document(id, tokens, token_start, commands, states, f)
 
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
@@ -60,9 +59,9 @@
   
   /** token view **/
 
-  def text_changed(change: Change): (ProofDocument, StructureChange) =
+  def text_changed(change: Change): (Proof_Document, StructureChange) =
   {
-    def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
+    def edit_doc(doc_chgs: (Proof_Document, StructureChange), edit: Edit) = {
       val (doc, chgs) = doc_chgs
       val (new_doc, chg) = doc.text_edit(edit, change.id)
       (new_doc, chgs ++ chg)
@@ -70,7 +69,7 @@
     ((this, Nil: StructureChange) /: change.edits)(edit_doc)
   }
 
-  def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
+  def text_edit(e: Edit, id: String): (Proof_Document, StructureChange) =
   {
     case class TextChange(start: Int, added: String, removed: String)
     val change = e match {
@@ -116,7 +115,7 @@
 
     val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
     val matcher =
-      ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
+      Proof_Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
 
     while (matcher.find() && invalid_tokens != Nil) {
 			val kind =
@@ -158,7 +157,7 @@
     after_change: Option[Token],
     new_tokens: List[Token],
     new_token_start: Map[Token, Int]):
-  (ProofDocument, StructureChange) =
+  (Proof_Document, StructureChange) =
   {
     val new_tokenset = Linear_Set[Token]() ++ new_tokens
     val cmd_before_change = before_change match {
@@ -236,7 +235,7 @@
 
 
     val doc =
-      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
+      new Proof_Document(new_id, new_tokenset, new_token_start, new_commandset,
         states -- removed_commands, is_command_keyword)
 
     val removes =
--- a/src/Tools/jEdit/src/proofdocument/prover.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/prover.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -6,7 +6,7 @@
  * @author Makarius
  */
 
-package isabelle.prover
+package isabelle.proofdocument
 
 
 import scala.actors.Actor, Actor._
@@ -14,7 +14,6 @@
 import javax.swing.JTextArea
 
 import isabelle.jedit.Isabelle
-import isabelle.proofdocument.{ProofDocument, Change, Token}
 
 
 class Prover(system: Isabelle_System, logic: String)
@@ -41,7 +40,7 @@
   /* outgoing messages */
 
   val command_change = new Event_Bus[Command]
-  val document_change = new Event_Bus[ProofDocument]
+  val document_change = new Event_Bus[Proof_Document]
 
 
   /* prover process */
@@ -67,12 +66,12 @@
   @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
   @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
   val document_0 =
-    ProofDocument.empty.
+    Proof_Document.empty.
     set_command_keyword((s: String) => command_decls().contains(s))
   @volatile private var document_versions = List(document_0)
 
   def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
-  def document(id: Isar_Document.Document_ID): Option[ProofDocument] =
+  def document(id: Isar_Document.Document_ID): Option[Proof_Document] =
     document_versions.find(_.id == id)
 
 
--- a/src/Tools/jEdit/src/proofdocument/state.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/state.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -5,7 +5,7 @@
  * @author Makarius
  */
 
-package isabelle.prover
+package isabelle.proofdocument
 
 
 class State(
--- a/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -6,14 +6,12 @@
  * @author Makarius
  */
 
-package isabelle.jedit
+package isabelle.proofdocument
+
 
 import scala.actors.Actor, Actor._
 import scala.collection.mutable
 
-import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
-import isabelle.prover.{Prover, Command}
-
 import java.awt.{Color, Graphics2D}
 import javax.swing.event.{CaretListener, CaretEvent}
 
@@ -21,10 +19,12 @@
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
 import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
 
+import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker, Raw_Output_Dockable}
 
-object TheoryView
+
+object Theory_View
 {
-  def choose_color(command: Command, doc: ProofDocument): Color =
+  def choose_color(command: Command, doc: Proof_Document): Color =
   {
     command.status(doc) match {
       case Command.Status.UNPROCESSED => new Color(255, 228, 225)
@@ -36,7 +36,7 @@
 }
 
 
-class TheoryView(text_area: JEditTextArea)
+class Theory_View(text_area: JEditTextArea)
 {
   private val buffer = text_area.getBuffer
 
@@ -115,8 +115,8 @@
       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
     {
       val document = current_document()
-      def from_current(pos: Int) = TheoryView.this.from_current(document, pos)
-      def to_current(pos: Int) = TheoryView.this.to_current(document, pos)
+      def from_current(pos: Int) = Theory_View.this.from_current(document, pos)
+      def to_current(pos: Int) = Theory_View.this.to_current(document, pos)
       val saved_color = gfx.getColor
 
       val metrics = text_area.getPainter.getFontMetrics
@@ -128,7 +128,7 @@
         val begin = start max to_current(e.start(document))
         val finish = (end - 1) min to_current(e.stop(document))
         encolor(gfx, y, metrics.getHeight, begin, finish,
-          TheoryView.choose_color(e, document), true)
+          Theory_View.choose_color(e, document), true)
         cmd = document.commands.next(e)
       }
 
@@ -166,18 +166,19 @@
     }
   }
 
-  def activate() {
+  def activate()
+  {
     text_area.addCaretListener(selected_state_controller)
     text_area.addLeftOfScrollBar(overview)
     text_area.getPainter.
       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
-    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
+    buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover))
     buffer.addBufferListener(buffer_listener)
 
     val dockable =
-      text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
+      text_area.getView.getDockableWindowManager.getDockable("isabelle-raw-output")
     if (dockable != null) {
-      val output_dockable = dockable.asInstanceOf[OutputDockable]
+      val output_dockable = dockable.asInstanceOf[Raw_Output_Dockable]
       val output_text_view = prover.output_text_view
       output_dockable.set_text(output_text_view)
     }
@@ -196,7 +197,7 @@
 
   /* history of changes */
 
-  private def doc_or_pred(c: Change): ProofDocument =
+  private def doc_or_pred(c: Change): Proof_Document =
     prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
 
   def current_document() = doc_or_pred(current_change)
@@ -254,14 +255,14 @@
 
   /* transforming offsets */
 
-  private def changes_from(doc: ProofDocument): List[Edit] =
+  private def changes_from(doc: Proof_Document): List[Edit] =
     List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
       edits.toList
 
-  def from_current(doc: ProofDocument, offset: Int): Int =
+  def from_current(doc: Proof_Document, offset: Int): Int =
     (offset /: changes_from(doc).reverse) ((i, change) => change before i)
 
-  def to_current(doc: ProofDocument, offset: Int): Int =
+  def to_current(doc: Proof_Document, offset: Int): Int =
     (offset /: changes_from(doc)) ((i, change) => change after i)
 
 
--- a/src/Tools/jEdit/src/proofdocument/token.scala	Tue Dec 08 14:49:01 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/token.scala	Tue Dec 08 16:30:20 2009 +0100
@@ -8,9 +8,6 @@
 package isabelle.proofdocument
 
 
-import isabelle.prover.Command
-
-
 object Token {
   object Kind extends Enumeration
   {