src/Pure/PIDE/command.ML
changeset 68184 6c693b2700b3
parent 68130 6fb85346cb79
child 68333 82dcd0d87fb1
     1.1 --- a/src/Pure/PIDE/command.ML	Mon May 14 22:01:00 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon May 14 22:22:47 2018 +0200
     1.3 @@ -12,13 +12,15 @@
     1.4    val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     1.5      blob list * int -> Token.T list -> Toplevel.transition
     1.6    type eval
     1.7 +  val eval_command_id: eval -> Document_ID.command
     1.8    val eval_exec_id: eval -> Document_ID.exec
     1.9    val eval_eq: eval * eval -> bool
    1.10    val eval_running: eval -> bool
    1.11    val eval_finished: eval -> bool
    1.12 +  val eval_result_command: eval -> Toplevel.transition
    1.13    val eval_result_state: eval -> Toplevel.state
    1.14    val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
    1.15 -    blob list * int -> Token.T list -> eval -> eval
    1.16 +    blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
    1.17    type print
    1.18    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    1.19      eval -> print list -> print list option
    1.20 @@ -161,7 +163,11 @@
    1.21    command = Toplevel.empty,
    1.22    state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)};
    1.23  
    1.24 -datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
    1.25 +datatype eval =
    1.26 +  Eval of
    1.27 +    {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy};
    1.28 +
    1.29 +fun eval_command_id (Eval {command_id, ...}) = command_id;
    1.30  
    1.31  fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
    1.32  val eval_eq = op = o apply2 eval_exec_id;
    1.33 @@ -172,6 +178,7 @@
    1.34  fun eval_result (Eval {eval_process, ...}) =
    1.35    task_context (Future.worker_subgroup ()) Lazy.force eval_process;
    1.36  
    1.37 +val eval_result_command = #command o eval_result;
    1.38  val eval_result_state = #state o eval_result;
    1.39  
    1.40  local
    1.41 @@ -259,7 +266,7 @@
    1.42  
    1.43  in
    1.44  
    1.45 -fun eval keywords master_dir init blobs_info span eval0 =
    1.46 +fun eval keywords master_dir init blobs_info command_id span eval0 =
    1.47    let
    1.48      val exec_id = Document_ID.make ();
    1.49      fun process () =
    1.50 @@ -271,7 +278,9 @@
    1.51              (fn () =>
    1.52                read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
    1.53        in eval_state keywords span tr eval_state0 end;
    1.54 -  in Eval {exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end;
    1.55 +  in
    1.56 +    Eval {command_id = command_id, exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process}
    1.57 +  end;
    1.58  
    1.59  end;
    1.60  
    1.61 @@ -404,7 +413,9 @@
    1.62  type exec = eval * print list;
    1.63  
    1.64  fun init_exec opt_thy : exec =
    1.65 -  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []);
    1.66 +  (Eval
    1.67 +    {command_id = Document_ID.none, exec_id = Document_ID.none,
    1.68 +      eval_process = Lazy.value (init_eval_state opt_thy)}, []);
    1.69  
    1.70  val no_exec = init_exec NONE;
    1.71  
    1.72 @@ -423,7 +434,7 @@
    1.73  fun ignore_process process =
    1.74    Lazy.is_running process orelse Lazy.is_finished process;
    1.75  
    1.76 -fun run_eval execution_id (Eval {exec_id, eval_process}) =
    1.77 +fun run_eval execution_id (Eval {exec_id, eval_process, ...}) =
    1.78    if Lazy.is_finished eval_process then ()
    1.79    else run_process execution_id exec_id eval_process;
    1.80