src/Pure/System/session.scala

   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,
     doc_edits: List[Document.Edit_Command],
-    header_edits: List[(String, Thy_Header.Header)],
     previous: Document.Version,
     version: Document.Version)
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {

         header: Document.Node.Header, edits: List[Document.Node.Edit[Text.Edit]])
     //{{{
     {
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
-      val doc_edits = edits.map(edit => (name, edit))
-      val result = Future.fork {
-        Thy_Syntax.text_edits(syntax, previous.join, doc_edits, List((name, header)))
-      }
+      val doc_edits =
+        (name, Document.Node.Update_Header[Text.Edit](header)) :: 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.map(_._3)))
+        global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
 
       result.map {
-        case (doc_edits, header_edits, _) =>
+        case (doc_edits, _) =>
           assignments.await { global_state().is_assigned(previous.get_finished) }
-          this_actor !
-            Change_Node(name, doc_edits, header_edits, previous.join, change.version.join)
+          this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join)
       }
     }
     //}}}
 
 

     {
       val previous = change.previous
       val version = change.version
       val name = change.name
       val doc_edits = change.doc_edits
-      val header_edits = change.header_edits
 
       var former_assignment = global_state().the_assignment(previous).get_finished
       for {
         (name, Document.Node.Edits(cmd_edits)) <- doc_edits  // FIXME proper coverage!?
         (prev, None) <- cmd_edits

           case (name, edit) =>
             (name, edit.map({ case (c1, c2) => (c1.map(id_command), c2.map(id_command)) }))
         }
 
       global_state.change(_.define_version(version, former_assignment))
-      prover.get.edit_version(previous.id, version.id, id_edits, header_edits)
+      prover.get.edit_version(previous.id, version.id, id_edits)
     }
     //}}}
 
 
     /* prover results */