more explicit edit_node vs. init_node;
some support for master_dir and header;

--- a/src/Pure/System/session.scala	Sun Jul 03 15:10:17 2011 +0200
+++ b/src/Pure/System/session.scala	Sun Jul 03 19:42:32 2011 +0200
@@ -145,13 +145,17 @@
   def current_state(): Document.State = global_state.peek()
 
   private case object Interrupt_Prover
-  private case class Edit_Version(edits: List[Document.Edit_Text])
+  private case class Edit_Node(thy_name: String,
+    header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
+  private case class Init_Node(thy_name: String,
+    header: Exn.Result[Thy_Header.Header], text: String)
   private case class Start(timeout: Time, args: List[String])
 
   var verbose: Boolean = false
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
+    val this_actor = self
     var prover: Isabelle_Process with Isar_Document = null
 
 
@@ -251,6 +255,21 @@
     //}}}
 
 
+    def edit_version(edits: List[Document.Edit_Text])
+    //{{{
+    {
+      val previous = global_state.peek().history.tip.version
+      val syntax = current_syntax()
+      val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
+      val change = global_state.change_yield(_.extend_history(previous, edits, result))
+
+      change.version.map(_ => {
+        assignments.await { global_state.peek().is_assigned(previous.get_finished) }
+        this_actor ! change })
+    }
+    //}}}
+
+
     /* main loop */
 
     var finished = false
@@ -259,27 +278,26 @@
         case Interrupt_Prover =>
           if (prover != null) prover.interrupt
 
-        case Edit_Version(edits) if prover != null =>
-          val previous = global_state.peek().history.tip.version
-          val syntax = current_syntax()
-          val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
-          val change = global_state.change_yield(_.extend_history(previous, edits, result))
-
-          val this_actor = self
-          change.version.map(_ => {
-            assignments.await { global_state.peek().is_assigned(previous.get_finished) }
-            this_actor ! change })
-
+        case Edit_Node(thy_name, header, text_edits) if prover != null =>
+          edit_version(List((thy_name, Some(text_edits))))
           reply(())
 
-        case change: Document.Change if prover != null => handle_change(change)
+        case Init_Node(thy_name, header, text) if prover != null =>
+          // FIXME compare with existing node
+          edit_version(List(
+            (thy_name, None),
+            (thy_name, Some(List(Text.Edit.insert(0, text))))))
+          reply(())
+
+        case change: Document.Change if prover != null =>
+          handle_change(change)
 
         case result: Isabelle_Process.Result => handle_result(result)
 
         case Start(timeout, args) if prover == null =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-            prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
+            prover = new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document
           }
 
         case Stop =>
@@ -308,7 +326,15 @@
 
   def interrupt() { session_actor ! Interrupt_Prover }
 
-  def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) }
+  def edit_node(thy_name: String, header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
+  {
+    session_actor !? Edit_Node(thy_name, header, edits)
+  }
+
+  def init_node(thy_name: String, header: Exn.Result[Thy_Header.Header], text: String)
+  {
+    session_actor !? Init_Node(thy_name, header, text)
+  }
 
   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
     global_state.peek().snapshot(name, pending_edits)

--- a/src/Pure/Thy/thy_header.scala	Sun Jul 03 15:10:17 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Jul 03 19:42:32 2011 +0200
@@ -36,8 +36,10 @@
 
   /* file name */
 
-  val Thy_Path1 = new Regex("([^/]*)\\.thy")
-  val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
+  def thy_path(name: String): Path = Path.basic(name).ext("thy")
+
+  private val Thy_Path1 = new Regex("([^/]*)\\.thy")
+  private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
 
   def split_thy_path(path: String): Option[(String, String)] =
     path match {
@@ -108,4 +110,15 @@
     try { read(reader).decode_permissive_utf8 }
     finally { reader.close }
   }
+
+
+  /* check */
+
+  def check(name: String, source: CharSequence): Header =
+  {
+    val header = read(source)
+    val name1 = header.name
+    if (name == name1) header
+    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1))
+  }
 }

--- a/src/Tools/jEdit/src/document_model.scala	Sun Jul 03 15:10:17 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Jul 03 19:42:32 2011 +0200
@@ -45,10 +45,10 @@
     }
   }
 
-  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
+  def init(session: Session, buffer: Buffer, master_dir: String, thy_name: String): Document_Model =
   {
     exit(buffer)
-    val model = new Document_Model(session, buffer, thy_name)
+    val model = new Document_Model(session, buffer, master_dir, thy_name)
     buffer.setProperty(key, model)
     model.activate()
     model
@@ -56,31 +56,36 @@
 }
 
 
-class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
+class Document_Model(val session: Session,
+  val buffer: Buffer, val master_dir: String, val thy_name: String)
 {
   /* pending text edits */
 
+  private def capture_header(): Exn.Result[Thy_Header.Header] =
+    Exn.capture {
+      session.thy_header.check(thy_name, buffer.getSegment(0, buffer.getLength))
+    }
+
   private object pending_edits  // owned by Swing thread
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
     def snapshot(): List[Text.Edit] = pending.toList
 
-    def flush(more_edits: Option[List[Text.Edit]]*)
+    def flush()
     {
       Swing_Thread.require()
-      val edits = snapshot()
-      pending.clear
-
-      val all_edits =
-        if (edits.isEmpty) more_edits.toList
-        else Some(edits) :: more_edits.toList
-      if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
+      snapshot() match {
+        case Nil =>
+        case edits =>
+          pending.clear
+          session.edit_node(master_dir + "/" + thy_name, capture_header(), edits)
+      }
     }
 
     def init()
     {
-      Swing_Thread.require()
-      flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
+      flush()
+      session.init_node(master_dir + "/" + thy_name, capture_header(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =
@@ -100,7 +105,7 @@
   def snapshot(): Document.Snapshot =
   {
     Swing_Thread.require()
-    session.snapshot(thy_name, pending_edits.snapshot())
+    session.snapshot(master_dir + "/" + thy_name, pending_edits.snapshot())
   }
 
 

--- a/src/Tools/jEdit/src/plugin.scala	Sun Jul 03 15:10:17 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Jul 03 19:42:32 2011 +0200
@@ -201,8 +201,8 @@
           case None =>
             // FIXME strip protocol prefix of URL
             Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
-              case Some((dir, thy_name)) =>
-                Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
+              case Some((master_dir, thy_name)) =>
+                Some(Document_Model.init(session, buffer, master_dir, thy_name))
               case None => None
             }
         }