1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 05 16:01:45 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 05 16:22:28 2013 +0200
     1.3 @@ -26,6 +26,13 @@
     1.4    type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
     1.5    val print: string -> eval -> print list
     1.6    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
     1.7 +  type exec = Document_ID.exec * (eval * print list)
     1.8 +  val no_exec: exec
     1.9 +  val exec_ids: exec -> Document_ID.exec list
    1.10 +  val exec_result: exec -> eval_state
    1.11 +  val exec_run: exec -> unit
    1.12 +  val stable_eval: exec -> bool
    1.13 +  val stable_print: print -> bool
    1.14  end;
    1.15  
    1.16  structure Command: COMMAND =
    1.17 @@ -80,6 +87,8 @@
    1.18  end;
    1.19  
    1.20  
    1.21 +(** main phases: read -- eval -- print **)
    1.22 +
    1.23  (* read *)
    1.24  
    1.25  fun read span =
    1.26 @@ -233,5 +242,35 @@
    1.27            (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.28      in if do_print then Toplevel.print_state false st' else () end));
    1.29  
    1.30 +
    1.31 +
    1.32 +(** managed evaluation with potential interrupts **)
    1.33 +
    1.34 +(* execution *)
    1.35 +
    1.36 +type exec = Document_ID.exec * (eval * print list);
    1.37 +val no_exec: exec = (Document_ID.none, (no_eval, []));
    1.38 +
    1.39 +fun exec_ids ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    1.40 +
    1.41 +fun exec_result ((_, (eval, _)): exec) = memo_result eval;
    1.42 +
    1.43 +fun exec_run ((_, (eval, prints)): exec) =
    1.44 + (memo_eval eval;
    1.45 +  prints |> List.app (fn {name, pri, print, ...} =>
    1.46 +    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
    1.47 +
    1.48 +
    1.49 +(* stable situations *)
    1.50 +
    1.51 +fun stable_goals exec_id =
    1.52 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
    1.53 +
    1.54 +fun stable_eval ((exec_id, (eval, _)): exec) =
    1.55 +  stable_goals exec_id andalso memo_stable eval;
    1.56 +
    1.57 +fun stable_print ({exec_id, print, ...}: print) =
    1.58 +  stable_goals exec_id andalso memo_stable print;
    1.59 +
    1.60  end;
    1.61  

     2.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 16:01:45 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 16:22:28 2013 +0200
     2.3 @@ -31,22 +31,6 @@
     2.4  structure Document: DOCUMENT =
     2.5  struct
     2.6  
     2.7 -(* command execution *)
     2.8 -
     2.9 -type exec = Document_ID.exec * (Command.eval * Command.print list);  (*eval/print process*)
    2.10 -val no_exec: exec = (Document_ID.none, (Command.no_eval, []));
    2.11 -
    2.12 -fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    2.13 -
    2.14 -fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
    2.15 -
    2.16 -fun exec_run ((_, (eval, prints)): exec) =
    2.17 - (Command.memo_eval eval;
    2.18 -  prints |> List.app (fn {name, pri, print, ...} =>
    2.19 -    Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
    2.20 -
    2.21 -
    2.22 -
    2.23  (** document structure **)
    2.24  
    2.25  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
    2.26 @@ -59,7 +43,7 @@
    2.27  abstype node = Node of
    2.28   {header: node_header,  (*master directory, theory header, errors*)
    2.29    perspective: perspective,  (*visible commands, last visible command*)
    2.30 -  entries: exec option Entries.T * bool,  (*command entries with excecutions, stable*)
    2.31 +  entries: Command.exec option Entries.T * bool,  (*command entries with excecutions, stable*)
    2.32    result: Command.eval option}  (*result of last execution*)
    2.33  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    2.34  with
    2.35 @@ -152,8 +136,8 @@
    2.36      NONE => err_undef "command entry" id
    2.37    | SOME (exec, _) => exec);
    2.38  
    2.39 -fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
    2.40 -  | the_default_entry _ NONE = (Document_ID.none, no_exec);
    2.41 +fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
    2.42 +  | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
    2.43  
    2.44  fun update_entry id exec =
    2.45    map_entries (Entries.update (id, exec));
    2.46 @@ -291,17 +275,6 @@
    2.47    in (versions', commands', execution) end);
    2.48  
    2.49  
    2.50 -(* consolidated states *)
    2.51 -
    2.52 -fun stable_goals exec_id =
    2.53 -  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
    2.54 -
    2.55 -fun stable_eval ((exec_id, (eval, _)): exec) =
    2.56 -  stable_goals exec_id andalso Command.memo_stable eval;
    2.57 -
    2.58 -fun stable_print ({exec_id, print, ...}: Command.print) =
    2.59 -  stable_goals exec_id andalso Command.memo_stable print;
    2.60 -
    2.61  fun finished_theory node =
    2.62    (case Exn.capture (Command.memo_result o the) (get_result node) of
    2.63      Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
    2.64 @@ -334,7 +307,7 @@
    2.65                    (fn () =>
    2.66                      iterate_entries (fn (_, opt_exec) => fn () =>
    2.67                        (case opt_exec of
    2.68 -                        SOME exec => if ! running then SOME (exec_run exec) else NONE
    2.69 +                        SOME exec => if ! running then SOME (Command.exec_run exec) else NONE
    2.70                        | NONE => NONE)) node ()))));
    2.71    in () end;
    2.72  
    2.73 @@ -406,7 +379,8 @@
    2.74              | SOME (exec_id, exec) =>
    2.75                  (case lookup_entry node0 id of
    2.76                    NONE => false
    2.77 -                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec)));
    2.78 +                | SOME (exec_id0, _) =>
    2.79 +                    exec_id = exec_id0 andalso Command.stable_eval (exec_id, exec)));
    2.80          in SOME (same', (prev, flags')) end
    2.81        else NONE;
    2.82      val (same, (common, flags)) =
    2.83 @@ -434,7 +408,7 @@
    2.84        val eval' =
    2.85          Command.memo (fn () =>
    2.86            let
    2.87 -            val eval_state = exec_result (snd command_exec);
    2.88 +            val eval_state = Command.exec_result (snd command_exec);
    2.89              val tr =
    2.90                Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
    2.91                  (fn () =>
    2.92 @@ -455,7 +429,7 @@
    2.93          val prints' =
    2.94            new_prints |> map (fn new_print =>
    2.95              (case find_first (fn {name, ...} => name = #name new_print) prints of
    2.96 -              SOME print => if stable_print print then print else new_print
    2.97 +              SOME print => if Command.stable_print print then print else new_print
    2.98              | NONE => new_print));
    2.99        in
   2.100          if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
   2.101 @@ -548,7 +522,7 @@
   2.102  
   2.103      val command_execs =
   2.104        map (rpair []) (maps #1 updated) @
   2.105 -      map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated);
   2.106 +      map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated);
   2.107      val updated_nodes = map_filter #3 updated;
   2.108  
   2.109      val state' = state