src/Pure/PIDE/document.ML

   type exec_id = id
   val no_id: id
   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
   val get_theory: state -> version_id -> Position.T -> string -> theory
   val cancel_execution: state -> unit -> unit

 
 
 
 (** 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*)
 with
 

 (* node edits and associated executions *)
 
 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;
 
 fun the_entry (Node {entries, ...}) id =
   (case Entries.lookup entries id of

   Version
     (case node_edit of
       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
     |> Graph.default_node (name, empty_node)
     |> Graph.map_node name (K node));