src/Pure/PIDE/command.ML
changeset 56291 e79f76a48449
parent 56265 785569927666
child 56292 1a91a0da65ab
     1.1 --- a/src/Pure/PIDE/command.ML	Wed Mar 26 09:19:04 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Mar 26 12:15:42 2014 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4      eval -> print list -> print list option
     1.5    type print_fn = Toplevel.transition -> Toplevel.state -> unit
     1.6    type print_function =
     1.7 -    {command_name: string, args: string list} ->
     1.8 +    {command_name: string, args: string list, exec_id: Document_ID.exec} ->
     1.9        {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
    1.10    val print_function: string -> print_function -> unit
    1.11    val no_print_function: string -> unit
    1.12 @@ -172,9 +172,10 @@
    1.13  
    1.14  datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
    1.15  
    1.16 -fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.17 +fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
    1.18 +val eval_eq = op = o pairself eval_exec_id;
    1.19  
    1.20 -fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id;
    1.21 +val eval_running = Execution.is_running_exec o eval_exec_id;
    1.22  fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
    1.23  
    1.24  fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
    1.25 @@ -260,10 +261,13 @@
    1.26   {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
    1.27    exec_id: Document_ID.exec, print_process: unit memo};
    1.28  
    1.29 +fun print_exec_id (Print {exec_id, ...}) = exec_id;
    1.30 +val print_eq = op = o pairself print_exec_id;
    1.31 +
    1.32  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    1.33  
    1.34  type print_function =
    1.35 -  {command_name: string, args: string list} ->
    1.36 +  {command_name: string, args: string list, exec_id: Document_ID.exec} ->
    1.37      {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
    1.38  
    1.39  local
    1.40 @@ -277,8 +281,6 @@
    1.41        if Exn.is_interrupt exn then reraise exn
    1.42        else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
    1.43  
    1.44 -fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.45 -
    1.46  fun print_finished (Print {print_process, ...}) = memo_finished print_process;
    1.47  
    1.48  fun print_persistent (Print {persistent, ...}) = persistent;
    1.49 @@ -315,7 +317,7 @@
    1.50  
    1.51      fun new_print name args get_pr =
    1.52        let
    1.53 -        val params = {command_name = command_name, args = args};
    1.54 +        val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
    1.55        in
    1.56          (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
    1.57            Exn.Res NONE => NONE
    1.58 @@ -353,6 +355,14 @@
    1.59  end;
    1.60  
    1.61  val _ =
    1.62 +  print_function "Execution.print"
    1.63 +    (fn {args, exec_id, ...} =>
    1.64 +      if null args then
    1.65 +        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
    1.66 +          print_fn = fn _ => fn _ => Execution.apply_prints exec_id}
    1.67 +      else NONE);
    1.68 +
    1.69 +val _ =
    1.70    print_function "print_state"
    1.71      (fn {command_name, ...} =>
    1.72        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
    1.73 @@ -373,8 +383,7 @@
    1.74    (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    1.75  
    1.76  fun exec_ids NONE = []
    1.77 -  | exec_ids (SOME (Eval {exec_id, ...}, prints)) =
    1.78 -      exec_id :: map (fn Print {exec_id, ...} => exec_id) prints;
    1.79 +  | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
    1.80  
    1.81  local
    1.82