src/Pure/PIDE/document.ML
changeset 38449 2eb6bad282b1
parent 38448 62d16c415019
child 38873 278f552b2e97
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 17 15:10:49 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 17 15:54:04 2010 +0200
     1.3 @@ -107,10 +107,10 @@
     1.4          |> Graph.default_node (name, empty_node)
     1.5          |> Graph.map_node name (fold edit_node edits))
     1.6    | edit_nodes (name, NONE) (Version nodes) =
     1.7 -      Version (Graph.del_node name nodes);  (* FIXME Graph.UNDEF !? *)
     1.8 +      Version (Graph.del_node name nodes);
     1.9  
    1.10  fun put_node name node (Version nodes) =
    1.11 -  Version (Graph.map_node name (K node) nodes);  (* FIXME Graph.UNDEF !? *)
    1.12 +  Version (Graph.map_node name (K node) nodes);
    1.13  
    1.14  end;
    1.15  
    1.16 @@ -133,8 +133,8 @@
    1.17  
    1.18  val init_state =
    1.19    make_state (Inttab.make [(no_id, empty_version)],
    1.20 -    Inttab.make [(no_id, Future.value Toplevel.empty)],          (* FIXME no_id !?? *)
    1.21 -    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],  (* FIXME no_id !?? *)
    1.22 +    Inttab.make [(no_id, Future.value Toplevel.empty)],
    1.23 +    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
    1.24      []);
    1.25  
    1.26  
    1.27 @@ -207,13 +207,13 @@
    1.28    let
    1.29      val exec = the_exec state exec_id;
    1.30      val exec_id' = new_id ();
    1.31 -    val tr = the_command state id;
    1.32 +    val future_tr = the_command state id;
    1.33      val exec' =
    1.34        Lazy.lazy (fn () =>
    1.35          (case Lazy.force exec of
    1.36            NONE => NONE
    1.37          | SOME st =>
    1.38 -            let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join tr)
    1.39 +            let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
    1.40              in Toplevel.run_command name exec_tr st end));
    1.41      val state' = define_exec exec_id' exec' state;
    1.42    in (exec_id', (id, exec_id') :: updates, state') end;