src/Pure/PIDE/document.ML
changeset 44156 6aa25b80e1a5
parent 44113 0baa8bbd355a
child 44157 a21d3e1e64fd
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 11 13:24:49 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 11 18:01:28 2011 +0200
     1.3 @@ -15,7 +15,8 @@
     1.4    val new_id: unit -> id
     1.5    val parse_id: string -> id
     1.6    val print_id: id -> string
     1.7 -  type edit = string * ((command_id option * command_id option) list) option
     1.8 +  datatype node_edit = Remove | Edits of (command_id option * command_id option) list
     1.9 +  type edit = string * node_edit
    1.10    type header = string * (string * string list * string list)
    1.11    type state
    1.12    val init_state: state
    1.13 @@ -75,10 +76,8 @@
    1.14  
    1.15  (* node edits and associated executions *)
    1.16  
    1.17 -type edit =
    1.18 -  string *
    1.19 -  (*NONE: remove node, SOME: insert/remove commands*)
    1.20 -  ((command_id option * command_id option) list) option;
    1.21 +datatype node_edit = Remove | Edits of (command_id option * command_id option) list;
    1.22 +type edit = string * node_edit;
    1.23  
    1.24  type header = string * (string * string list * string list);
    1.25  
    1.26 @@ -108,12 +107,12 @@
    1.27  fun get_node version name = Graph.get_node (nodes_of version) name
    1.28    handle Graph.UNDEF _ => empty_node;
    1.29  
    1.30 -fun edit_nodes (name, SOME edits) (Version nodes) =
    1.31 +fun edit_nodes (name, Remove) (Version nodes) =
    1.32 +      Version (perhaps (try (Graph.del_node name)) nodes)
    1.33 +  | edit_nodes (name, Edits edits) (Version nodes) =
    1.34        Version (nodes
    1.35          |> Graph.default_node (name, empty_node)
    1.36 -        |> Graph.map_node name (edit_node edits))
    1.37 -  | edit_nodes (name, NONE) (Version nodes) =
    1.38 -      Version (perhaps (try (Graph.del_node name)) nodes);
    1.39 +        |> Graph.map_node name (edit_node edits));
    1.40  
    1.41  fun put_node name node (Version nodes) =
    1.42    Version (nodes