src/Pure/PIDE/document.ML

 sig
   val timing: bool Unsynchronized.ref
   type node_header = string * Thy_Header.header * string list
   type overlay = Document_ID.command * (string * string list)
   datatype node_edit =
-    Clear |    (* FIXME unused !? *)
     Edits of (Document_ID.command option * Document_ID.command option) list |
     Deps of node_header |
     Perspective of bool * Document_ID.command list * overlay list
   type edit = string * node_edit
   type state

 
 val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["No theory header"]);
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
-val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
 
 
 (* basic components *)
 
 fun master_directory (Node {header = (master, _, _), ...}) =

 (* node edits and associated executions *)
 
 type overlay = Document_ID.command * (string * string list);
 
 datatype node_edit =
-  Clear |
   Edits of (Document_ID.command option * Document_ID.command option) list |
   Deps of node_header |
   Perspective of bool * Document_ID.command list * overlay list;
 
 type edit = string * node_edit;

 fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
 
 fun edit_nodes (name, node_edit) (Version nodes) =
   Version
     (case node_edit of
-      Clear => update_node name clear_node nodes
-    | Edits edits => update_node name (edit_node edits) nodes
+      Edits edits => update_node name (edit_node edits) nodes
     | Deps (master, header, errors) =>
         let
           val imports = map fst (#imports header);
           val errors1 =
             (Thy_Header.define_keywords header; errors)