src/Pure/PIDE/command.ML
changeset 52761 909167fdd367
parent 52713 cd3ce844248f
child 52762 c2a6e220f157
equal deleted inserted replaced
52760:8517172b9626 52761:909167fdd367
     8 sig
     8 sig
     9   val read: (unit -> theory) -> Token.T list -> Toplevel.transition
     9   val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    10   type eval
    10   type eval
    11   val eval_eq: eval * eval -> bool
    11   val eval_eq: eval * eval -> bool
    12   val eval_result_state: eval -> Toplevel.state
    12   val eval_result_state: eval -> Toplevel.state
    13   val eval_stable: eval -> bool
       
    14   val eval: (unit -> theory) -> Token.T list -> eval -> eval
    13   val eval: (unit -> theory) -> Token.T list -> eval -> eval
    15   type print
    14   type print
    16   val print: bool -> string -> eval -> print list -> print list option
    15   val print: bool -> string -> eval -> print list -> print list option
    17   type print_fn = Toplevel.transition -> Toplevel.state -> unit
    16   type print_fn = Toplevel.transition -> Toplevel.state -> unit
    18   val print_function: string ->
    17   val print_function: string ->
    26 end;
    25 end;
    27 
    26 
    28 structure Command: COMMAND =
    27 structure Command: COMMAND =
    29 struct
    28 struct
    30 
    29 
    31 (** memo results -- including physical interrupts! **)
    30 (** memo results -- including physical interrupts **)
    32 
    31 
    33 datatype 'a expr =
    32 datatype 'a expr =
    34   Expr of Document_ID.exec * (unit -> 'a) |
    33   Expr of Document_ID.exec * (unit -> 'a) |
    35   Result of 'a Exn.result;
    34   Result of 'a Exn.result;
    36 
    35 
    42 
    41 
    43 fun memo_result (Memo v) =
    42 fun memo_result (Memo v) =
    44   (case Synchronized.value v of
    43   (case Synchronized.value v of
    45     Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
    44     Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
    46   | Result res => Exn.release res);
    45   | Result res => Exn.release res);
    47 
       
    48 fun memo_stable (Memo v) =
       
    49   (case Synchronized.value v of
       
    50    Expr _ => true
       
    51  | Result res => not (Exn.is_interrupt_exn res));
       
    52 
    46 
    53 fun memo_finished (Memo v) =
    47 fun memo_finished (Memo v) =
    54   (case Synchronized.value v of
    48   (case Synchronized.value v of
    55    Expr _ => false
    49    Expr _ => false
    56  | Result res => not (Exn.is_interrupt_exn res));
    50  | Result res => not (Exn.is_interrupt_exn res));
   122 
   116 
   123 fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
   117 fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
   124 
   118 
   125 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
   119 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
   126 val eval_result_state = #state o eval_result;
   120 val eval_result_state = #state o eval_result;
   127 
       
   128 fun eval_stable (Eval {exec_id, eval_process}) =
       
   129   Goal.stable_futures exec_id andalso memo_stable eval_process;
       
   130 
   121 
   131 local
   122 local
   132 
   123 
   133 fun run int tr st =
   124 fun run int tr st =
   134   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
   125   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
   218       if Exn.is_interrupt exn then reraise exn
   209       if Exn.is_interrupt exn then reraise exn
   219       else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   210       else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   220 
   211 
   221 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
   212 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
   222 
   213 
   223 fun print_stable (Print {exec_id, print_process, ...}) =
   214 fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process;
   224   Goal.stable_futures exec_id andalso memo_stable print_process;
       
   225 
       
   226 fun print_finished (Print {exec_id, print_process, ...}) =
       
   227   Goal.stable_futures exec_id andalso memo_finished print_process;
       
   228 
   215 
   229 fun print_persistent (Print {persistent, ...}) = persistent;
   216 fun print_persistent (Print {persistent, ...}) = persistent;
   230 
   217 
   231 in
   218 in
   232 
   219 
   262 
   249 
   263     val new_prints =
   250     val new_prints =
   264       if command_visible then
   251       if command_visible then
   265         rev (Synchronized.value print_functions) |> map_filter (fn pr =>
   252         rev (Synchronized.value print_functions) |> map_filter (fn pr =>
   266           (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
   253           (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
   267             SOME print => if print_stable print then SOME print else new_print pr
   254             NONE => new_print pr
   268           | NONE => new_print pr))
   255           | some => some))
   269       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   256       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   270   in
   257   in
   271     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   258     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   272   end;
   259   end;
   273 
   260