replaced individual Document_Model history by all-inclusive one in Session;
Document_Model: provide thy_name externally, i.e. by central Isabelle plugin;
tuned;

--- a/src/Pure/PIDE/change.scala	Sat Aug 07 13:19:48 2010 +0200
+++ b/src/Pure/PIDE/change.scala	Sat Aug 07 14:45:26 2010 +0200
@@ -44,18 +44,6 @@
 
   /* editing and state assignment */
 
-  def edit(session: Session, edits: List[Document.Node_Text_Edit]): Change =
-  {
-    val new_id = session.create_id()
-    val result: Future[(List[Document.Edit[Command]], Document)] =
-      Future.fork {
-        val old_doc = join_document
-        old_doc.await_assignment
-        Document.text_edits(session, old_doc, new_id, edits)
-      }
-    new Change(new_id, Some(this), edits, result)
-  }
-
   def join_document: Document = result.join._2
   def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
 

--- a/src/Pure/System/session.scala	Sat Aug 07 13:19:48 2010 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 07 14:45:26 2010 +0200
@@ -315,4 +315,28 @@
   def stop() { session_actor ! Stop }
 
   def input(change: Change) { session_actor ! change }
+
+
+
+  /** editor model **/  // FIXME subclass Editor_Session (!?)
+
+  @volatile private var history = Change.init // owned by Swing thread (!??)
+  def current_change(): Change = history
+
+  def edit_document(edits: List[Document.Node_Text_Edit])
+  {
+    Swing_Thread.now {
+      val old_change = current_change()
+      val new_id = create_id()
+      val result: Future[(List[Document.Edit[Command]], Document)] =
+        Future.fork {
+          val old_doc = old_change.join_document
+          old_doc.await_assignment
+          Document.text_edits(this, old_doc, new_id, edits)
+        }
+      val new_change = new Change(new_id, Some(old_change), edits, result)
+      history = new_change
+      new_change.result.map(_ => input(new_change))
+    }
+  }
 }

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 13:19:48 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 14:45:26 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
-Document model connected to jEdit buffer.
+Document model connected to jEdit buffer -- single node in theory graph.
 */
 
 package isabelle.jedit
@@ -149,10 +149,10 @@
 
   private val key = "isabelle.document_model"
 
-  def init(session: Session, buffer: Buffer): Document_Model =
+  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
   {
     Swing_Thread.assert()
-    val model = new Document_Model(session, buffer)
+    val model = new Document_Model(session, buffer, thy_name)
     buffer.setProperty(key, model)
     model.activate()
     model
@@ -180,7 +180,7 @@
 }
 
 
-class Document_Model(val session: Session, val buffer: Buffer)
+class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
 {
   /* visible line end */
 
@@ -195,33 +195,22 @@
   }
 
 
-  /* global state -- owned by Swing thread */
+  /* text edits */
+
+  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
 
-  @volatile private var history = Change.init // owned by Swing thread
-  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
+  private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
+    if (!edits_buffer.isEmpty) {
+      session.edit_document(List((thy_name, edits_buffer.toList)))
+      edits_buffer.clear
+    }
+  }
 
 
   /* snapshot */
 
-  // FIXME proper error handling
-  val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
-
-  def current_change(): Change = history
-
   def snapshot(): Change.Snapshot =
-    Swing_Thread.now { history.snapshot(thy_name, edits_buffer.toList) }
-
-
-  /* text edits */
-
-  private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
-    if (!edits_buffer.isEmpty) {
-      val new_change = history.edit(session, List((thy_name, edits_buffer.toList)))
-      edits_buffer.clear
-      history = new_change
-      new_change.result.map(_ => session.input(new_change))
-    }
-  }
+    Swing_Thread.now { session.current_change().snapshot(thy_name, edits_buffer.toList) }
 
 
   /* buffer listener */

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Aug 07 13:19:48 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Aug 07 14:45:26 2010 +0200
@@ -162,7 +162,10 @@
   def activate_buffer(view: View, buffer: Buffer)
   {
     if (prover_started(view)) {
-      val model = Document_Model.init(session, buffer)
+      // FIXME proper error handling
+      val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
+
+      val model = Document_Model.init(session, buffer, thy_name)
       for (text_area <- jedit_text_areas(buffer))
         Document_View.init(model, text_area)
     }