# HG changeset patch
# User immler@in.tum.de
# Date 1239037478 -7200
# Node ID 56217d219e27fdfe90f3336f79f94be92825f453
# Parent  b32b20f0692ff8a87650efbfacfbabe782cd04af
proofdocument-versions get id from changes

diff -r b32b20f0692f -r 56217d219e27 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sat Mar 28 15:40:47 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Apr 06 19:04:38 2009 +0200
@@ -80,7 +80,7 @@
     val start = buffer.getLineStartOffset(line)
     val stop = start + line_segment.count
 
-    val (current_document, current_version) = synchronized (prover.document, prover.document_id)
+    val current_document = prover.document
    
     def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
     def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
diff -r b32b20f0692f -r 56217d219e27 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat Mar 28 15:40:47 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 06 19:04:38 2009 +0200
@@ -42,8 +42,7 @@
 class TheoryView (text_area: JEditTextArea, document_actor: Actor)
     extends TextAreaExtension with BufferListener {
 
-  private var id_count = 0;
-  private def id(): Int = synchronized {id_count += 1; id_count}
+  def id() = Isabelle.plugin.id();
   
   private val buffer = text_area.getBuffer
   private val prover = Isabelle.prover_setup(buffer).get.prover
diff -r b32b20f0692f -r 56217d219e27 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sat Mar 28 15:40:47 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Apr 06 19:04:38 2009 +0200
@@ -38,23 +38,27 @@
       "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
       "[()\\[\\]{}:;]", Pattern.MULTILINE)
 
- val empty = new ProofDocument(LinearSet.empty, LinearSet.empty, false, _ => false)
+ val empty =
+  new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), LinearSet.empty, LinearSet.empty, false, _ => false)
 
 }
 
-class ProofDocument(val tokens: LinearSet[Token],
+class ProofDocument(val id: String,
+                    val tokens: LinearSet[Token],
                     val commands: LinearSet[Command],
                     val active: Boolean,
                     is_command_keyword: String => Boolean)
 {
 
-  def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword)
+  def mark_active: ProofDocument =
+    new ProofDocument(id, tokens, commands, true, is_command_keyword)
   def activate: (ProofDocument, StructureChange) = {
-    val (doc, change) = text_changed(new Text.Change(0, 0, content, content.length))
+    val (doc, change) =
+      text_changed(new Text.Change(isabelle.jedit.Isabelle.plugin.id(), 0, content, content.length))
     return (doc.mark_active, change)
   }
   def set_command_keyword(f: String => Boolean): ProofDocument =
-    new ProofDocument(tokens, commands, active, f)
+    new ProofDocument(id, tokens, commands, active, f)
 
   def content = Token.string_from_tokens(List() ++ tokens)
   /** token view **/
@@ -105,13 +109,11 @@
       }
     }
     val insert = new_tokens.reverse
-    val new_tokenset = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]]
-
-    token_changed(begin.lastOption,
+    val new_token_list = begin ::: insert ::: old_suffix
+    token_changed(change.id,
                   insert,
                   removed,
-                  new_tokenset,
-                  old_suffix.firstOption)
+                  new_token_list)
   }
   
   /** command view **/
@@ -121,40 +123,32 @@
     return null
   }
 
-  private def token_changed(before_change: Option[Token],
+  private def token_changed(new_id: String,
                             inserted_tokens: List[Token],
                             removed_tokens: List[Token],
-                            new_tokenset: LinearSet[Token],
-                            after_change: Option[Token]): (ProofDocument, StructureChange) =
+                            new_token_list: List[Token]): (ProofDocument, StructureChange) =
   {
-    val commands = List() ++ this.commands
+    val commands = List[Command]() ++ this.commands
+
+    // calculate removed commands
+    val first_removed = removed_tokens.firstOption
+    val last_removed = removed_tokens.lastOption
+
     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))
+      first_removed match {
+        case None => (Nil: List[Command], commands)
+        case Some(fr) => commands.break(_.tokens.contains(fr))
       }
-    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)
-    }
-    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)
-        }
+    val removed: List[Command]=
+      last_removed match {
+        case None => Nil
+        case Some(lr) =>
+          remaining.takeWhile(!_.tokens.contains(lr)) ++
+          (remaining.find(_.tokens.contains(lr)) match {
+            case None => Nil
+            case Some(x) => List(x)
+          })
       }
-    val pseudo_new_post = rest.dropWhile(Some(_) != after_change)
 
     def tokens_to_commands(tokens: List[Token]): List[Command]= {
       tokens match {
@@ -165,13 +159,24 @@
       }
     }
 
-    val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
+    // calculate inserted commands
+    val first_inserted = inserted_tokens.firstOption
+    val last_inserted = inserted_tokens.lastOption
+
+    val new_commands = tokens_to_commands(new_token_list)
 
-    val new_commandset = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
+    // drop known commands from the beginning
+    val after_change = new_commands
+    val inserted_commands = new_commands.dropWhile(_.tokens.contains(first_inserted))
+
+    val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
+    val new_commandset = (LinearSet() ++ (new_commands)).asInstanceOf[LinearSet[Command]]
+
     val before = begin match {case Nil => None case _ => Some (begin.last)}
+    val change = new StructureChange(None,List() ++ new_commandset, removed)
 
-    val change = new StructureChange(before, new_commands, removed)
-    val doc = new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword)
+    val doc =
+      new ProofDocument(new_id, new_tokenset, new_commandset, active, is_command_keyword)
     return (doc, change)
   }
 }
diff -r b32b20f0692f -r 56217d219e27 src/Tools/jEdit/src/proofdocument/Text.scala
--- a/src/Tools/jEdit/src/proofdocument/Text.scala	Sat Mar 28 15:40:47 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala	Mon Apr 06 19:04:38 2009 +0200
@@ -8,7 +8,7 @@
 
 
 object Text {
-  case class Change(id: Int, start: Int, val added: String, val removed: Int) {
+  case class Change(id: String, 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 b32b20f0692f -r 56217d219e27 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sat Mar 28 15:40:47 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Apr 06 19:04:38 2009 +0200
@@ -48,11 +48,10 @@
     mutable.SynchronizedMap[IsarDocument.State_ID, Command]
   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_versions = List((document_id0, ProofDocument.empty))
+  private var document_versions = List(ProofDocument.empty)
+  private val document_id0 = ProofDocument.empty.id
 
-  def document_id = document_versions.head._1
-  def document = document_versions.head._2
+  def document = document_versions.head
 
   private var initialized = false
 
@@ -145,7 +144,7 @@
 
                   // document edits
                   case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
-                  if document_versions.exists(dv => doc_id == dv._1) =>
+                  if document_versions.exists(dv => doc_id == dv.id) =>
                     output_info.event(result.toString)
                     for {
                       XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
@@ -212,24 +211,22 @@
     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)
+            val old = document
+            val (doc, structure_change) = old.activate
+            document_versions ::= 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))
+            val old = document
+            val doc = old.set_command_keyword(f)
+            document_versions ::= doc
+            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)
+            val old = document
+            val (doc, structure_change) = old.text_changed(change)
+            document_versions ::= doc
+            edit_document(old.id, doc.id, structure_change)
         }
         case command: Command => {
             //state of command has changed