src/Pure/PIDE/document.ML
changeset 43722 9b5dadb0c28d
parent 43713 1ba5331b4623
child 43761 e72ba84ae58f
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Jul 09 21:53:27 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Jul 10 00:21:19 2011 +0200
     1.3 @@ -16,12 +16,14 @@
     1.4    val parse_id: string -> id
     1.5    val print_id: id -> string
     1.6    type edit = string * ((command_id option * command_id option) list) option
     1.7 +  type header = string * (string * string list * string list)
     1.8    type state
     1.9    val init_state: state
    1.10    val get_theory: state -> version_id -> Position.T -> string -> theory
    1.11    val cancel_execution: state -> unit -> unit
    1.12    val define_command: command_id -> string -> state -> state
    1.13 -  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
    1.14 +  val edit: version_id -> version_id -> edit list -> header list ->
    1.15 +    state -> (command_id * exec_id) list * state
    1.16    val execute: version_id -> state -> state
    1.17    val state: unit -> state
    1.18    val change_state: (state -> state) -> unit
    1.19 @@ -78,6 +80,8 @@
    1.20    (*NONE: remove node, SOME: insert/remove commands*)
    1.21    ((command_id option * command_id option) list) option;
    1.22  
    1.23 +type header = string * (string * string list * string list);
    1.24 +
    1.25  fun the_entry (Node {entries, ...}) id =
    1.26    (case Entries.lookup entries id of
    1.27      NONE => err_undef "command entry" id
    1.28 @@ -309,8 +313,10 @@
    1.29  
    1.30  in
    1.31  
    1.32 -fun edit (old_id: version_id) (new_id: version_id) edits state =
    1.33 +fun edit (old_id: version_id) (new_id: version_id) edits headers state =
    1.34    let
    1.35 +    (* FIXME apply headers *)
    1.36 +
    1.37      val old_version = the_version state old_id;
    1.38      val _ = Time.now ();  (* FIXME odd workaround *)
    1.39      val new_version = fold edit_nodes edits old_version;