clarified node header -- exclude master_dir;

--- a/src/Pure/PIDE/document.ML	Sat Aug 13 13:48:26 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 13 15:59:26 2011 +0200
@@ -15,11 +15,11 @@
   val new_id: unit -> id
   val parse_id: string -> id
   val print_id: id -> string
-  type node_header = string * string list * string list
+  type node_header = (string * string list * string list) Exn.result
   datatype node_edit =
     Remove |
     Edits of (command_id option * command_id option) list |
-    Update_Header of node_header Exn.result
+    Header of node_header
   type edit = string * node_edit
   type state
   val init_state: state
@@ -55,11 +55,11 @@
 
 (** document structure **)
 
-type node_header = string * string list * string list;
+type node_header = (string * string list * string list) Exn.result;
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 abstype node = Node of
- {header: node_header Exn.result,
+ {header: node_header,
   entries: exec_id option Entries.T,  (*command entries with excecutions*)
   last: exec_id}  (*last entry with main result*)
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
@@ -90,7 +90,7 @@
 datatype node_edit =
   Remove |
   Edits of (command_id option * command_id option) list |
-  Update_Header of node_header Exn.result;
+  Header of node_header;
 
 type edit = string * node_edit;
 
@@ -129,7 +129,7 @@
       Remove => perhaps (try (Graph.del_node name)) nodes
     | Edits edits => update_node name (edit_node edits) nodes
     (* FIXME maintain deps; cycles!? *)
-    | Update_Header header => update_node name (set_header header) nodes);
+    | Header header => update_node name (set_header header) nodes);
 
 fun put_node name node (Version nodes) =
   Version (nodes

--- a/src/Pure/PIDE/document.scala	Sat Aug 13 13:48:26 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 13 15:59:26 2011 +0200
@@ -36,6 +36,8 @@
   type Edit_Command = Edit[(Option[Command], Option[Command])]
   type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
 
+  type Node_Header = Exn.Result[Thy_Header]
+
   object Node
   {
     sealed abstract class Edit[A]
@@ -44,26 +46,20 @@
         this match {
           case Remove() => Remove()
           case Edits(es) => Edits(es.map(f))
-          case Update_Header(header: Header) => Update_Header(header)
+          case Header(header) => 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]
+    case class Header[A](header: Node_Header) extends Edit[A]
 
-    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
-    {
-      def norm_deps(f: (String, Path) => String): Header =
-        copy(thy_header =
-          thy_header match {
-            case Exn.Res(header) =>
-              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
-            case exn => exn
-          })
-    }
-    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
+    def norm_header[A](f: Path => String, header: Node_Header): Header[A] =
+      header match {
+        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(name => f(Path.explode(name))) })
+        case exn => Header[A](exn)
+      }
 
-    val empty: Node = Node(empty_header, Map(), Linear_Set())
+    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -80,7 +76,7 @@
   private val block_size = 1024
 
   sealed case class Node(
-    val header: Node.Header,
+    val header: Node_Header,
     val blobs: Map[String, Blob],
     val commands: Linear_Set[Command])
   {

--- a/src/Pure/PIDE/isar_document.ML	Sat Aug 13 13:48:26 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Sat Aug 13 15:59:26 2011 +0200
@@ -25,8 +25,8 @@
                  [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))]))
+                    Document.Header (Exn.Res (triple string (list string) (list string) a)),
+                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
             end;
 
       val await_cancellation = Document.cancel_execution state;

--- a/src/Pure/PIDE/isar_document.scala	Sat Aug 13 13:48:26 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sat Aug 13 15:59:26 2011 +0200
@@ -149,11 +149,9 @@
           variant(List(
             { case Document.Node.Remove() => (Nil, Nil) },
             { 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(a, b, c)))) =>
+            { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
                 (Nil, triple(string, list(string), list(string))(a, b, c)) },
-            { case Document.Node.Update_Header(
-                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
+            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
       YXML.string_of_body(encode(edits)) }
 
     input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)

--- a/src/Pure/System/session.scala	Sat Aug 13 13:48:26 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 13 15:59:26 2011 +0200
@@ -164,8 +164,10 @@
 
   private case class Start(timeout: Time, args: List[String])
   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 Init_Node(
+    name: String, master_dir: String, header: Document.Node_Header, text: String)
+  private case class Edit_Node(
+    name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
   private case class Change_Node(
     name: String,
     doc_edits: List[Document.Edit_Command],
@@ -180,15 +182,15 @@
 
     /* incoming edits */
 
-    def handle_edits(name: String,
-        header: Document.Node.Header, edits: List[Document.Node.Edit[Text.Edit]])
+    def handle_edits(name: String, master_dir: String,
+        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 =
-        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
-          edits.map(edit => (name, edit))
+      val norm_header =
+        Document.Node.norm_header[Text.Edit](file_store.append(master_dir, _), header)
+      val doc_edits = (name, norm_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(_._2)))
@@ -325,14 +327,14 @@
         case Interrupt if prover.isDefined =>
           prover.get.interrupt
 
-        case Init_Node(name, header, text) if prover.isDefined =>
+        case Init_Node(name, master_dir, header, text) if prover.isDefined =>
           // FIXME compare with existing node
-          handle_edits(name, header,
+          handle_edits(name, master_dir, header,
             List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
           reply(())
 
-        case Edit_Node(name, header, text_edits) if prover.isDefined =>
-          handle_edits(name, header, List(Document.Node.Edits(text_edits)))
+        case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
+          handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
           reply(())
 
         case change: Change_Node if prover.isDefined =>
@@ -360,9 +362,9 @@
 
   def interrupt() { session_actor ! Interrupt }
 
-  def init_node(name: String, header: Document.Node.Header, text: String)
-  { session_actor !? Init_Node(name, header, text) }
+  def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
+  { session_actor !? Init_Node(name, master_dir, header, text) }
 
-  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
-  { session_actor !? Edit_Node(name, header, edits) }
+  def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
+  { session_actor !? Edit_Node(name, master_dir, header, edits) }
 }

--- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 13:48:26 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 15:59:26 2011 +0200
@@ -199,16 +199,15 @@
           doc_edits += (name -> Document.Node.Edits(cmd_edits))
           nodes += (name -> node.copy(commands = commands2))
 
-        case (name, Document.Node.Update_Header(header)) =>
+        case (name, Document.Node.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))) =>
-                thy_header0 != thy_header
+            (node.header, header) match {
+              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
               case _ => true
             }
           if (update_header) {
-            doc_edits += (name -> Document.Node.Update_Header(header))
+            doc_edits += (name -> Document.Node.Header(header))
             nodes += (name -> node.copy(header = header))
           }
       }

--- a/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 13:48:26 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 15:59:26 2011 +0200
@@ -62,9 +62,8 @@
 {
   /* pending text edits */
 
-  def node_header(): Document.Node.Header =
-    Document.Node.Header(master_dir,
-      Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
+  def node_header(): Exn.Result[Thy_Header] =
+    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
 
   private object pending_edits  // owned by Swing thread
   {
@@ -78,14 +77,14 @@
         case Nil =>
         case edits =>
           pending.clear
-          session.edit_node(node_name, node_header(), edits)
+          session.edit_node(node_name, master_dir, node_header(), edits)
       }
     }
 
     def init()
     {
       flush()
-      session.init_node(node_name, node_header(), Isabelle.buffer_text(buffer))
+      session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =