--- 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), _) =>