1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 15 20:38:16 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 21:05:30 2011 +0200
     1.3 @@ -123,7 +123,6 @@
     1.4  
     1.5  fun nodes_of (Version nodes) = nodes;
     1.6  val node_of = get_node o nodes_of;
     1.7 -val node_names_of = Graph.keys o nodes_of;
     1.8  
     1.9  fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
    1.10  
    1.11 @@ -324,19 +323,13 @@
    1.12      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
    1.13      val new_version = fold edit_nodes edits old_version;
    1.14  
    1.15 -    (* FIXME futures *)
    1.16      val updates =
    1.17        nodes_of new_version |> Graph.schedule
    1.18          (fn deps => fn (name, node) =>
    1.19            (case first_entry NONE (is_changed (node_of old_version name)) node of
    1.20 -            NONE => (([], [], []), node)
    1.21 +            NONE => Future.value (([], [], []), node)
    1.22            | SOME ((prev, id), _) =>
    1.23                let
    1.24 -                val prev_exec =
    1.25 -                  (case prev of
    1.26 -                    NONE => no_id
    1.27 -                  | SOME prev_id => the_default no_id (the_entry node prev_id));
    1.28 -
    1.29                  fun init () =
    1.30                    let
    1.31                      val (thy_name, imports, uses) = Exn.release (get_header node);
    1.32 @@ -347,21 +340,32 @@
    1.33                      val parents =
    1.34                        imports |> map (fn import =>
    1.35                          (case AList.lookup (op =) deps import of
    1.36 -                          SOME (_, parent_node) =>
    1.37 -                            get_theory (Position.file_only (import ^ ".thy")) parent_node
    1.38 +                          SOME parent_future =>
    1.39 +                            get_theory (Position.file_only (import ^ ".thy"))
    1.40 +                              (#2 (Future.join parent_future))
    1.41                          | NONE => Thy_Info.get_theory (Thy_Info.base_name import)));
    1.42                    in Thy_Load.begin_theory dir thy_name imports files parents end
    1.43                  fun get_command id =
    1.44                    (id, the_command state id |> Future.map (Toplevel.modify_init init));
    1.45 -
    1.46 -                val (assigns, execs, result) =
    1.47 -                  fold_entries (SOME id) (new_exec o get_command o #2 o #1)
    1.48 -                    node ([], [], the_exec state prev_exec);
    1.49 -                val node' = node
    1.50 -                  |> fold update_entry assigns
    1.51 -                  |> set_result result;
    1.52 -              in ((assigns, execs, [(name, node')]), node') end))
    1.53 -      |> map #1;
    1.54 +              in
    1.55 +                singleton
    1.56 +                  (Future.forks {name = "Document.edit", group = NONE,
    1.57 +                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
    1.58 +                  (fn () =>
    1.59 +                    let
    1.60 +                      val prev_exec =
    1.61 +                        (case prev of
    1.62 +                          NONE => no_id
    1.63 +                        | SOME prev_id => the_default no_id (the_entry node prev_id));
    1.64 +                      val (assigns, execs, result) =
    1.65 +                        fold_entries (SOME id) (new_exec o get_command o #2 o #1)
    1.66 +                          node ([], [], the_exec state prev_exec);
    1.67 +                      val node' = node
    1.68 +                        |> fold update_entry assigns
    1.69 +                        |> set_result result;
    1.70 +                    in ((assigns, execs, [(name, node')]), node') end)
    1.71 +              end))
    1.72 +      |> Future.join_results |> Exn.release_all |> map #1;
    1.73  
    1.74      val state' = state
    1.75        |> fold (fold define_exec o #2) updates
    1.76 @@ -382,13 +386,15 @@
    1.77        fun force_exec NONE = ()
    1.78          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
    1.79  
    1.80 -      val execution' = (* FIXME Graph.schedule *)
    1.81 -        Future.forks
    1.82 -          {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
    1.83 -          [fn () =>
    1.84 -            node_names_of version |> List.app (fn name =>
    1.85 -              fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
    1.86 -                  (node_of version name) ())];
    1.87 +      val execution' =
    1.88 +        nodes_of version |> Graph.schedule
    1.89 +          (fn deps => fn (name, node) =>
    1.90 +            singleton
    1.91 +              (Future.forks
    1.92 +                {name = "theory:" ^ name, group = NONE,
    1.93 +                  deps = map (Future.task_of o #2) deps,
    1.94 +                  pri = 1, interrupts = true})
    1.95 +              (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
    1.96  
    1.97      in (versions, commands, execs, execution') end);
    1.98