src/Pure/PIDE/command.ML
author wenzelm
Sat Mar 30 16:34:02 2013 +0100 (2013-03-30 ago)
changeset 51589 8ea0a5dd5a35
parent 51284 59a03019f3bf
child 51595 8e9746e584c9
permissions -rw-r--r--
timing status for forked diagnostic commands;
     1 (*  Title:      Pure/PIDE/command.ML
     2     Author:     Makarius
     3 
     4 Prover command execution.
     5 *)
     6 
     7 signature COMMAND =
     8 sig
     9   val range: Token.T list -> Position.range
    10   val proper_range: Token.T list -> Position.range
    11   type 'a memo
    12   val memo: (unit -> 'a) -> 'a memo
    13   val memo_value: 'a -> 'a memo
    14   val memo_eval: 'a memo -> 'a
    15   val memo_result: 'a memo -> 'a
    16   val run_command: Toplevel.transition * Token.T list ->
    17     Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
    18 end;
    19 
    20 structure Command: COMMAND =
    21 struct
    22 
    23 (* span range *)
    24 
    25 val range = Token.position_range_of;
    26 val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
    27 
    28 
    29 (* memo results *)
    30 
    31 datatype 'a expr =
    32   Expr of unit -> 'a |
    33   Result of 'a Exn.result;
    34 
    35 abstype 'a memo = Memo of 'a expr Synchronized.var
    36 with
    37 
    38 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    39 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    40 
    41 fun memo_eval (Memo v) =
    42   (case Synchronized.value v of
    43     Result res => res
    44   | _ =>
    45       Synchronized.guarded_access v
    46         (fn Result res => SOME (res, Result res)
    47           | Expr e =>
    48               let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
    49               in SOME (res, Result res) end))
    50   |> Exn.release;
    51 
    52 fun memo_result (Memo v) =
    53   (case Synchronized.value v of
    54     Result res => Exn.release res
    55   | _ => raise Fail "Unfinished memo result");
    56 
    57 end;
    58 
    59 
    60 (* run command *)
    61 
    62 local
    63 
    64 fun timing tr t =
    65   if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
    66 
    67 fun run int tr st =
    68   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
    69     Toplevel.setmp_thread_position tr (fn () =>
    70       (Goal.fork_name "Toplevel.diag" ~1
    71         (fn () =>
    72           let
    73             val start = Timing.start ();
    74             val res = Exn.interruptible_capture (fn () => Toplevel.command_exception int tr st) ();
    75             val _ = timing tr (Timing.result start);
    76           in Exn.release res end); ([], SOME st))) ()
    77   else Toplevel.command_errors int tr st;
    78 
    79 fun check_cmts tr cmts st =
    80   Toplevel.setmp_thread_position tr
    81     (fn () => cmts
    82       |> maps (fn cmt =>
    83         (Thy_Output.check_text (Token.source_position_of cmt) st; [])
    84           handle exn => ML_Compiler.exn_messages_ids exn)) ();
    85 
    86 fun proof_status tr st =
    87   (case try Toplevel.proof_of st of
    88     SOME prf => Toplevel.status tr (Proof.status_markup prf)
    89   | NONE => ());
    90 
    91 val no_print = Lazy.value ();
    92 
    93 fun print_state tr st =
    94   (Lazy.lazy o Toplevel.setmp_thread_position tr)
    95     (fn () => Toplevel.print_state false st);
    96 
    97 in
    98 
    99 fun run_command (tr, cmts) (st, malformed) =
   100   if malformed then ((Toplevel.toplevel, malformed), no_print)
   101   else
   102     let
   103       val malformed' = Toplevel.is_malformed tr;
   104       val is_init = Toplevel.is_init tr;
   105       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   106 
   107       val _ = Multithreading.interrupted ();
   108       val _ = Toplevel.status tr Markup.running;
   109       val start = Timing.start ();
   110       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   111       val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
   112       val errs = errs1 @ errs2;
   113       val _ = timing tr (Timing.result start);
   114       val _ = Toplevel.status tr Markup.finished;
   115       val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   116     in
   117       (case result of
   118         NONE =>
   119           let
   120             val _ = if null errs then Exn.interrupt () else ();
   121             val _ = Toplevel.status tr Markup.failed;
   122           in ((st, malformed'), no_print) end
   123       | SOME st' =>
   124           let
   125             val _ = proof_status tr st';
   126             val do_print =
   127               not is_init andalso
   128                 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   129           in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
   130     end;
   131 
   132 end;
   133 
   134 end;
   135