propagate header changes to prover process;
simplified Document case classes;
Document.State.assignments: indexed by Version_ID;

--- a/src/Pure/PIDE/document.ML	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sun Jul 10 00:21:19 2011 +0200
@@ -16,12 +16,14 @@
   val parse_id: string -> id
   val print_id: id -> string
   type edit = string * ((command_id option * command_id option) list) option
+  type header = string * (string * string list * string list)
   type state
   val init_state: state
   val get_theory: state -> version_id -> Position.T -> string -> theory
   val cancel_execution: state -> unit -> unit
   val define_command: command_id -> string -> state -> state
-  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
+  val edit: version_id -> version_id -> edit list -> header list ->
+    state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
   val state: unit -> state
   val change_state: (state -> state) -> unit
@@ -78,6 +80,8 @@
   (*NONE: remove node, SOME: insert/remove commands*)
   ((command_id option * command_id option) list) option;
 
+type header = string * (string * string list * string list);
+
 fun the_entry (Node {entries, ...}) id =
   (case Entries.lookup entries id of
     NONE => err_undef "command entry" id
@@ -309,8 +313,10 @@
 
 in
 
-fun edit (old_id: version_id) (new_id: version_id) edits state =
+fun edit (old_id: version_id) (new_id: version_id) edits headers state =
   let
+    (* FIXME apply headers *)
+
     val old_version = the_version state old_id;
     val _ = Time.now ();  (* FIXME odd workaround *)
     val new_version = fold edit_nodes edits old_version;

--- a/src/Pure/PIDE/document.scala	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Jul 10 00:21:19 2011 +0200
@@ -70,11 +70,6 @@
     val blobs: Map[String, Blob],
     val commands: Linear_Set[Command])
   {
-    /* header */
-
-    def set_header(new_header: Node.Header): Node = copy(header = new_header)
-
-
     /* commands */
 
     private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
@@ -135,25 +130,24 @@
 
   object Version
   {
-    val init: Version = new Version(no_id, Map().withDefaultValue(Node.empty))
+    val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
   }
 
-  class Version(val id: Version_ID, val nodes: Map[String, Node])
+  sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
 
 
   /* changes of plain text, eventually resulting in document edits */
 
   object Change
   {
-    val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
+    val init = Change(Future.value(Version.init), Nil, Future.value(Version.init))
   }
 
-  class Change(
+  sealed case class Change(
     val previous: Future[Version],
     val edits: List[Edit_Text],
-    val result: Future[(List[Edit_Command], Version)])
+    val version: Future[Version])
   {
-    val version: Future[Version] = result.map(_._2)
     def is_finished: Boolean = previous.is_finished && version.is_finished
   }
 
@@ -216,7 +210,7 @@
     val versions: Map[Version_ID, Version] = Map(),
     val commands: Map[Command_ID, Command.State] = Map(),
     val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
-    val assignments: Map[Version, State.Assignment] = Map(),
+    val assignments: Map[Version_ID, State.Assignment] = Map(),
     val disposed: Set[ID] = Set(),  // FIXME unused!?
     val history: History = History.init)
   {
@@ -227,7 +221,7 @@
       val id = version.id
       if (versions.isDefinedAt(id) || disposed(id)) fail
       copy(versions = versions + (id -> version),
-        assignments = assignments + (version -> State.Assignment(former_assignment)))
+        assignments = assignments + (id -> State.Assignment(former_assignment)))
     }
 
     def define_command(command: Command): State =
@@ -242,7 +236,8 @@
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
     def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
-    def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
+    def the_assignment(version: Version): State.Assignment =
+      assignments.getOrElse(version.id, fail)
 
     def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
@@ -272,22 +267,21 @@
           (st.command, exec_id)
         }
       val new_assignment = the_assignment(version).assign(assigned_execs)
-      val new_state =
-        copy(assignments = assignments + (version -> new_assignment), execs = new_execs)
+      val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
       (assigned_execs.map(_._1), new_state)
     }
 
     def is_assigned(version: Version): Boolean =
-      assignments.get(version) match {
+      assignments.get(version.id) match {
         case Some(assgn) => assgn.is_finished
         case None => false
       }
 
     def extend_history(previous: Future[Version],
         edits: List[Edit_Text],
-        result: Future[(List[Edit_Command], Version)]): (Change, State) =
+        version: Future[Version]): (Change, State) =
     {
-      val change = new Change(previous, edits, result)
+      val change = Change(previous, edits, version)
       (change, copy(history = history + change))
     }
 

--- a/src/Pure/PIDE/isar_document.ML	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 00:21:19 2011 +0200
@@ -13,7 +13,7 @@
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.edit_version"
-    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
+    (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state =>
       let
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;
@@ -26,9 +26,15 @@
                   (XML_Data.dest_pair
                     (XML_Data.dest_option XML_Data.dest_int)
                     (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
+        val headers =
+          XML_Data.dest_list
+            (XML_Data.dest_pair XML_Data.dest_string
+              (XML_Data.dest_triple XML_Data.dest_string
+                (XML_Data.dest_list XML_Data.dest_string)
+                (XML_Data.dest_list XML_Data.dest_string))) (YXML.parse_body headers_yxml);
 
       val await_cancellation = Document.cancel_execution state;
-      val (updates, state') = Document.edit old_id new_id edits state;
+      val (updates, state') = Document.edit old_id new_id edits headers state;
       val _ = await_cancellation ();
       val _ =
         Output.status (Markup.markup (Markup.assign new_id)

--- a/src/Pure/PIDE/isar_document.scala	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 00:21:19 2011 +0200
@@ -140,9 +140,9 @@
   /* document versions */
 
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-      edits: List[Document.Edit_Command_ID])
+      edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
   {
-    val arg =
+    val arg1 =
       XML_Data.make_list(
         XML_Data.make_pair(XML_Data.make_string)(
           XML_Data.make_option(XML_Data.make_list(
@@ -150,7 +150,11 @@
                 XML_Data.make_option(XML_Data.make_long))(
                 XML_Data.make_option(XML_Data.make_long))))))(edits)
 
+    val arg2 =
+      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string)(Thy_Header.make_xml_data))(headers)
+
     input("Isar_Document.edit_version",
-      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
+      Document.ID(old_id), Document.ID(new_id),
+        YXML.string_of_body(arg1), YXML.string_of_body(arg2))
   }
 }

--- a/src/Pure/System/session.scala	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Pure/System/session.scala	Sun Jul 10 00:21:19 2011 +0200
@@ -165,7 +165,12 @@
   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 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)
   {
@@ -182,27 +187,36 @@
       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) }
-      val change = global_state.change_yield(_.extend_history(previous, doc_edits, result))
+      val result = Future.fork {
+        Thy_Syntax.text_edits(syntax, previous.join, doc_edits, List((name, header)))
+      }
+      val change =
+        global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._3)))
 
-      change.version.map(_ => {
-        assignments.await { global_state().is_assigned(previous.get_finished) }
-        this_actor ! Change_Node(name, header, change) })
+      result.map {
+        case (doc_edits, header_edits, _) =>
+          assignments.await { global_state().is_assigned(previous.get_finished) }
+          this_actor !
+            Change_Node(name, doc_edits, header_edits, previous.join, change.version.join)
+      }
     }
     //}}}
 
 
     /* resulting changes */
 
-    def handle_change(name: String, header: Document.Node.Header, change: Document.Change)
+    def handle_change(change: Change_Node)
     //{{{
     {
-      val previous = change.previous.get_finished
-      val (node_edits, version) = change.result.get_finished
+      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, Some(cmd_edits)) <- node_edits
+        (name, Some(cmd_edits)) <- doc_edits
         (prev, None) <- cmd_edits
         removed <- previous.nodes(name).commands.get_after(prev)
       } former_assignment -= removed
@@ -216,14 +230,15 @@
         command.id
       }
       val id_edits =
-        node_edits map {
+        doc_edits map {
           case (name, edits) =>
             val ids =
               edits.map(_.map { case (c1, c2) => (c1.map(id_command), c2.map(id_command)) })
             (name, ids)
         }
+
       global_state.change(_.define_version(version, former_assignment))
-      prover.get.edit_version(previous.id, version.id, id_edits)
+      prover.get.edit_version(previous.id, version.id, id_edits, header_edits)
     }
     //}}}
 
@@ -315,8 +330,8 @@
           handle_edits(name, header, List(Some(text_edits)))
           reply(())
 
-        case Change_Node(name, header, change) if prover.isDefined =>
-          handle_change(name, header, change)
+        case change: Change_Node if prover.isDefined =>
+          handle_change(change)
 
         case input: Isabelle_Process.Input =>
           raw_messages.event(input)

--- a/src/Pure/Thy/thy_header.scala	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 00:21:19 2011 +0200
@@ -31,6 +31,11 @@
       Header(f(name), imports.map(f), uses.map(f))
   }
 
+  def make_xml_data(header: Header): XML.Body =
+    XML_Data.make_triple(XML_Data.make_string)(
+      XML_Data.make_list(XML_Data.make_string))(
+        XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)
+
 
   /* file name */
 

--- a/src/Pure/Thy/thy_syntax.scala	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Jul 10 00:21:19 2011 +0200
@@ -99,8 +99,12 @@
 
   /** text edits **/
 
-  def text_edits(syntax: Outer_Syntax, previous: Document.Version,
-      edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+  def text_edits(
+      syntax: Outer_Syntax,
+      previous: Document.Version,
+      edits: List[Document.Edit_Text],
+      headers: List[(String, Document.Node.Header)])
+    : (List[Document.Edit_Command], List[(String, Thy_Header.Header)], Document.Version) =
   {
     /* phase 1: edit individual command source */
 
@@ -169,10 +173,25 @@
     }
 
 
+    /* node header */
+
+    def node_header(name: String, node: Document.Node)
+        : (List[(String, Thy_Header.Header)], Document.Node.Header) =
+      (node.header.thy_header, headers.find(p => p._1 == name).map(_._2)) match {
+        case (Exn.Res(thy_header0), Some(header @ Document.Node.Header(_, Exn.Res(thy_header))))
+        if thy_header0 != thy_header =>
+          (List((name, thy_header)), header)
+        case (Exn.Exn(_), Some(header @ Document.Node.Header(_, Exn.Res(thy_header)))) =>
+          (List((name, thy_header)), header)
+        case _ => (Nil, node.header)
+      }
+
+
     /* resulting document edits */
 
     {
       val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
+      val header_edits = new mutable.ListBuffer[(String, Thy_Header.Header)]
       var nodes = previous.nodes
 
       edits foreach {
@@ -194,9 +213,13 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Some(cmd_edits))
-          nodes += (name -> Document.Node(node.header, node.blobs, commands2))
+
+          val (new_headers, new_header) = node_header(name, node)
+          header_edits ++= new_headers
+
+          nodes += (name -> Document.Node(new_header, node.blobs, commands2))
       }
-      (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
+      (doc_edits.toList, header_edits.toList, Document.Version(Document.new_id(), nodes))
     }
   }
 }

--- a/src/Tools/jEdit/src/document_model.scala	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Jul 10 00:21:19 2011 +0200
@@ -64,7 +64,7 @@
   private val node_name = (master_dir + Path.basic(thy_name)).implode
 
   private def node_header(): Document.Node.Header =
-    Document.Node.Header(master_dir,
+    Document.Node.Header(Path.current,  // FIXME master_dir (!?)
       Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
 
   private object pending_edits  // owned by Swing thread