# HG changeset patch
# User immler@in.tum.de
# Date 1233487267 -3600
# Node ID 5839e34ef0bdb6d10fcba16f33f69734b138c4f7
# Parent  6106e71c6ee5b3ef4aec9ad74a90339f203ff07f# Parent  839d1f0b2dd1a72ffa83846ab32b2bd3ed7ab681
merge

diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -22,7 +22,7 @@
   /* parsing */
 
   private var stopped = false
-  override def stop () = { stopped = true }
+  override def stop() = { stopped = true }
 
   def parse(buffer : Buffer, error_source : DefaultErrorSource): SideKickParsedData = {
     stopped = false
@@ -30,7 +30,7 @@
     val data = new SideKickParsedData(buffer.getName)
 
     val prover_setup = Isabelle.plugin.prover_setup(buffer)
-    if(prover_setup.isDefined){
+    if (prover_setup.isDefined) {
         val document = prover_setup.get.prover.document
         val commands = document.commands
         while (!stopped && commands.hasNext) {
@@ -54,7 +54,7 @@
   override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
     val buffer = pane.getBuffer
     val ps = Isabelle.prover_setup(buffer)
-    if(ps.isDefined) {
+    if (ps.isDefined) {
       val completions = ps.get.prover.completions
       def before_caret(i : Int) = buffer.getText(0 max caret - i, i)
       def next_nonfitting(s : String) : String = {
@@ -64,9 +64,9 @@
       }
       def suggestions(i : Int) : (Set[String], String)= {
         val text = before_caret(i)
-        if(!text.matches("\\s") && i < 30){
+        if (!text.matches("\\s") && i < 30) {
           val larger_results = suggestions(i + 1)
-          if(larger_results._1.size > 0) larger_results
+          if (larger_results._1.size > 0) larger_results
           else (completions.range(text, next_nonfitting(text)), text)
         } else (Set[String](), text)
 
@@ -76,10 +76,10 @@
       val descriptions = new java.util.LinkedList[String]
       // compute suggestions
       val (suggs, text) = suggestions(1)
-      for(s <- suggs) {
+      for (s <- suggs) {
         val decoded = Isabelle.symbols.decode(s)
         list.add(decoded)
-        if(decoded != s) descriptions.add(s) else descriptions.add(null)
+        if (decoded != s) descriptions.add(s) else descriptions.add(null)
       }
       return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
     } else return null
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/jedit/OptionPane.scala
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -44,7 +44,7 @@
     addComponent(Isabelle.Property("font-size.title"), {
       try {
         if (Isabelle.Property("font-size") != null)
-          fontSize.setValue(Integer.valueOf(Isabelle.Property("font-size")))
+          fontSize.setValue(Isabelle.Property("font-size").toInt)
       }
       catch {
         case e : NumberFormatException => 
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -31,7 +31,7 @@
   addMouseListener(new MouseAdapter {
     override def mousePressed(evt : MouseEvent) {
       val line = yToLine(evt.getY)
-      if(line >= 0 && line < textarea.getLineCount())
+      if (line >= 0 && line < textarea.getLineCount())
         textarea.setCaretPosition(textarea.getLineStartOffset(line))
     }
   })
@@ -52,7 +52,7 @@
 		val buffer = textarea.getBuffer
 		val lineCount = buffer.getLineCount
 		val line = yToLine(evt.getY())
-		if(line >= 0 && line < textarea.getLineCount)
+		if (line >= 0 && line < textarea.getLineCount)
 		{
       "TODO: Tooltip"
     } else ""
@@ -71,7 +71,7 @@
 
       gfx.setColor(light)
       gfx.fillRect(0, y, getWidth - 1, 1 max height)
-      if(height > 2){
+      if (height > 2) {
         gfx.setColor(dark)
         gfx.drawRect(0, y, getWidth - 1, height)
       }
@@ -82,7 +82,7 @@
 		super.paintComponent(gfx)
 
 		val buffer = textarea.getBuffer
-    for(c <- prover.document.commands)
+    for (c <- prover.document.commands)
       paintCommand(c, buffer, gfx)
     
 	}
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -12,7 +12,7 @@
 import java.awt.Font
 import javax.swing.JScrollPane
 
-import scala.collection.mutable.HashMap
+import scala.collection.mutable
 
 import isabelle.prover.{Prover, Command}
 import isabelle.IsabelleSystem
@@ -39,6 +39,12 @@
   var system: IsabelleSystem = null
   def symbols = system.symbols
 
+  // settings
+  def default_logic = {
+    val logic = Isabelle.Property("logic")
+    if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC")
+  }
+
   // plugin instance
   var plugin: Plugin = null
 
@@ -69,7 +75,7 @@
 
   // mapping buffer <-> prover
 
-  private val mapping = new HashMap[JEditBuffer, ProverSetup]
+  private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
 
   private def install(view: View) {
     val buffer = view.getBuffer
@@ -100,9 +106,9 @@
           case Some(prover_setup) => 
             prover_setup.theory_view.activate
             val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
-            if(dockable != null) {
+            if (dockable != null) {
               val output_dockable = dockable.asInstanceOf[OutputDockable]
-              if(output_dockable.getComponent(0) != prover_setup.output_text_view ) {
+              if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
                 output_dockable.asInstanceOf[OutputDockable].removeAll
                 output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
                 output_dockable.revalidate
@@ -111,7 +117,7 @@
         }
       case EditPaneUpdate.BUFFER_CHANGING =>
         val buffer = epu.getEditPane.getBuffer
-        if(buffer != null) mapping get buffer match {
+        if (buffer != null) mapping get buffer match {
           //only deactivate 'isabelle'-buffers!
           case None =>
           case Some(prover_setup) => prover_setup.theory_view.deactivate
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -22,7 +22,7 @@
 
 class ProverSetup(buffer: JEditBuffer)
 {
-  val prover = new Prover(Isabelle.system)
+  var prover: Prover = null
   var theory_view: TheoryView = null
 
   val state_update = new EventBus[Command]
@@ -34,7 +34,8 @@
   val output_text_view = new JTextArea
 
   def activate(view: View) {
-    prover.start(Isabelle.Property("logic"))
+    prover = new Prover(Isabelle.system, Isabelle.default_logic)
+    
     val buffer = view.getBuffer
     val dir = buffer.getDirectory
 
@@ -49,9 +50,9 @@
         output_text_view.append(text)
         val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
         //link process output if dockable is active
-        if(dockable != null) {
+        if (dockable != null) {
           val output_dockable = dockable.asInstanceOf[OutputDockable]
-          if(output_dockable.getComponent(0) != output_text_view ) {
+          if (output_dockable.getComponent(0) != output_text_view ) {
             output_dockable.asInstanceOf[OutputDockable].removeAll
             output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view))
             output_dockable.revalidate
@@ -65,7 +66,7 @@
       val state_panel =
         if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
         else null
-      if (state_panel != null){
+      if (state_panel != null) {
         if (state == null)
           state_panel.setDocument(null: Document)
         else
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -11,7 +11,7 @@
 import isabelle.renderer.UserAgent
 
 
-import scala.collection.mutable.{ArrayBuffer, HashMap}
+import scala.collection.mutable
 
 import java.awt.{BorderLayout, Adjustable, Dimension}
 import java.awt.event.{ActionListener, ActionEvent, AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent}
@@ -60,7 +60,7 @@
         //panel has to be displayable before calculating preferred size!
         add(panel)
         // recalculate preferred size after resizing the message_view
-        if(panel.getPreferredSize.getWidth.toInt != getWidth){
+        if (panel.getPreferredSize.getWidth.toInt != getWidth) {
           cache.renderer.relayout (panel, getWidth)
         }
         val width = panel.getPreferredSize.getWidth.toInt
@@ -76,12 +76,12 @@
     removeAll()
     //calculate offset in pixel
     val panel = place_message(no, 0)
-    val pixeloffset = if(panel != null) panel.getHeight*offset/100 else 0
+    val pixeloffset = if (panel != null) panel.getHeight*offset/100 else 0
     var n = no
     var y:Int = getHeight + pixeloffset
-    while (y >= 0 && n >= 0){
+    while (y >= 0 && n >= 0) {
       val panel = place_message (n, y)
-      if(panel != null) {
+      if (panel != null) {
         panel.setBorder(javax.swing.border.LineBorder.createBlackLineBorder)
         y = y - panel.getHeight
       }
@@ -132,9 +132,9 @@
   // do not show every new message, wait a certain amount of time
   val message_ind_timer : Timer = new Timer(250, new ActionListener {
       // this method is called to indicate a new message
-      override def actionPerformed(e:ActionEvent){
+      override def actionPerformed(e:ActionEvent) {
         //fire scroll-event if necessary and wanted
-        if(message_panel.no != buffer.size*subunits - 1 && infopanel.isAutoScroll) {
+        if (message_panel.no != buffer.size*subunits - 1 && infopanel.isAutoScroll) {
           vscroll.setValue(buffer.size*subunits - 1)
         }
         infopanel.setIndicator(false)
@@ -147,15 +147,15 @@
     infopanel.setIndicator(true)
     infopanel.setText(buffer.size.toString)
 
-    if (! message_ind_timer.isRunning()){
-      if(infopanel.isAutoScroll){
+    if (!message_ind_timer.isRunning()) {
+      if (infopanel.isAutoScroll) {
         vscroll.setValue(buffer.size*subunits - 1)
       }
       message_ind_timer.setRepeats(false)
       message_ind_timer.start()
     }
 
-    if(message_panel.no == -1) {
+    if (message_panel.no == -1) {
       message_panel.no = 0
       message_panel.revalidate
     }
@@ -164,7 +164,7 @@
   override def adjustmentValueChanged (e : AdjustmentEvent) = {
     //event-handling has to be so general (without UNIT_INCR,...)
     // because all events could be sent as TRACK e.g. on my mac
-    if (e.getSource == vscroll){
+    if (e.getSource == vscroll) {
       message_panel.no = e.getValue / subunits
       message_panel.offset = 100 - 100 * (e.getValue % subunits) / subunits
       message_panel.revalidate
@@ -179,12 +179,12 @@
 //Concrete Implementations
 
 //containing the unrendered messages
-class MessageBuffer extends HashMap[Int,Result] with Unrendered[Result]{
+class MessageBuffer extends mutable.HashMap[Int,Result] with Unrendered[Result]{
   override def addUnrendered (id: Int, m: Result) {
     update(id, m)
   }
-  override def getUnrendered (id: Int): Option[Result] = {
-    if(id < size && id >= 0 && apply(id) != null) Some (apply(id))
+  override def getUnrendered(id: Int): Option[Result] = {
+    if (id < size && id >= 0 && apply(id) != null) Some (apply(id))
     else None
   }
   override def size = super.size
@@ -192,11 +192,11 @@
 
 //containing the rendered messages
 class PanelCache (buffer: Unrendered[Result], val renderer: Renderer[Result, XHTMLPanel])
-  extends HashMap[Int, XHTMLPanel] with Rendered[Result, XHTMLPanel]{
+  extends mutable.HashMap[Int, XHTMLPanel] with Rendered[Result, XHTMLPanel]{
 
   override def getRendered (id: Int): Option[XHTMLPanel] = {
     //get message from buffer and render it if necessary
-    if(!isDefinedAt(id)){
+    if (!isDefinedAt(id)) {
       buffer.getUnrendered(id) match {
         case Some (message) =>
           update (id, renderer.render (message))
@@ -204,7 +204,7 @@
       }
     }
     val result = try {
-      Some (apply(id))
+      Some(apply(id))
     } catch {
       case _ => {
           None
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/jedit/SelectionActions.scala
--- a/src/Tools/jEdit/src/jedit/SelectionActions.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/SelectionActions.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -32,7 +32,7 @@
   }
   
   override def keyPressed(e: KeyEvent) {
-    if(e.getKeyCode == KeyEvent.VK_ENTER) {
+    if (e.getKeyCode == KeyEvent.VK_ENTER) {
       copyaction
       e.consume
     }
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -148,8 +148,7 @@
 
   def repaint(cmd: Command) =
   {
-    val status = cmd.status
-    if (text_area != null && status != Command.Status.REMOVE && status != Command.Status.REMOVED) {
+    if (text_area != null) {
       val start = text_area.getLineOfOffset(to_current(cmd.start))
       val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
       text_area.invalidateLineRange(start, stop)
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -37,7 +37,7 @@
 
 }
 
-class ProofDocument(text: Text, prover: Prover)
+class ProofDocument(text: Text, is_command_keyword: String => Boolean)
 {
   private var active = false 
   def activate() {
@@ -103,7 +103,7 @@
     while (matcher.find(position) && !finished) {
       position = matcher.end
 			val kind =
-        if (prover.is_command_keyword(matcher.group))
+        if (is_command_keyword(matcher.group))
           Token.Kind.COMMAND_START
         else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
           Token.Kind.COMMENT
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -11,7 +11,7 @@
 import javax.swing.text.Position
 import javax.swing.tree.DefaultMutableTreeNode
 
-import scala.collection.mutable.ListBuffer
+import scala.collection.mutable
 
 import isabelle.proofdocument.{Text, Token, ProofDocument}
 import isabelle.jedit.{Isabelle, Plugin}
@@ -24,8 +24,6 @@
   object Status extends Enumeration {
     val UNPROCESSED = Value("UNPROCESSED")
     val FINISHED = Value("FINISHED")
-    val REMOVE = Value("REMOVE")
-    val REMOVED = Value("REMOVED")
     val FAILED = Value("FAILED")
   }
 }
@@ -34,7 +32,10 @@
 class Command(text: Text, val first: Token, val last: Token)
 {
   val id = Isabelle.plugin.id()
-  
+
+
+  /* content */
+
   {
     var t = first
     while (t != null) {
@@ -43,37 +44,6 @@
     }
   }
 
-
-  /* command status */
-
-  private var _status = Command.Status.UNPROCESSED
-  def status = _status
-  def status_=(st: Command.Status.Value) = {
-    if (st == Command.Status.UNPROCESSED) {
-      // delete markup
-      for (child <- root_node.children) {
-        child.children = Nil
-      }
-    }
-    _status = st
-  }
-
-
-  /* accumulated results */
-
-  private val results = new ListBuffer[XML.Tree]
-  def add_result(tree: XML.Tree) { results += tree }
-
-  def result_document = XML.document(
-    results.toList match {
-      case Nil => XML.Elem("message", Nil, Nil)
-      case List(elem) => elem
-      case elems => XML.Elem("messages", Nil, List(elems.first, elems.last))  // FIXME all elems!?
-    }, "style")
-
-
-  /* content */
-
   override def toString = name
 
   val name = text.content(first.start, first.stop)
@@ -94,7 +64,40 @@
   }
 
 
-  /* markup tree */
+  /* command status */
+
+  var state_id: IsarDocument.State_ID = null
+
+  private var _status = Command.Status.UNPROCESSED
+  def status = _status
+  def status_=(st: Command.Status.Value) {
+    if (st == Command.Status.UNPROCESSED) {
+      // delete markup
+      for (child <- root_node.children) {
+        child.children = Nil
+      }
+    }
+    _status = st
+  }
+
+
+  /* results */
+
+  private val results = new mutable.ListBuffer[XML.Tree]
+  private val state_results = new mutable.ListBuffer[XML.Tree]
+  def add_result(running: Boolean, tree: XML.Tree) {
+    (if (running) state_results else results) += tree
+  }
+
+  def result_document = XML.document(
+    results.toList ::: state_results.toList match {
+      case Nil => XML.Elem("message", Nil, Nil)
+      case List(elem) => elem
+      case elems => XML.Elem("messages", Nil, elems)
+    }, "style")
+
+
+  /* markup */
 
   val root_node =
     new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -23,7 +23,7 @@
       override def getShortString : String = node.short
       override def getLongString : String = node.long
       override def getName : String = node.name
-      override def setName (name : String) = ()
+      override def setName(name : String) = ()
       override def setStart(start : Position) = ()
       override def getStart : Position = node.base.start + node.start
       override def setEnd(end : Position) = ()
@@ -48,7 +48,7 @@
   def children = children_cell
   def children_= (cs : List[MarkupNode]) = {
     swing_node.removeAllChildren
-    for(c <- cs) swing_node add c.swing_node
+    for (c <- cs) swing_node add c.swing_node
     children_cell = cs
   }
   
@@ -62,7 +62,7 @@
   private def remove(nodes : List[MarkupNode]) {
     children_cell = children diff nodes
 
-      for(node <- nodes) try {
+      for (node <- nodes) try {
         swing_node remove node.swing_node
       } catch { case e : IllegalArgumentException =>
         System.err.println(e.toString)
@@ -72,23 +72,23 @@
 
   def dfs : List[MarkupNode] = {
     var all = Nil : List[MarkupNode]
-    for(child <- children)
+    for (child <- children)
       all = child.dfs ::: all
     all = this :: all
     all
   }
 
   def insert(new_child : MarkupNode) : Unit = {
-    if(new_child fitting_into this){
-      for(child <- children){
-        if(new_child fitting_into child)
+    if (new_child fitting_into this) {
+      for (child <- children) {
+        if (new_child fitting_into child)
           child insert new_child
       }
-      if(new_child orphan){
+      if (new_child orphan) {
         // new_child did not fit into children of this
         // -> insert new_child between this and its children
-        for(child <- children){
-          if(child fitting_into new_child) {
+        for (child <- children) {
+          if (child fitting_into new_child) {
             new_child add child
           }
         }
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -1,5 +1,5 @@
 /*
- * Higher-level prover communication
+ * Higher-level prover communication: interactive document model
  *
  * @author Johannes Hölzl, TU Munich
  * @author Fabian Immler, TU Munich
@@ -9,40 +9,57 @@
 package isabelle.prover
 
 
-import scala.collection.mutable.{HashMap, HashSet}
+import scala.collection.mutable
 import scala.collection.immutable.{TreeSet}
 
 import org.gjt.sp.util.Log
 
+import isabelle.jedit.Isabelle
 import isabelle.proofdocument.{ProofDocument, Text, Token}
 import isabelle.IsarDocument
 
 
-class Prover(isabelle_system: IsabelleSystem)
+class Prover(isabelle_system: IsabelleSystem, logic: String)
 {
-  private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC")
+  /* prover process */
+
   private var process: Isar = null
 
-  private val commands = new HashMap[IsarDocument.Command_ID, Command]
+  {
+    val results = new EventBus[IsabelleProcess.Result] + handle_result
+    results.logger = Log.log(Log.ERROR, null, _)
+    process = new Isar(isabelle_system, results, "-m", "xsymbols", logic)
+  }
+
+  def stop() { process.kill }
 
+  
+  /* document state information */
 
+  private val states = new mutable.HashMap[IsarDocument.State_ID, Command]
+  private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command]
+  private val document0 = Isabelle.plugin.id()
+  private val document_versions = new mutable.HashSet[IsarDocument.Document_ID] + document0
+
+  private var initialized = false
+
+  
   /* outer syntax keywords */
 
   val decl_info = new EventBus[(String, String)]
 
-  private val keyword_decls = new HashSet[String] {
+  private val keyword_decls = new mutable.HashSet[String] {
     override def +=(name: String) = {
       decl_info.event(name, OuterKeyword.MINOR)
       super.+=(name)
     }
   }
-  private val command_decls = new HashMap[String, String] {
+  private val command_decls = new mutable.HashMap[String, String] {
     override def +=(entry: (String, String)) = {
       decl_info.event(entry)
       super.+=(entry)
     }
   }
-  def is_command_keyword(s: String): Boolean = command_decls.contains(s)
 
 
   /* completions */
@@ -51,9 +68,9 @@
   def completions = _completions
   /* // TODO: ask Makarius to make Interpretation.symbols public (here: read-only as 'symbol_map')
   val map = isabelle.jedit.Isabelle.symbols.symbol_map
-  for(xsymb <- map.keys) {
+  for (xsymb <- map.keys) {
     _completions += xsymb
-    if(map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
+    if (map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
   }
   */
   decl_info += (k_v => _completions += k_v._1)
@@ -61,8 +78,6 @@
 
   /* event handling */
 
-  private var initialized = false
-
   val activated = new EventBus[Unit]
   val command_info = new EventBus[Command]
   val output_info = new EventBus[String]
@@ -71,15 +86,20 @@
 
   def command_change(c: Command) = Swing.now { command_info.event(c) }
 
-  private def handle_result(r: IsabelleProcess.Result)
+  private def handle_result(result: IsabelleProcess.Result)
   {
-    val (id, st) = r.props.find(p => p._1 == Markup.ID) match
-      { case None => (null, null)
-        case Some((_, i)) => (i, commands.getOrElse(i, null)) }
+    val (running, command) =
+      result.props.find(p => p._1 == Markup.ID) match {
+        case None => (false, null)
+        case Some((_, id)) =>
+          if (commands.contains(id)) (false, commands(id))
+          else if (states.contains(id)) (true, states(id))
+          else (false, null)
+      }
 
-    if (r.kind == IsabelleProcess.Kind.STDOUT || r.kind == IsabelleProcess.Kind.STDIN)
-      Swing.now { output_info.event(r.result) }
-    else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
+    if (result.kind == IsabelleProcess.Kind.STDOUT || result.kind == IsabelleProcess.Kind.STDIN)
+      Swing.now { output_info.event(result.result) }
+    else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) {  // FIXME !?
       initialized = true
       Swing.now {
         if (document != null) {
@@ -89,97 +109,90 @@
       }
     }
     else {
-      if (st == null || (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)) {
-        r.kind match {
+      result.kind match {
+
+        case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
+          | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR
+        if command != null =>
+          if (result.kind == IsabelleProcess.Kind.ERROR)
+            command.status = Command.Status.FAILED
+          command.add_result(running, process.parse_message(result))
+          command_change(command)
 
-          case IsabelleProcess.Kind.STATUS =>
-            //{{{ handle all kinds of status messages here
-            val tree = process.parse_message(r)
-            tree match {
-              case XML.Elem(Markup.MESSAGE, _, elems) =>
-                for (elem <- elems) {
-                  elem match {
-                    //{{{
-                    // command status
-                    case XML.Elem(Markup.FINISHED, _, _) =>
-                      st.status = Command.Status.FINISHED
-                      command_change(st)
-                    case XML.Elem(Markup.UNPROCESSED, _, _) =>
-                      st.status = Command.Status.UNPROCESSED
-                      command_change(st)
-                    case XML.Elem(Markup.FAILED, _, _) =>
-                      st.status = Command.Status.FAILED
-                      command_change(st)
-                    case XML.Elem(Markup.DISPOSED, _, _) =>
-                      commands.removeKey(st.id)
-                      st.status = Command.Status.REMOVED
-                      command_change(st)
-
-                    // command and keyword declarations
-                    case XML.Elem(Markup.COMMAND_DECL,
-                        (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
-                      command_decls += (name -> kind)
-                    case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
-                      keyword_decls += name
+        case IsabelleProcess.Kind.STATUS =>
+          //{{{ handle all kinds of status messages here
+          process.parse_message(result) match {
+            case XML.Elem(Markup.MESSAGE, _, elems) =>
+              for (elem <- elems) {
+                elem match {
+                  //{{{
+                  // command and keyword declarations
+                  case XML.Elem(Markup.COMMAND_DECL,
+                      (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
+                    command_decls += (name -> kind)
+                  case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
+                    keyword_decls += name
 
-                    // other markup
-                    case XML.Elem(kind,
-                        (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) ::
-                             (Markup.ID, markup_id) :: _, _) =>
-                      val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
-                      val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1
+                  // document edits
+                  case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
+                  if document_versions.contains(doc_id) =>
+                    for {
+                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+                        <- edits
+                      if (commands.contains(cmd_id))
+                    } {
+                      val cmd = commands(cmd_id)
+                      if (cmd.state_id != null) states -= cmd.state_id
+                      states(cmd_id) = cmd
+                      cmd.state_id = state_id
+                      cmd.status = Command.Status.UNPROCESSED
+                      command_change(cmd)
+                    }
 
-                      val command =
-                        // outer syntax: no id in props
-                        if (st == null) commands.getOrElse(markup_id, null)
-                        // inner syntax: id from props
-                        else st
-                      command.root_node.insert(command.node_from(kind, begin, end))
+                  // command status
+                  case XML.Elem(Markup.UNPROCESSED, _, _)
+                  if command != null =>
+                    command.status = Command.Status.UNPROCESSED
+                    command_change(command)
+                  case XML.Elem(Markup.FINISHED, _, _)
+                  if command != null =>
+                    command.status = Command.Status.FINISHED
+                    command_change(command)
+                  case XML.Elem(Markup.FAILED, _, _)
+                  if command != null =>
+                    command.status = Command.Status.FAILED
+                    command_change(command)
 
-                    case _ =>
-                    //}}}
-                  }
+                  // other markup
+                  case XML.Elem(kind,
+                      (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) ::
+                           (Markup.ID, markup_id) :: _, _) =>
+                    val begin = offset.toInt - 1
+                    val end = end_offset.toInt - 1
+
+                    val cmd =  // FIXME proper command version!? running!?
+                      // outer syntax: no id in props
+                      if (command == null) commands.getOrElse(markup_id, null)
+                      // inner syntax: id from props
+                      else command
+                    if (cmd != null)
+                      cmd.root_node.insert(cmd.node_from(kind, begin, end))
+
+                  case _ =>
+                  //}}}
                 }
-              case _ =>
-            }
-            //}}}
+              }
+            case _ =>
+          }
+          //}}}
 
-          case IsabelleProcess.Kind.ERROR if st != null =>
-            val tree = process.parse_message(r)
-            if (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)
-              st.status = Command.Status.FAILED
-            st.add_result(tree)
-            command_change(st)
-
-          case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
-            | IsabelleProcess.Kind.WARNING if st != null =>
-            val tree = process.parse_message(r)
-            st.add_result(tree)
-            command_change(st)
-
-          case _ =>
-        }
+        case _ =>
       }
     }
   }
 
-
-  def start(logic: String) {
-    if (logic != null) _logic = logic
-
-    val results = new EventBus[IsabelleProcess.Result]
-    results += handle_result
-    results.logger = Log.log(Log.ERROR, null, _)
-
-    process = new Isar(isabelle_system, results, "-m", "xsymbols", _logic)
-  }
-
-  def stop() {
-    process.kill
-  }
-
   def set_document(text: Text, path: String) {
-    this.document = new ProofDocument(text, this)
+    this.document = new ProofDocument(text, command_decls.contains(_))
     process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
 
     document.structural_changes += (changes => {
@@ -202,7 +215,8 @@
   }
 
   def remove(cmd: Command) {
-    cmd.status = Command.Status.REMOVE
+    commands -= cmd.id
+    if (cmd.state_id != null) states -= cmd.state_id
     process.remove_command(cmd.id)
   }
 }
diff -r 6106e71c6ee5 -r 5839e34ef0bd src/Tools/jEdit/src/utils/Delay.scala
--- a/src/Tools/jEdit/src/utils/Delay.scala	Sat Jan 24 16:31:04 2009 +0100
+++ b/src/Tools/jEdit/src/utils/Delay.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -12,14 +12,14 @@
 class Delay(amount : Int, action : () => Unit) {
 
   val timer : Timer = new Timer(amount, new ActionListener {
-      override def actionPerformed(e:ActionEvent){
-        action ()
+      override def actionPerformed(e:ActionEvent) {
+        action()
       }
     })
   // if called very often, action is executed at most once
   // in amount milliseconds
-  def delay_or_ignore () = {
-    if (! timer.isRunning()){
+  def delay_or_ignore() = {
+    if (!timer.isRunning()) {
       timer.setRepeats(false)
       timer.start()
     }