# HG changeset patch
# User immler@in.tum.de
# Date 1237477709 -3600
# Node ID 5d88e0681d443909a7ae348c9c2dc30f27381a19
# Parent  20bfcca24658d1e81cf2dae00899bad93699a88e# Parent  b06946a1d4cbd0aafbe1c6f5100cb68d814ad0f4
merged; resolved conflicts (kept own versions)

diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/build.xml
--- a/src/Tools/jEdit/build.xml	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/build.xml	Thu Mar 19 16:48:29 2009 +0100
@@ -66,11 +66,16 @@
     nbproject/build-impl.xml file. 
 
     -->
+    <target name="run" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.run">
+    </target>
+    <target name="debug" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.debug">
+    </target>
     <target name="-pre-jar">
       <copy file="plugin/services.xml" todir="${build.classes.dir}" />
       <copy file="plugin/dockables.xml" todir="${build.classes.dir}" />
       <copy file="plugin/actions.xml" todir="${build.classes.dir}" />
       <copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
+      <copy file="plugin/styles.props" todir="${build.classes.dir}" />
     </target>
     <target name="-post-jar">
       <!-- jars -->
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/nbproject/build-impl.xml
--- a/src/Tools/jEdit/nbproject/build-impl.xml	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/nbproject/build-impl.xml	Thu Mar 19 16:48:29 2009 +0100
@@ -173,6 +173,9 @@
                 <javac debug="@{debug}" deprecation="${javac.deprecation}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includeantruntime="false" includes="@{includes}" source="${javac.source}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="${javac.target}">
                     <classpath>
                         <path path="@{classpath}"/>
+                        <fileset dir="${scala.lib}">
+                            <include name="**/*.jar"/>
+                        </fileset>
                     </classpath>
                     <compilerarg line="${javac.compilerargs} ${javac.compilerargs.jaxws}"/>
                     <customize/>
@@ -398,6 +401,7 @@
     </target>
     <target depends="init,deps-jar,-pre-pre-compile,-pre-compile,-compile-depend" if="have.sources" name="-do-compile">
         <scalaProject1:scalac/>
+        <scalaProject1:javac/>
         <copy todir="${build.classes.dir}">
             <fileset dir="${src.dir}" excludes="${build.classes.excludes},${excludes}" includes="${includes}"/>
         </copy>
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/nbproject/genfiles.properties
--- a/src/Tools/jEdit/nbproject/genfiles.properties	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/nbproject/genfiles.properties	Thu Mar 19 16:48:29 2009 +0100
@@ -4,5 +4,5 @@
 # This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
 # Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
 nbproject/build-impl.xml.data.CRC32=8f41dcce
-nbproject/build-impl.xml.script.CRC32=828f71d1
-nbproject/build-impl.xml.stylesheet.CRC32=2aa5193a
+nbproject/build-impl.xml.script.CRC32=87cef431
+nbproject/build-impl.xml.stylesheet.CRC32=371897b9
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/plugin/styles.props
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/styles.props	Thu Mar 19 16:48:29 2009 +0100
@@ -0,0 +1,11 @@
+#syntax styles
+options.isabelle.styles.command.foreground=#000080
+options.isabelle.styles.keyword.foreground=#008000
+options.isabelle.styles.fixed_decl.foreground=#080808
+options.isabelle.styles.local_fact_decl.foreground=#080808
+options.isabelle.styles.fact.foreground=#080808
+options.isabelle.styles.method.foreground=#101010
+options.isabelle.styles.literal.foreground=#808000
+options.isabelle.styles.ident.foreground=#C0C000
+options.isabelle.styles.doc_source.foreground=#C00000
+options.isabelle.styles.ML_source.foreground=#C00000
\ No newline at end of file
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -7,8 +7,7 @@
 
 package isabelle.jedit
 
-import isabelle.proofdocument.ProofDocument
-import isabelle.prover.{Command, MarkupNode}
+import isabelle.prover.{Command, MarkupNode, Prover}
 import isabelle.Markup
 
 import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -20,59 +19,55 @@
 
 object DynamicTokenMarker {
 
-  def styles: Array[SyntaxStyle] = {
-    val array = new Array[SyntaxStyle](256)
-    // array(0) won't be used: reserved for global default-font
-    array(1) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
-    array(2) = new SyntaxStyle(new Color(255, 0, 255), Color.white, Isabelle.plugin.font)
-    array(3) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
-    array(4) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font)
-    array(5) = new SyntaxStyle(new Color(255, 128, 128), Color.white,Isabelle.plugin.font)
-    array(6) = new SyntaxStyle(Color.yellow, Color.white, Isabelle.plugin.font)
-    array(7) = new SyntaxStyle( new Color(0, 192, 0), Color.white, Isabelle.plugin.font)
-    array(8) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
-    array(9) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font)
-    array(10) = new SyntaxStyle(Color.gray, Color.white, Isabelle.plugin.font)
-    array(11) = new SyntaxStyle(Color.white, Color.white, Isabelle.plugin.font)
-    array(12) = new SyntaxStyle(Color.red, Color.white, Isabelle.plugin.font)
-    array(13) = new SyntaxStyle(Color.orange, Color.white, Isabelle.plugin.font)
-    return array
+  var styles : Array[SyntaxStyle] = null
+  def reload_styles: Array[SyntaxStyle] = {
+    styles = new Array[SyntaxStyle](256)
+    //jEdit styles
+    for(i <- 0 to Token.ID_COUNT) styles(i) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
+    //isabelle styles
+    def from_property(kind : String, spec : String, default : Color) : Color = 
+      try {Color.decode(Isabelle.Property("styles." + kind + "." + spec))} catch {case _ => default}
+
+    for((kind, i) <- kinds) styles(i + FIRST_BYTE) = new SyntaxStyle(
+      from_property(kind, "foreground", Color.black),
+      from_property(kind, "background", Color.white),
+      Isabelle.plugin.font)
+    return styles
   }
 
-  def choose_byte(kind: String): Byte = {
-    // TODO: as properties
-    kind match {
-      // logical entities
-      case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
-        | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
-        | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => 2
-      // inner syntax
-      case Markup.TFREE | Markup.FREE => 3
-      case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => 4
-      case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
-        | Markup.INNER_COMMENT => 5
-      case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
-        | Markup.ATTRIBUTE | Markup.METHOD => 6
-      // embedded source text
-      case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
-        | Markup.DOC_ANTIQ => 7
-      // outer syntax
-      case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => 8
-      case Markup.VERBATIM => 9
-      case Markup.COMMENT => 10
-      case Markup.CONTROL => 11
-      case Markup.MALFORMED => 12
-      case Markup.STRING | Markup.ALTSTRING => 13
-      // other
-      case _ => 1
-    }
+  private final val FIRST_BYTE : Byte = 30
+  val kinds = List(// TODO Markups as Enumeration?
+     // default style
+    null,
+    // logical entities
+    Markup.TCLASS, Markup.TYCON, Markup.FIXED_DECL, Markup.FIXED, Markup.CONST_DECL,
+    Markup.CONST, Markup.FACT_DECL, Markup.FACT, Markup.DYNAMIC_FACT,
+    Markup.LOCAL_FACT_DECL, Markup.LOCAL_FACT,
+    // inner syntax
+    Markup.TFREE, Markup.FREE,
+    Markup.TVAR, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
+    Markup.NUM, Markup.FLOAT, Markup.XNUM, Markup.XSTR, Markup.LITERAL,
+    Markup.INNER_COMMENT,
+    Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP,
+    Markup.ATTRIBUTE, Markup.METHOD,
+    // embedded source text
+    Markup.ML_SOURCE, Markup.DOC_SOURCE, Markup.ANTIQ, Markup.ML_ANTIQ,
+    Markup.DOC_ANTIQ,
+    // outer syntax
+    Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT,
+    Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING
+  ).zipWithIndex
+
+  def choose_byte(kind : String) : Byte = (kinds.find (k => kind == k._1)) match {
+    case Some((kind, index)) => (index + FIRST_BYTE).asInstanceOf[Byte]
+    case _ => FIRST_BYTE
   }
 
   def choose_color(kind : String) : Color = styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
 
 }
 
-class DynamicTokenMarker(buffer: JEditBuffer, document: ProofDocument) extends TokenMarker {
+class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker {
 
   override def markTokens(prev: TokenMarker.LineContext,
     handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
@@ -85,30 +80,25 @@
     def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
     def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
 
-    val commands = document.commands.dropWhile(_.stop <= from(start))
-    if(commands.hasNext) {
-      var next_x = start
-      for {
-        command <- commands.takeWhile(_.start < from(stop))
-        markup <- command.root_node.flatten
-        if(to(markup.abs_stop) > start)
-        if(to(markup.abs_start) < stop)
-        byte = DynamicTokenMarker.choose_byte(markup.kind)
-        token_start = to(markup.abs_start) - start max 0
-        token_length = to(markup.abs_stop) - to(markup.abs_start) -
-                       (start - to(markup.abs_start) max 0) -
-                       (to(markup.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
-      }
-      if (next_x < stop)
-        handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
-    } else {
-      handler.handleToken(line_segment, 1, 0, line_segment.count, context)
+    var next_x = start
+    for {
+      command <- prover.document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
+      markup <- command.root_node.flatten
+      if(to(markup.abs_stop) > start)
+      if(to(markup.abs_start) < stop)
+      byte = DynamicTokenMarker.choose_byte(markup.kind)
+      token_start = to(markup.abs_start) - start max 0
+      token_length = to(markup.abs_stop) - to(markup.abs_start) -
+                     (start - to(markup.abs_start) max 0) -
+                     (to(markup.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
     }
+    if (next_x < stop)
+      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
 
     handler.handleToken(line_segment,Token.END, line_segment.count, 0, context)
     handler.setLineContext(context)
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -32,10 +32,9 @@
     val prover_setup = Isabelle.plugin.prover_setup(buffer)
     if (prover_setup.isDefined) {
         val document = prover_setup.get.prover.document
-        val commands = document.commands
-        while (!stopped && commands.hasNext) {
-          data.root.add(commands.next.root_node.swing_node)
-        }
+        for (command <- document.commands)
+          data.root.add(command.root_node.swing_node)
+        
         if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
     } else {
       data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
@@ -51,7 +50,7 @@
   override def canCompleteAnywhere = true
   override def getInstantCompletionTriggers = "\\"
 
-  override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
+  override def complete(pane: EditPane, caret: Int): SideKickCompletion = null /*{
     val buffer = pane.getBuffer
     val ps = Isabelle.prover_setup(buffer)
     if (ps.isDefined) {
@@ -83,7 +82,7 @@
       }
       return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
     } else return null
-  }
+  }*/
 
 }
 
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -24,7 +24,6 @@
   var textarea : JEditTextArea = null
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
-  prover.command_info += (_ => repaint_delay.delay_or_ignore())
 
   setRequestFocusEnabled(false);
 
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -10,7 +10,6 @@
 import isabelle.prover.{Prover, Command}
 import isabelle.renderer.UserAgent
 
-
 import org.w3c.dom.Document
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, View}
@@ -35,12 +34,12 @@
 
   def activate(view: View) {
     prover = new Prover(Isabelle.system, Isabelle.default_logic)
-
+    prover.start() //start actor
     val buffer = view.getBuffer
     val path = buffer.getPath
 
-    theory_view = new TheoryView(view.getTextArea)
-    prover.set_document(theory_view,
+    theory_view = new TheoryView(view.getTextArea, prover)
+    prover.set_document(theory_view.change_receiver,
       if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path)
     theory_view.activate
 
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -8,6 +8,7 @@
 
 package isabelle.jedit
 
+import scala.actors.Actor
 
 import isabelle.proofdocument.Text
 import isabelle.prover.{Prover, Command}
@@ -38,15 +39,15 @@
 }
 
 
-class TheoryView (text_area: JEditTextArea)
-    extends TextAreaExtension with Text with BufferListener {
+class TheoryView (text_area: JEditTextArea, document_actor: Actor)
+    extends TextAreaExtension with BufferListener {
 
   private val buffer = text_area.getBuffer
   private val prover = Isabelle.prover_setup(buffer).get.prover
   buffer.addBufferListener(this)
 
 
-  private var col: Text.Changed = null
+  private var col: Text.Change = null
 
   private val col_timer = new Timer(300, new ActionListener() {
     override def actionPerformed(e: ActionEvent) = commit
@@ -66,7 +67,7 @@
   private def update_styles = {
     if (text_area != null) {
       if (Isabelle.plugin.font != null) {
-        text_area.getPainter.setStyles(DynamicTokenMarker.styles)
+        text_area.getPainter.setStyles(DynamicTokenMarker.reload_styles)
         repaint_all
       }
     }
@@ -86,8 +87,9 @@
     phase_overview.textarea = text_area
     text_area.addLeftOfScrollBar(phase_overview)
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
-    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
+    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
     update_styles
+    document_actor ! new Text.Change(0,buffer.getText(0, buffer.getLength),0)
   }
 
   def deactivate() = {
@@ -100,18 +102,28 @@
   /* painting */
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
-  prover.command_info += (_ => repaint_delay.delay_or_ignore())
+  
+  val change_receiver = scala.actors.Actor.actor {
+    scala.actors.Actor.loop {
+      scala.actors.Actor.react {
+        case _ => {
+            repaint_delay.delay_or_ignore()
+            phase_overview.repaint_delay.delay_or_ignore()
+        }
+      }
+    }
+  }.start
 
   def from_current (pos: Int) =
     if (col != null && col.start <= pos)
-      if (pos < col.start + col.added) col.start
-      else pos - col.added + col.removed
+      if (pos < col.start + col.added.length) col.start
+      else pos - col.added.length + col.removed
     else pos
 
   def to_current (pos : Int) =
     if (col != null && col.start <= pos)
       if (pos < col.start + col.removed) col.start
-      else pos + col.added - col.removed
+      else pos + col.added.length - col.removed
     else pos
 
   def repaint(cmd: Command) =
@@ -162,9 +174,10 @@
 
     val metrics = text_area.getPainter.getFontMetrics
     var e = prover.document.find_command_at(from_current(start))
-
+    val commands = prover.document.commands.dropWhile(_.stop <= from_current(start)).
+      takeWhile(c => to_current(c.start) < end)
     // encolor phase
-    while (e != null && to_current(e.start) < end) {
+    for (e <- commands) {
       val begin = start max to_current(e.start)
       val finish = end - 1 min to_current(e.stop)
       encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
@@ -178,25 +191,16 @@
             DynamicTokenMarker.choose_color(node.kind), true)
         }
       }
-      e = e.next
     }
 
     gfx.setColor(saved_color)
   }
 
-
-  /* Text methods */
-
-  def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
-  def length = buffer.getLength
-  val changes = new EventBus[Text.Changed]
-
-
   /* BufferListener methods */
 
   private def commit {
     if (col != null)
-      changes.event(col)
+      document_actor ! col
     col = null
     if (col_timer.isRunning())
       col_timer.stop()
@@ -211,51 +215,50 @@
 
 
   override def contentInserted(buffer: JEditBuffer,
-    start_line: Int, offset: Int, num_lines: Int, length: Int)
+    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+  override def contentRemoved(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+  override def preContentInserted(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) =
   {
-/*
+    val text = buffer.getText(offset, length)
     if (col == null)
-      col = new Text.Changed(offset, length, 0)
-    else if (col.start <= offset && offset <= col.start + col.added)
-      col = new Text.Changed(col.start, col.added + length, col.removed)
+      col = new Text.Change(offset, text, 0)
+    else if (col.start <= offset && offset <= col.start + col.added.length)
+      col = new Text.Change(col.start, col.added + text, col.removed)
     else {
       commit
-      col = new Text.Changed(offset, length, 0)
+      col = new Text.Change(offset, text, 0)
     }
     delay_commit
-*/
-    changes.event(new Text.Changed(offset, length, 0))
   }
 
   override def preContentRemoved(buffer: JEditBuffer,
     start_line: Int, start: Int, num_lines: Int, removed: Int) =
   {
-/*
     if (col == null)
-      col = new Text.Changed(start, 0, removed)
-    else if (col.start > start + removed || start > col.start + col.added) {
+      col = new Text.Change(start, "", removed)
+    else if (col.start > start + removed || start > col.start + col.added.length) {
       commit
-      col = new Text.Changed(start, 0, removed)
+      col = new Text.Change(start, "", removed)
     }
     else {
-      val offset = start - col.start
-      val diff = col.added - removed
+/*      val offset = start - col.start
+      val diff = col.added.length - removed
       val (added, add_removed) =
         if (diff < offset)
           (offset max 0, diff - (offset max 0))
         else
           (diff - (offset min 0), offset min 0)
-      col = new Text.Changed(start min col.start, added, col.removed - add_removed)
+      col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
+      commit
+      col = new Text.Change(start, "", removed)
     }
     delay_commit
-*/
-    changes.event(new Text.Changed(start, 0, removed))
   }
 
-  override def contentRemoved(buffer: JEditBuffer,
-    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-  override def preContentInserted(buffer: JEditBuffer,
-    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
   override def bufferLoaded(buffer: JEditBuffer) { }
   override def foldHandlerChanged(buffer: JEditBuffer) { }
   override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -2,18 +2,21 @@
  * Document as list of commands, consisting of lists of tokens
  *
  * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
  * @author Makarius
  */
 
 package isabelle.proofdocument
 
-
+import scala.collection.mutable.ListBuffer
+import scala.actors.Actor
+import scala.actors.Actor._
 import java.util.regex.Pattern
 import isabelle.prover.{Prover, Command}
-
+import isabelle.utils.LinearSet
 
 case class StructureChange(
-  val before_change: Command,
+  val before_change: Option[Command],
   val added_commands: List[Command],
   val removed_commands: List[Command])
 
@@ -35,73 +38,52 @@
       "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
       "[()\\[\\]{}:;]", Pattern.MULTILINE)
 
+ val empty = new ProofDocument(LinearSet.empty, LinearSet.empty, false, _ => false)
+
 }
 
-class ProofDocument(text: Text, is_command_keyword: String => Boolean)
+class ProofDocument(val tokens: LinearSet[Token],
+                    val commands: LinearSet[Command],
+                    val active: Boolean,
+                    is_command_keyword: String => Boolean)
 {
-  private var active = false 
-  def activate() {
-    if (!active) {
-      active = true
-      text_changed(0, text.length, 0)
-    }
+
+  def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword)
+  def activate: (ProofDocument, StructureChange) = {
+    val (doc, change) = text_changed(new Text.Change(0, content, content.length))
+    return (doc.mark_active, change)
   }
-
-  text.changes += (changed => text_changed(changed.start, changed.added, changed.removed))
+  def set_command_keyword(f: String => Boolean): ProofDocument =
+    new ProofDocument(tokens, commands, active, f)
 
-
-
+  def content = Token.string_from_tokens(List() ++ tokens)
   /** token view **/
 
-  private var first_token: Token = null
-  private var last_token: Token = null
-  
-  private def tokens(start: Token, stop: Token) = new Iterator[Token] {
-      var current = start
-      def hasNext = current != stop && current != null
-      def next() = { val save = current; current = current.next; save }
-    }
-  private def tokens(start: Token): Iterator[Token] = tokens(start, null)
-  private def tokens(): Iterator[Token] = tokens(first_token, null)
-
-
-  private def text_changed(start: Int, added_len: Int, removed_len: Int)
+  def text_changed(change: Text.Change): (ProofDocument, StructureChange) =
   {
-    if (!active)
-      return
+    val tokens = List() ++ this.tokens
+    val (begin, remaining) = tokens.span(_.stop < change.start)
+    val (removed, end_unshifted) = remaining.span(_.start <= change.start + change.removed)
+    val end = for (t <- end_unshifted) yield t.shift(change.added.length - change.removed)
 
-    var before_change =
-      if (Token.check_stop(first_token, _ < start)) Token.scan(first_token, _.stop >= start)
-      else null
-    
-    var first_removed =
-      if (before_change != null) before_change.next
-      else if (Token.check_start(first_token, _ <= start + removed_len)) first_token
-      else null 
-
-    var last_removed = Token.scan(first_removed, _.start > start + removed_len)
+    val split_begin = removed.takeWhile(_.start < change.start).
+      map (t => new Token(t.start,
+                          t.content.substring(0, change.start - t.start),
+                          t.kind))
+    val split_end = removed.dropWhile(_.stop < change.start + change.removed).
+      map (t => new Token(change.start + change.added.length,
+                          t.content.substring(change.start + change.removed - t.start),
+                          t.kind))
 
-    var shift_token =
-      if (last_removed != null) last_removed
-      else if (Token.check_start(first_token, _ > start)) first_token
-      else null
-    
-    while (shift_token != null) {
-      shift_token.shift(added_len - removed_len, start)
-      shift_token = shift_token.next
-    }
-    
-    // scan changed tokens until the end of the text or a matching token is
-    // found which is beyond the changed area
-    val match_start = if (before_change == null) 0 else before_change.stop
-    var first_added: Token = null
-    var last_added: Token = null
+    var invalid_tokens =  split_begin :::
+      new Token(change.start, change.added, Token.Kind.OTHER) :: split_end ::: end
+    var new_tokens = Nil: List[Token]
+    var old_suffix = Nil: List[Token]
 
-    val matcher = ProofDocument.token_pattern.matcher(text.content(match_start, text.length))
-    var finished = false
-    var position = 0 
-    while (matcher.find(position) && !finished) {
-      position = matcher.end
+    val match_start = invalid_tokens.first.start
+    val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens))
+
+    while (matcher.find() && invalid_tokens != Nil) {
 			val kind =
         if (is_command_keyword(matcher.group))
           Token.Kind.COMMAND_START
@@ -109,252 +91,87 @@
           Token.Kind.COMMENT
         else
           Token.Kind.OTHER
-      val new_token = new Token(matcher.start + match_start, matcher.end + match_start, kind)
-
-      if (first_added == null)
-        first_added = new_token
-      else {
-        new_token.prev = last_added
-        last_added.next = new_token
-      }
-      last_added = new_token
-      
-      while (Token.check_stop(last_removed, _ < new_token.stop) &&
-              last_removed.next != null)
-        last_removed = last_removed.next
-			
-      if (new_token.stop >= start + added_len &&
-            Token.check_stop(last_removed, _ == new_token.stop))
-        finished = true
-    }
+      val new_token = new Token(match_start + matcher.start, matcher.group, kind)
+      new_tokens ::= new_token
 
-    var after_change = if (last_removed != null) last_removed.next else null
-		
-    // remove superflous first token-change
-    if (first_added != null && first_added == first_removed &&
-          first_added.stop < start) {
-      before_change = first_removed
-      if (last_removed == first_removed) {
-        last_removed = null
-        first_removed = null
-      }
-      else {
-        first_removed = first_removed.next
-        assert(first_removed != null)
-      }
-
-      if (last_added == first_added) {
-        last_added = null
-        first_added = null
-      }
-      if (first_added != null)
-        first_added = first_added.next
-    }
-    
-    // remove superflous last token-change
-    if (last_added != null && last_added == last_removed &&
-          last_added.start > start + added_len) {
-      after_change = last_removed
-      if (first_removed == last_removed) {
-        first_removed = null
-        last_removed = null
-      }
-      else {
-        last_removed = last_removed.prev
-        assert(last_removed != null)
+      invalid_tokens = invalid_tokens dropWhile (_.stop < new_token.stop)
+      invalid_tokens match {
+        case t::ts => if(t.start == new_token.start &&
+                         t.start > change.start + change.added.length) {
+          old_suffix = ts
+          invalid_tokens = Nil
+        }
+        case _ =>
       }
-      
-      if (last_added == first_added) {
-        last_added = null
-        first_added = null
-      }
-      else
-        last_added = last_added.prev
     }
-    
-    if (first_removed == null && first_added == null)
-      return
-    
-    if (first_token == null) {
-      first_token = first_added
-      last_token = last_added
-    }
-    else {
-      // cut removed tokens out of list
-      if (first_removed != null)
-        first_removed.prev = null
-      if (last_removed != null)
-        last_removed.next = null
-      
-      if (first_token == first_removed)
-        if (first_added != null)
-          first_token = first_added
-        else
-          first_token = after_change
-      
-      if (last_token == last_removed)
-        if (last_added != null)
-          last_token = last_added
-        else
-          last_token = before_change
-      
-      // insert new tokens into list
-      if (first_added != null) {
-        first_added.prev = before_change
-        if (before_change != null)
-          before_change.next = first_added
-        else
-          first_token = first_added
-      }
-      else if (before_change != null)
-        before_change.next = after_change
-      
-      if (last_added != null) {
-        last_added.next = after_change
-        if (after_change != null)
-          after_change.prev = last_added
-        else
-          last_token = last_added
-      }
-      else if (after_change != null)
-        after_change.prev = before_change
-    }
+    val insert = new_tokens.reverse
+    val new_tokenset = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]]
 
-    System.err.println("token_changed: " + before_change + " " + after_change + " " + first_removed)
-    token_changed(before_change, after_change, first_removed)
+    token_changed(begin.lastOption,
+                  insert,
+                  removed,
+                  new_tokenset,
+                  old_suffix.firstOption)
   }
   
-
-  
   /** command view **/
 
-  val structural_changes = new EventBus[StructureChange]
-
-  def commands_from(start: Token) = new Iterator[Command] {
-    var current = start
-    def hasNext = current != null
-    def next = { val s = current.command ; current = s.last.next ; s }
-  }
-  def commands_from(start: Command): Iterator[Command] = commands_from(start.first)
-  def commands = commands_from(first_token)
-
   def find_command_at(pos: Int): Command = {
     for (cmd <- commands) { if (pos < cmd.stop) return cmd }
     return null
   }
 
-  private def token_changed(start: Token, stop: Token, removed: Token)
+  private def token_changed(before_change: Option[Token],
+                            inserted_tokens: List[Token],
+                            removed_tokens: List[Token],
+                            new_tokenset: LinearSet[Token],
+                            after_change: Option[Token]): (ProofDocument, StructureChange) =
   {
-    var removed_commands: List[Command] = Nil
-    var first: Command = null
-    var last: Command = null
-
-    for (t <- tokens(removed)) {
-      if (first == null)
-        first = t.command
-      if (t.command != last)
-        removed_commands = t.command :: removed_commands
-      last = t.command
+    val commands = List() ++ this.commands
+    val (begin, remaining) =
+      before_change match {
+        case None => (Nil, commands)
+        case Some(bc) => commands.break(_.tokens.contains(bc))
+      }
+    val (_removed, _end) =
+      after_change match {
+        case None => (remaining, Nil)
+        case Some(ac) => remaining.break(_.tokens.contains(ac))
+      }
+    val (removed, end) = _end match {
+      case Nil => (_removed, Nil)
+      case acc::end => if (after_change.isDefined && after_change.get.kind == Token.Kind.COMMAND_START)
+          (_removed, _end)
+        else (_removed ::: List(acc), end)
     }
-
-    var before: Command = null
-    if (!removed_commands.isEmpty) {
-      if (first.first == removed) {
-        if (start == null)
-          before = null
-        else
-          before = start.command
+    val all_removed_tokens = for(c <- removed; t <- c.tokens) yield t
+    val (pseudo_new_pre, rest) =
+      if (! before_change.isDefined) (Nil, all_removed_tokens)
+      else {
+        val (a, b) = all_removed_tokens.span (_ != before_change.get)
+        b match {
+          case Nil => (a, Nil)
+          case bc::rest => (a ::: List(bc), b)
+        }
       }
-      else
-        before = first.prev
-    }
+    val pseudo_new_post = rest.dropWhile(Some(_) != after_change)
 
-    var added_commands: List[Command] = Nil
-    var scan: Token = null
-    if (start != null) {
-      val next = start.next
-      if (first != null && first.first != removed) {
-        scan = first.first
-        if (before == null)
-          before = first.prev
-      }
-      else if (next != null && next != stop) {
-        if (next.kind == Token.Kind.COMMAND_START) {
-          before = start.command
-          scan = next
-        }
-        else if (first == null || first.first == removed) {
-          first = start.command
-          removed_commands = first :: removed_commands
-          scan = first.first
-          if (before == null)
-            before = first.prev
-        }
-        else {
-          scan = first.first
-          if (before == null)
-            before = first.prev
-        }
+    def tokens_to_commands(tokens: List[Token]): List[Command]= {
+      tokens match {
+        case Nil => Nil
+        case t::ts =>
+          val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
+          new Command(t::cmd) :: tokens_to_commands (rest)
       }
     }
-    else
-      scan = first_token
 
-    var stop_scan: Token = null
-    if (stop != null) {
-      if (stop == stop.command.first)
-        stop_scan = stop
-      else
-        stop_scan = stop.command.last.next
-    }
-    else if (last != null)
-      stop_scan = last.last.next
-    else
-      stop_scan = null
-
-    var cmd_start: Token = null
-    var cmd_stop: Token = null
-    var overrun = false
-    var finished = false
-    while (scan != null && !finished) {
-      if (scan == stop_scan) {
-        if (scan.kind == Token.Kind.COMMAND_START)
-          finished = true
-        else
-          overrun = true
-      }
+    val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
 
-      if (scan.kind == Token.Kind.COMMAND_START && cmd_start != null && !finished) {
-        if (!overrun) {
-          added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
-          cmd_start = scan
-          cmd_stop = scan
-        }
-        else
-          finished = true
-      }
-      else if (!finished) {
-        if (cmd_start == null)
-          cmd_start = scan
-        cmd_stop = scan
-      }
-      if (overrun && !finished) {
-        if (scan.command != last)
-          removed_commands = scan.command :: removed_commands
-        last = scan.command
-      }
+    val new_commandset = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
+    val before = begin match {case Nil => None case _ => Some (begin.last)}
 
-      if (!finished)
-        scan = scan.next
-    }
-
-    if (cmd_start != null)
-      added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
-
-    // relink commands
-    added_commands = added_commands.reverse
-    removed_commands = removed_commands.reverse
-
-    structural_changes.event(new StructureChange(before, added_commands, removed_commands))
+    val change = new StructureChange(before, new_commands, removed)
+    val doc = new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword)
+    return (doc, change)
   }
 }
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/proofdocument/Text.scala
--- a/src/Tools/jEdit/src/proofdocument/Text.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -8,11 +8,7 @@
 
 
 object Text {
-  case class Changed(val start: Int, val added: Int, val removed: Int)
-}
-
-trait Text {
-  def content(start: Int, stop: Int): String
-  def length: Int
-  def changes: EventBus[Text.Changed]
-}
+  case class Change(start: Int, val added: String, val removed: Int) {
+    override def toString = "start: " + start + " added: " + added + " removed: " + removed
+  }
+}
\ No newline at end of file
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -18,44 +18,30 @@
     val OTHER = Value("OTHER")
   }
 
-  def check_start(t: Token, P: Int => Boolean) = { t != null && P(t.start) }
-  def check_stop(t: Token, P: Int => Boolean) = { t != null && P(t.stop) }
+  def check_start(t: Token, P: Int => Boolean) = t != null && P(t.start)
+  def check_stop(t: Token, P: Int => Boolean) = t != null && P(t.stop)
 
-  def scan(s: Token, f: Token => Boolean): Token =
-  {
-    var current = s
-    while (current != null) {
-      val next = current.next
-      if (next == null || f(next)) return current
-      current = next
+  private def fill(n: Int) = {
+    val blanks = new Array[Char](n)
+    for(i <- 0 to n - 1) blanks(i) = ' '
+    new String(blanks)
+  }
+  def string_from_tokens (tokens: List[Token]): String = {
+    tokens match {
+      case Nil => ""
+      case t::tokens => (tokens.foldLeft
+          (t.content, t.stop)
+          ((a, token) => (a._1 + fill(token.start - a._2) + token.content, token.stop))
+        )._1
     }
-    return null
   }
+
 }
 
-class Token(var start: Int, var stop: Int, val kind: Token.Kind.Value)
-{
-  var next: Token = null
-  var prev: Token = null
-  var command: Command = null
-  
-  def length = stop - start
-
-  def shift(offset: Int, bottom_clamp: Int) {
-    start = bottom_clamp max (start + offset)
-    stop = bottom_clamp max (stop + offset)
-  }
-
-  override def toString: String = "[" + start + ":" + stop + "]"
+class Token(val start: Int, val content: String, val kind: Token.Kind.Value) {
+  val length = content.length
+  val stop = start + length
+  override def toString = content + "(" + kind + ")"
   override def hashCode: Int = (31 + start) * 31 + stop
-
-  override def equals(obj: Any): Boolean =
-  {
-    if (super.equals(obj)) return true
-    if (null == obj) return false
-    obj match {
-      case other: Token => (start == other.start) && (stop == other.stop)
-      case other: Any => false
-    }
-  }
+  def shift(i: Int) = new Token(start + i, content, kind)
 }
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -29,40 +29,19 @@
 }
 
 
-class Command(text: Text, val first: Token, val last: Token)
+class Command(val tokens: List[Token])
 {
   val id = Isabelle.plugin.id()
 
-
   /* content */
 
-  {
-    var t = first
-    while (t != null) {
-      t.command = this
-      t = if (t == last) null else t.next
-    }
-  }
-
   override def toString = name
 
-  val name = text.content(first.start, first.stop)
-  val content = text.content(proper_start, proper_stop)
-
-  def next = if (last.next != null) last.next.command else null
-  def prev = if (first.prev != null) first.prev.command else null
-
-  def start = first.start
-  def stop = last.stop
+  val name = tokens.head.content
+  val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT))
 
-  def proper_start = start
-  def proper_stop = {
-    var i = last
-    while (i != first && i.kind == Token.Kind.COMMENT)
-      i = i.prev
-    i.stop
-  }
-
+  def start = tokens.first.start
+  def stop = tokens.last.stop
 
   /* command status */
 
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -12,17 +12,26 @@
 import scala.collection.mutable
 import scala.collection.immutable.{TreeSet}
 
+import scala.actors.Actor
+import scala.actors.Actor._
+
 import org.gjt.sp.util.Log
 
 import isabelle.jedit.Isabelle
 import isabelle.proofdocument.{StructureChange, ProofDocument, Text, Token}
 import isabelle.IsarDocument
 
+object ProverEvents {
+  case class Activate
+  case class SetEventBus(bus: EventBus[StructureChange])
+  case class SetIsCommandKeyword(is_command_keyword: String => Boolean)
+}
 
-class Prover(isabelle_system: IsabelleSystem, logic: String)
+class Prover(isabelle_system: IsabelleSystem, logic: String) extends Actor
 {
   /* prover process */
 
+
   private val process =
   {
     val results = new EventBus[IsabelleProcess.Result] + handle_result
@@ -40,8 +49,10 @@
   private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
     mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
   private val document_id0 = Isabelle.plugin.id()
-  private var document_id = document_id0
-  private var document_versions = Set(document_id)
+  private var document_versions = List((document_id0, ProofDocument.empty))
+
+  def document_id = document_versions.head._1
+  def document = document_versions.head._2
 
   private var initialized = false
 
@@ -83,14 +94,12 @@
   /* event handling */
 
   val activated = new EventBus[Unit]
-  val command_info = new EventBus[Command]
   val output_info = new EventBus[String]
-  var document: ProofDocument = null
-
-
-  private def handle_result(result: IsabelleProcess.Result): Unit = Swing.now
+  var change_receiver = null: Actor
+  
+  private def handle_result(result: IsabelleProcess.Result)
   {
-    def command_change(c: Command) = command_info.event(c)
+    def command_change(c: Command) = this ! c
     val (running, command) =
       result.props.find(p => p._1 == Markup.ID) match {
         case None => (false, null)
@@ -104,21 +113,21 @@
       output_info.event(result.toString)
     else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) {  // FIXME !?
       initialized = true
-      if (document != null) {
-        document.activate()
-        activated.event(())
-      }
+      Swing.now { this ! ProverEvents.Activate }
     }
     else {
       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)
+          | 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)
+          } else {
+            output_info.event(result.toString)
+          }
 
         case IsabelleProcess.Kind.STATUS =>
           //{{{ handle all kinds of status messages here
@@ -145,13 +154,13 @@
                       if (commands.contains(cmd_id)) {
                         val cmd = commands(cmd_id)
                         if (cmd.state_id != null) states -= cmd.state_id
-                        states(state_id) = cmd
+                        states(cmd_id) = cmd
                         cmd.state_id = state_id
                         cmd.status = Command.Status.UNPROCESSED
                         command_change(cmd)
                       }
+
                     }
-
                   // command status
                   case XML.Elem(Markup.UNPROCESSED, _, _)
                   if command != null =>
@@ -181,9 +190,10 @@
                       if (command == null) commands.getOrElse(markup_id, null)
                       // inner syntax: id from props
                       else command
-                    if (cmd != null)
+                    if (cmd != null) {
                       cmd.root_node.insert(cmd.node_from(kind, begin, end))
-
+                      command_change(cmd)
+                    }
                   case _ =>
                   //}}}
                 }
@@ -197,36 +207,58 @@
     }
   }
 
-  def set_document(text: Text, path: String): Unit = Swing.now
-  {
-    document = new ProofDocument(text, command_decls.contains(_))
+  def act() {
+    import ProverEvents._
+    loop {
+      react {
+        case Activate => {
+            val (doc, structure_change) = document.activate
+            val old_id = document_id
+            val doc_id = Isabelle.plugin.id()
+            document_versions ::= (doc_id, doc)
+            edit_document(old_id, doc_id, structure_change)
+        }
+        case SetIsCommandKeyword(f) => {
+            val old_id = document_id
+            val doc_id = Isabelle.plugin.id()
+            document_versions ::= (doc_id, document.set_command_keyword(f))
+            edit_document(old_id, doc_id, StructureChange(None, Nil, Nil))
+        }
+        case change: Text.Change => {
+            val (doc, structure_change) = document.text_changed(change)
+            val old_id = document_id
+            val doc_id = Isabelle.plugin.id()
+            document_versions ::= (doc_id, doc)
+            edit_document(old_id, doc_id, structure_change)
+        }
+        case command: Command => {
+            //state of command has changed
+            change_receiver ! command
+        }
+      }
+    }
+  }
+  
+  def set_document(change_receiver: Actor, path: String) {
+    this.change_receiver = change_receiver
+    this ! ProverEvents.SetIsCommandKeyword(command_decls.contains)
     process.ML("()")  // FIXME force initial writeln
     process.begin_document(document_id0, path)
-    document.structural_changes += edit_document
-    // FIXME !?
-    if (initialized) {
-      document.activate()
-      activated.event(())
-    }
   }
 
-  private def edit_document(changes: StructureChange) = Swing.now
+  private def edit_document(old_id: String, document_id: String, changes: StructureChange) = Swing.now
   {
-    val old_id = document_id
-    document_id = Isabelle.plugin.id()
-    document_versions += document_id
-
     val removes =
       for (cmd <- changes.removed_commands) yield {
         commands -= cmd.id
         if (cmd.state_id != null) states -= cmd.state_id
-        (if (cmd.prev == null) document_id0 else cmd.prev.id) -> None
+        (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> None
       }
     val inserts =
       for (cmd <- changes.added_commands) yield {
         commands += (cmd.id -> cmd)
         process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
-        (if (cmd.prev == null) document_id0 else cmd.prev.id) -> Some(cmd.id)
+        (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id)
       }
     process.edit_document(old_id, document_id, removes.reverse ++ inserts)
   }
diff -r b06946a1d4cb -r 5d88e0681d44 src/Tools/jEdit/src/utils/LinearSet.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Mar 19 16:48:29 2009 +0100
@@ -0,0 +1,87 @@
+/*  Title:      LinearSet.scala
+    Author:     Makarius
+
+Sets with canonical linear order, or immutable linked-lists.
+*/
+package isabelle.utils
+
+object LinearSet
+{
+  def empty[A]: LinearSet[A] = new LinearSet[A]
+  def apply[A](elems: A*): LinearSet[A] =
+    (empty[A] /: elems) ((s, elem) => s + elem)
+
+  class Duplicate(s: String) extends Exception(s)
+  class Undefined(s: String) extends Exception(s)
+
+  private def make[A](first: Option[A], last: Option[A], b: Map[A, A]): LinearSet[A] =
+    new LinearSet[A] {
+      override val first_elem = first
+      override val last_elem = last
+      override val body = b
+    }
+}
+
+class LinearSet[A] extends scala.collection.immutable.Set[A]
+{
+  /* representation */
+
+  val first_elem: Option[A] = None
+  val last_elem: Option[A] = None
+  val body: Map[A, A] = Map.empty
+
+
+  /* basic methods */
+
+  def next(elem: A) = body.get(elem)
+  def prev(elem: A) = body.find(_._2 == elem).map(_._1)
+  override def isEmpty: Boolean = !last_elem.isDefined
+  def size: Int = if (isEmpty) 0 else body.size + 1
+
+  def empty[B] = LinearSet.empty[B]
+
+  def contains(elem: A): Boolean =
+    !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem))
+
+  def insert_after(hook: Option[A], elem: A): LinearSet[A] =
+    if (contains(elem)) throw new LinearSet.Duplicate(elem.toString)
+    else hook match {
+      case Some(hook) =>
+        if (!contains(hook)) throw new LinearSet.Undefined(hook.toString)
+        else if (body.isDefinedAt(hook))
+          LinearSet.make(first_elem, last_elem, body - hook + (hook -> elem) + (elem -> body(hook)))
+        else LinearSet.make(first_elem, Some(elem), body + (hook -> elem))
+      case None =>
+        if (isEmpty) LinearSet.make(Some(elem), Some(elem), Map.empty)
+        else LinearSet.make(Some(elem), last_elem, body + (elem -> first_elem.get))
+    }
+    
+  def +(elem: A): LinearSet[A] = insert_after(last_elem, elem)
+
+  def delete_after(elem: Option[A]): LinearSet[A] =
+    elem match {
+      case Some(elem) =>
+        if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
+        else if (!body.isDefinedAt(elem)) throw new LinearSet.Undefined(null)
+        else if (body(elem) == last_elem.get) LinearSet.make(first_elem, Some(elem), body - elem)
+        else LinearSet.make(first_elem, last_elem, body - elem - body(elem) + (elem -> body(body(elem))))
+      case None =>
+        if (isEmpty) throw new LinearSet.Undefined(null)
+        else if (size == 1) empty
+        else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get)
+    }
+    
+  def -(elem: A): LinearSet[A] =
+    if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
+    else delete_after(body find (p => p._2 == elem) map (p => p._1))
+
+  def elements = new Iterator[A] {
+    private var next_elem = first_elem
+    def hasNext = next_elem.isDefined
+    def next = {
+      val elem = next_elem.get
+      next_elem = if (body.isDefinedAt(elem)) Some(body(elem)) else None
+      elem
+    }
+  }
+}
\ No newline at end of file