1.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 16:01:45 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 16:22:28 2013 +0200
     1.3 @@ -31,22 +31,6 @@
     1.4  structure Document: DOCUMENT =
     1.5  struct
     1.6  
     1.7 -(* command execution *)
     1.8 -
     1.9 -type exec = Document_ID.exec * (Command.eval * Command.print list);  (*eval/print process*)
    1.10 -val no_exec: exec = (Document_ID.none, (Command.no_eval, []));
    1.11 -
    1.12 -fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    1.13 -
    1.14 -fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
    1.15 -
    1.16 -fun exec_run ((_, (eval, prints)): exec) =
    1.17 - (Command.memo_eval eval;
    1.18 -  prints |> List.app (fn {name, pri, print, ...} =>
    1.19 -    Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
    1.20 -
    1.21 -
    1.22 -
    1.23  (** document structure **)
    1.24  
    1.25  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
    1.26 @@ -59,7 +43,7 @@
    1.27  abstype node = Node of
    1.28   {header: node_header,  (*master directory, theory header, errors*)
    1.29    perspective: perspective,  (*visible commands, last visible command*)
    1.30 -  entries: exec option Entries.T * bool,  (*command entries with excecutions, stable*)
    1.31 +  entries: Command.exec option Entries.T * bool,  (*command entries with excecutions, stable*)
    1.32    result: Command.eval option}  (*result of last execution*)
    1.33  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    1.34  with
    1.35 @@ -152,8 +136,8 @@
    1.36      NONE => err_undef "command entry" id
    1.37    | SOME (exec, _) => exec);
    1.38  
    1.39 -fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
    1.40 -  | the_default_entry _ NONE = (Document_ID.none, no_exec);
    1.41 +fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
    1.42 +  | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
    1.43  
    1.44  fun update_entry id exec =
    1.45    map_entries (Entries.update (id, exec));
    1.46 @@ -291,17 +275,6 @@
    1.47    in (versions', commands', execution) end);
    1.48  
    1.49  
    1.50 -(* consolidated states *)
    1.51 -
    1.52 -fun stable_goals exec_id =
    1.53 -  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
    1.54 -
    1.55 -fun stable_eval ((exec_id, (eval, _)): exec) =
    1.56 -  stable_goals exec_id andalso Command.memo_stable eval;
    1.57 -
    1.58 -fun stable_print ({exec_id, print, ...}: Command.print) =
    1.59 -  stable_goals exec_id andalso Command.memo_stable print;
    1.60 -
    1.61  fun finished_theory node =
    1.62    (case Exn.capture (Command.memo_result o the) (get_result node) of
    1.63      Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
    1.64 @@ -334,7 +307,7 @@
    1.65                    (fn () =>
    1.66                      iterate_entries (fn (_, opt_exec) => fn () =>
    1.67                        (case opt_exec of
    1.68 -                        SOME exec => if ! running then SOME (exec_run exec) else NONE
    1.69 +                        SOME exec => if ! running then SOME (Command.exec_run exec) else NONE
    1.70                        | NONE => NONE)) node ()))));
    1.71    in () end;
    1.72  
    1.73 @@ -406,7 +379,8 @@
    1.74              | SOME (exec_id, exec) =>
    1.75                  (case lookup_entry node0 id of
    1.76                    NONE => false
    1.77 -                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec)));
    1.78 +                | SOME (exec_id0, _) =>
    1.79 +                    exec_id = exec_id0 andalso Command.stable_eval (exec_id, exec)));
    1.80          in SOME (same', (prev, flags')) end
    1.81        else NONE;
    1.82      val (same, (common, flags)) =
    1.83 @@ -434,7 +408,7 @@
    1.84        val eval' =
    1.85          Command.memo (fn () =>
    1.86            let
    1.87 -            val eval_state = exec_result (snd command_exec);
    1.88 +            val eval_state = Command.exec_result (snd command_exec);
    1.89              val tr =
    1.90                Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
    1.91                  (fn () =>
    1.92 @@ -455,7 +429,7 @@
    1.93          val prints' =
    1.94            new_prints |> map (fn new_print =>
    1.95              (case find_first (fn {name, ...} => name = #name new_print) prints of
    1.96 -              SOME print => if stable_print print then print else new_print
    1.97 +              SOME print => if Command.stable_print print then print else new_print
    1.98              | NONE => new_print));
    1.99        in
   1.100          if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
   1.101 @@ -548,7 +522,7 @@
   1.102  
   1.103      val command_execs =
   1.104        map (rpair []) (maps #1 updated) @
   1.105 -      map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated);
   1.106 +      map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated);
   1.107      val updated_nodes = map_filter #3 updated;
   1.108  
   1.109      val state' = state