--- 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;