1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 05 22:09:16 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 05 22:58:24 2013 +0200
     1.3 @@ -8,19 +8,18 @@
     1.4  sig
     1.5    type eval_process
     1.6    type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
     1.7 +  val eval_result_state: eval -> Toplevel.state
     1.8    type print_process
     1.9    type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
    1.10    type exec = eval * print list
    1.11 +  val no_exec: exec
    1.12 +  val exec_ids: exec -> Document_ID.exec list
    1.13    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    1.14 -  val no_eval: eval
    1.15 -  val eval_result_state: eval -> Toplevel.state
    1.16    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.17    val print: string -> eval -> print list
    1.18    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.19    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    1.20 -  val no_exec: exec
    1.21 -  val exec_ids: exec -> Document_ID.exec list
    1.22 -  val exec_run: exec -> unit
    1.23 +  val execute: exec -> unit
    1.24    val stable_eval: eval -> bool
    1.25    val stable_print: print -> bool
    1.26  end;
    1.27 @@ -70,16 +69,29 @@
    1.28  
    1.29  
    1.30  
    1.31 -(** main phases **)
    1.32 +(** main phases of execution **)
    1.33 +
    1.34 +(* basic type definitions *)
    1.35  
    1.36  type eval_state =
    1.37    {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
    1.38 +val init_eval_state =
    1.39 +  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    1.40 +
    1.41  type eval_process = eval_state memo;
    1.42  type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
    1.43  
    1.44 +fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
    1.45 +val eval_result_state = #state o eval_result;
    1.46 +
    1.47  type print_process = unit memo;
    1.48  type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
    1.49  
    1.50 +type exec = eval * print list;
    1.51 +val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    1.52 +
    1.53 +fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
    1.54 +
    1.55  
    1.56  (* read *)
    1.57  
    1.58 @@ -113,14 +125,6 @@
    1.59  
    1.60  (* eval *)
    1.61  
    1.62 -val no_eval_state: eval_state =
    1.63 -  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    1.64 -
    1.65 -val no_eval: eval = {exec_id = Document_ID.none, eval_process = memo_value no_eval_state};
    1.66 -
    1.67 -fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
    1.68 -val eval_result_state = #state o eval_result;
    1.69 -
    1.70  local
    1.71  
    1.72  fun run int tr st =
    1.73 @@ -179,7 +183,7 @@
    1.74        let
    1.75          val tr =
    1.76            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
    1.77 -            (fn () => read init span |> Toplevel.put_id exec_id) ();
    1.78 +            (fn () => read init span |> Toplevel.exec_id exec_id) ();
    1.79        in eval_state span tr (eval_result eval0) end;
    1.80    in {exec_id = exec_id, eval_process = memo process} end;
    1.81  
    1.82 @@ -214,7 +218,7 @@
    1.83            fun process () =
    1.84              let
    1.85                val {failed, command, state = st', ...} = eval_result eval;
    1.86 -              val tr = Toplevel.put_id exec_id command;
    1.87 +              val tr = Toplevel.exec_id exec_id command;
    1.88              in if failed then () else print_error tr (fn () => print_fn tr st') () end;
    1.89          in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
    1.90      | Exn.Exn exn =>
    1.91 @@ -223,7 +227,7 @@
    1.92            fun process () =
    1.93              let
    1.94                val {command, ...} = eval_result eval;
    1.95 -              val tr = Toplevel.put_id exec_id command;
    1.96 +              val tr = Toplevel.exec_id exec_id command;
    1.97              in output_error tr exn end;
    1.98          in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
    1.99  
   1.100 @@ -246,24 +250,13 @@
   1.101      in if do_print then Toplevel.print_state false st' else () end));
   1.102  
   1.103  
   1.104 +(* overall execution process *)
   1.105  
   1.106 -(** managed evaluation **)
   1.107 -
   1.108 -(* execution *)
   1.109 -
   1.110 -type exec = eval * print list;
   1.111 -val no_exec: exec = (no_eval, []);
   1.112 -
   1.113 -fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
   1.114 -
   1.115 -fun exec_run (({eval_process, ...}, prints): exec) =
   1.116 +fun execute (({eval_process, ...}, prints): exec) =
   1.117   (memo_eval eval_process;
   1.118    prints |> List.app (fn {name, pri, print_process, ...} =>
   1.119      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
   1.120  
   1.121 -
   1.122 -(* stable situations after cancellation *)
   1.123 -
   1.124  fun stable_goals exec_id =
   1.125    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
   1.126