1.1 --- a/src/Pure/PIDE/document.ML	Sat Sep 03 19:39:16 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Sep 03 19:47:31 2011 +0200
     1.3 @@ -250,12 +250,8 @@
     1.4  fun map_state f (State {versions, commands, execution}) =
     1.5    make_state (f (versions, commands, execution));
     1.6  
     1.7 -val empty_commands =  (* FIXME no_id ??? *)
     1.8 -  Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))];
     1.9 -val empty_execution = (no_id, Future.new_group NONE);
    1.10 -
    1.11  val init_state =
    1.12 -  make_state (Inttab.make [(no_id, empty_version)], empty_commands, empty_execution);
    1.13 +  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE));
    1.14  
    1.15  
    1.16  (* document versions *)
    1.17 @@ -567,7 +563,7 @@
    1.18  
    1.19      val versions' = fold delete_version ids versions;
    1.20      val commands' =
    1.21 -      (versions', empty_commands) |->
    1.22 +      (versions', Inttab.empty) |->
    1.23          Inttab.fold (fn (_, version) => nodes_of version |>
    1.24            Graph.fold (fn (_, (node, _)) => node |>
    1.25              iterate_entries (fn ((_, id), _) =>