src/Pure/PIDE/document.ML
changeset 54562 301a721af68b
parent 54558 31844ca390ad
child 55788 67699e08e969
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Nov 22 20:54:26 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Nov 22 21:13:44 2013 +0100
     1.3 @@ -11,7 +11,6 @@
     1.4    type node_header = string * Thy_Header.header * string list
     1.5    type overlay = Document_ID.command * (string * string list)
     1.6    datatype node_edit =
     1.7 -    Clear |    (* FIXME unused !? *)
     1.8      Edits of (Document_ID.command option * Document_ID.command option) list |
     1.9      Deps of node_header |
    1.10      Perspective of bool * Document_ID.command list * overlay list
    1.11 @@ -76,7 +75,6 @@
    1.12  val no_perspective = make_perspective (false, [], []);
    1.13  
    1.14  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.15 -val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
    1.16  
    1.17  
    1.18  (* basic components *)
    1.19 @@ -145,7 +143,6 @@
    1.20  type overlay = Document_ID.command * (string * string list);
    1.21  
    1.22  datatype node_edit =
    1.23 -  Clear |
    1.24    Edits of (Document_ID.command option * Document_ID.command option) list |
    1.25    Deps of node_header |
    1.26    Perspective of bool * Document_ID.command list * overlay list;
    1.27 @@ -193,8 +190,7 @@
    1.28  fun edit_nodes (name, node_edit) (Version nodes) =
    1.29    Version
    1.30      (case node_edit of
    1.31 -      Clear => update_node name clear_node nodes
    1.32 -    | Edits edits => update_node name (edit_node edits) nodes
    1.33 +      Edits edits => update_node name (edit_node edits) nodes
    1.34      | Deps (master, header, errors) =>
    1.35          let
    1.36            val imports = map fst (#imports header);