# HG changeset patch
# User wenzelm
# Date 1310228123 -7200
# Node ID 4a4ca9e4a14b4a97ca70583dfc8956237056ffa7
# Parent  c3ddb5537a2f20afc75ef8e67503815184e07371
clarified propagation of node name and header;

diff -r c3ddb5537a2f -r 4a4ca9e4a14b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 09 17:14:08 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Jul 09 18:15:23 2011 +0200
@@ -165,6 +165,7 @@
   private case object Interrupt
   private case class Init_Node(name: String, header: Document.Node.Header, text: String)
   private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
+  private case class Change_Node(name: String, header: Document.Node.Header, change: Document.Change)
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
@@ -174,24 +175,26 @@
 
     /* incoming edits */
 
-    def handle_edits(headers: List[Document.Node.Header], edits: List[Document.Edit_Text])
+    def handle_edits(name: String,
+        header: Document.Node.Header, edits: List[Option[List[Text.Edit]]])
     //{{{
     {
       val syntax = current_syntax()
       val previous = current_state().history.tip.version
-      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, edits) }
-      val change = global_state.change_yield(_.extend_history(previous, edits, result))
+      val doc_edits = edits.map(edit => (name, edit))
+      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
+      val change = global_state.change_yield(_.extend_history(previous, doc_edits, result))
 
       change.version.map(_ => {
         assignments.await { current_state().is_assigned(previous.get_finished) }
-        this_actor ! change })
+        this_actor ! Change_Node(name, header, change) })
     }
     //}}}
 
 
     /* resulting changes */
 
-    def handle_change(change: Document.Change)
+    def handle_change(name: String, header: Document.Node.Header, change: Document.Change)
     //{{{
     {
       val previous = change.previous.get_finished
@@ -312,22 +315,17 @@
         case Interrupt if prover.isDefined =>
           prover.get.interrupt
 
-        case Edit_Node(name, header, text_edits) if prover.isDefined =>
-          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
-          handle_edits(List(header), List((node_name, Some(text_edits))))
-          reply(())
-
         case Init_Node(name, header, text) if prover.isDefined =>
           // FIXME compare with existing node
-          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
-          handle_edits(List(header),
-            List(
-              (node_name, None),
-              (node_name, Some(List(Text.Edit.insert(0, text))))))
+          handle_edits(name, header, List(None, Some(List(Text.Edit.insert(0, text)))))
           reply(())
 
-        case change: Document.Change if prover.isDefined =>
-          handle_change(change)
+        case Edit_Node(name, header, text_edits) if prover.isDefined =>
+          handle_edits(name, header, List(Some(text_edits)))
+          reply(())
+
+        case Change_Node(name, header, change) if prover.isDefined =>
+          handle_change(name, header, change)
 
         case result: Isabelle_Process.Result =>
           handle_result(result)
diff -r c3ddb5537a2f -r 4a4ca9e4a14b src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Jul 09 17:14:08 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jul 09 18:15:23 2011 +0200
@@ -61,6 +61,8 @@
 {
   /* pending text edits */
 
+  private val node_name = (master_dir + Path.basic(thy_name)).implode
+
   private def node_header(): Document.Node.Header =
     Document.Node.Header(master_dir,
       Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
@@ -77,14 +79,14 @@
         case Nil =>
         case edits =>
           pending.clear
-          session.edit_node(thy_name, node_header(), edits)
+          session.edit_node(node_name, node_header(), edits)
       }
     }
 
     def init()
     {
       flush()
-      session.init_node(thy_name, node_header(), Isabelle.buffer_text(buffer))
+      session.init_node(node_name, node_header(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =
@@ -104,7 +106,6 @@
   def snapshot(): Document.Snapshot =
   {
     Swing_Thread.require()
-    val node_name = (master_dir + Path.basic(thy_name)).implode  // FIXME
     session.snapshot(node_name, pending_edits.snapshot())
   }