uniform treatment of header edits as document edits;

--- a/src/Pure/PIDE/document.ML	Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 11 20:32:44 2011 +0200
@@ -15,16 +15,17 @@
   val new_id: unit -> id
   val parse_id: string -> id
   val print_id: id -> string
-  datatype node_edit = Remove | Edits of (command_id option * command_id option) list
+  datatype node_edit =
+    Remove |
+    Edits of (command_id option * command_id option) list |
+    Update_Header of (string * string list * string list) Exn.result
   type edit = string * node_edit
-  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 -> header list ->
-    state -> (command_id * exec_id) list * state
+  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
   val state: unit -> state
   val change_state: (state -> state) -> unit
@@ -76,11 +77,13 @@
 
 (* node edits and associated executions *)
 
-datatype node_edit = Remove | Edits of (command_id option * command_id option) list;
+datatype node_edit =
+  Remove |
+  Edits of (command_id option * command_id option) list |
+  Update_Header of (string * string list * string list) Exn.result;
+
 type edit = string * node_edit;
 
-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
@@ -107,12 +110,15 @@
 fun get_node version name = Graph.get_node (nodes_of version) name
   handle Graph.UNDEF _ => empty_node;
 
-fun edit_nodes (name, Remove) (Version nodes) =
-      Version (perhaps (try (Graph.del_node name)) nodes)
-  | edit_nodes (name, Edits edits) (Version nodes) =
-      Version (nodes
+fun edit_nodes (name, node_edit) (Version nodes) =
+  Version
+    (case node_edit of
+      Remove => perhaps (try (Graph.del_node name)) nodes
+    | Edits edits =>
+        nodes
         |> Graph.default_node (name, empty_node)
-        |> Graph.map_node name (edit_node edits));
+        |> Graph.map_node name (edit_node edits)
+    | Update_Header _ => nodes);  (* FIXME *)
 
 fun put_node name node (Version nodes) =
   Version (nodes
@@ -312,10 +318,8 @@
 
 in
 
-fun edit (old_id: version_id) (new_id: version_id) edits headers state =
+fun edit (old_id: version_id) (new_id: version_id) edits 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	Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 11 20:32:44 2011 +0200
@@ -44,10 +44,12 @@
         this match {
           case Remove() => Remove()
           case Edits(es) => Edits(es.map(f))
+          case Update_Header(header: Header) => Update_Header(header)
         }
     }
     case class Remove[A]() extends Edit[A]
     case class Edits[A](edits: List[A]) extends Edit[A]
+    case class Update_Header[A](header: Header) extends Edit[A]
 
     sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
     val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))

--- a/src/Pure/PIDE/isar_document.ML	Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 11 20:32:44 2011 +0200
@@ -13,23 +13,24 @@
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.edit_version"
-    (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state =>
+    (fn [old_id_string, new_id_string, edits_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;
-        val edits = YXML.parse_body edits_yxml |>
-          let open XML.Decode in
-            list (pair string
-              (variant
-               [fn ([], []) => Document.Remove,
-                fn ([], a) => Document.Edits (list (pair (option int) (option int)) a)]))
-          end;
-        val headers = YXML.parse_body headers_yxml |>
-          let open XML.Decode
-          in list (pair string (triple string (list string) (list string))) end;
+        val edits =
+          YXML.parse_body edits_yxml |>
+            let open XML.Decode in
+              list (pair string
+                (variant
+                 [fn ([], []) => Document.Remove,
+                  fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+                  fn ([], a) =>
+                    Document.Update_Header (Exn.Res (triple string (list string) (list string) a)),
+                  fn ([a], []) => Document.Update_Header (Exn.Exn (ERROR a))]))
+            end;
 
       val await_cancellation = Document.cancel_execution state;
-      val (updates, state') = Document.edit old_id new_id edits headers state;
+      val (updates, state') = Document.edit old_id new_id edits state;
       val _ = await_cancellation ();
       val _ =
         Output.status (Markup.markup (Markup.assign new_id)

--- a/src/Pure/PIDE/isar_document.scala	Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 11 20:32:44 2011 +0200
@@ -140,24 +140,23 @@
   /* document versions */
 
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-      edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
+    edits: List[Document.Edit_Command_ID])
   {
-    val arg1 =
+    val edits_yxml =
     { import XML.Encode._
       def encode: T[List[Document.Edit_Command_ID]] =
         list(pair(string,
           variant(List(
             { case Document.Node.Remove() => (Nil, Nil) },
-            { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) }))))
-      encode(edits) }
+            { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
+            { case Document.Node.Update_Header(
+                  Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
+                (Nil, triple(string, list(string), list(string))(a, b, c)) },
+            { case Document.Node.Update_Header(
+                  Document.Node.Header(_, Exn.Exn(ERROR(a)))) => (List(a), Nil) }))))
+      YXML.string_of_body(encode(edits)) }
 
-    val arg2 =
-    { import XML.Encode._
-      list(pair(string, Thy_Header.xml_encode))(headers) }
-
-    input("Isar_Document.edit_version",
-      Document.ID(old_id), Document.ID(new_id),
-        YXML.string_of_body(arg1), YXML.string_of_body(arg2))
+    input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
   }
 
 

--- a/src/Pure/System/session.scala	Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 11 20:32:44 2011 +0200
@@ -168,7 +168,6 @@
   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)
 
@@ -186,18 +185,16 @@
     {
       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)
       }
     }
     //}}}
@@ -212,7 +209,6 @@
       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 {
@@ -236,7 +232,7 @@
         }
 
       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)
     }
     //}}}
 

--- a/src/Pure/Thy/thy_header.scala	Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Thu Aug 11 20:32:44 2011 +0200
@@ -31,13 +31,6 @@
       Header(f(name), imports.map(f), uses.map(f))
   }
 
-  val xml_encode: XML.Encode.T[Header] =
-  {
-    case Header(name, imports, uses) =>
-      import XML.Encode._
-      triple(string, list(string), list(string))(name, imports, uses)
-  }
-
 
   /* file name */
 

--- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 11 18:01:28 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 11 20:32:44 2011 +0200
@@ -102,9 +102,8 @@
   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) =
+      edits: List[Document.Edit_Text])
+    : (List[Document.Edit_Command], Document.Version) =
   {
     /* phase 1: edit individual command source */
 
@@ -173,25 +172,10 @@
     }
 
 
-    /* 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 {
@@ -213,13 +197,19 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Document.Node.Edits(cmd_edits))
-
-          val (new_headers, new_header) = node_header(name, node)
-          header_edits ++= new_headers
+          nodes += (name -> node.copy(commands = commands2))
 
-          nodes += (name -> Document.Node(new_header, node.blobs, commands2))
+        case (name, Document.Node.Update_Header(header)) =>
+          val node = nodes(name)
+          val update_header =
+            (node.header.thy_header, header) match {
+              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header)))
+              if thy_header0 != thy_header => true
+              case (Exn.Exn(_), Document.Node.Header(_, Exn.Res(thy_header))) => true
+            }
+          if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
       }
-      (doc_edits.toList, header_edits.toList, Document.Version(Document.new_id(), nodes))
+      (doc_edits.toList, Document.Version(Document.new_id(), nodes))
     }
   }
 }