# HG changeset patch
# User wenzelm
# Date 1315072051 -7200
# Node ID f665a5d35a3de59f27d140433a8f7b01e9c0e098
# Parent  bad4f9158c80b9b11f78c0ed3e7bd579c344b26c
discontinued predefined empty command (obsolete!?);

diff -r bad4f9158c80 -r f665a5d35a3d src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Sep 03 19:39:16 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Sep 03 19:47:31 2011 +0200
@@ -250,12 +250,8 @@
 fun map_state f (State {versions, commands, execution}) =
   make_state (f (versions, commands, execution));
 
-val empty_commands =  (* FIXME no_id ??? *)
-  Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))];
-val empty_execution = (no_id, Future.new_group NONE);
-
 val init_state =
-  make_state (Inttab.make [(no_id, empty_version)], empty_commands, empty_execution);
+  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE));
 
 
 (* document versions *)
@@ -567,7 +563,7 @@
 
     val versions' = fold delete_version ids versions;
     val commands' =
-      (versions', empty_commands) |->
+      (versions', Inttab.empty) |->
         Inttab.fold (fn (_, version) => nodes_of version |>
           Graph.fold (fn (_, (node, _)) => node |>
             iterate_entries (fn ((_, id), _) =>