src/Pure/PIDE/command.ML
author wenzelm
Tue Apr 02 11:41:50 2013 +0200 (2013-04-02 ago)
changeset 51595 8e9746e584c9
parent 51589 8ea0a5dd5a35
child 51603 92fda7beace4
permissions -rw-r--r--
more centralized command timing;
clarified old-style timing message;
     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 run int tr st =
    65   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
    66     (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st);
    67       ([], SOME st))
    68   else Toplevel.command_errors int tr st;
    69 
    70 fun check_cmts tr cmts st =
    71   Toplevel.setmp_thread_position tr
    72     (fn () => cmts
    73       |> maps (fn cmt =>
    74         (Thy_Output.check_text (Token.source_position_of cmt) st; [])
    75           handle exn => ML_Compiler.exn_messages_ids exn)) ();
    76 
    77 fun proof_status tr st =
    78   (case try Toplevel.proof_of st of
    79     SOME prf => Toplevel.status tr (Proof.status_markup prf)
    80   | NONE => ());
    81 
    82 val no_print = Lazy.value ();
    83 
    84 fun print_state tr st =
    85   (Lazy.lazy o Toplevel.setmp_thread_position tr)
    86     (fn () => Toplevel.print_state false st);
    87 
    88 in
    89 
    90 fun run_command (tr, cmts) (st, malformed) =
    91   if malformed then ((Toplevel.toplevel, malformed), no_print)
    92   else
    93     let
    94       val malformed' = Toplevel.is_malformed tr;
    95       val is_init = Toplevel.is_init tr;
    96       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    97 
    98       val _ = Multithreading.interrupted ();
    99       val _ = Toplevel.status tr Markup.running;
   100       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   101       val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
   102       val errs = errs1 @ errs2;
   103       val _ = Toplevel.status tr Markup.finished;
   104       val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   105     in
   106       (case result of
   107         NONE =>
   108           let
   109             val _ = if null errs then Exn.interrupt () else ();
   110             val _ = Toplevel.status tr Markup.failed;
   111           in ((st, malformed'), no_print) end
   112       | SOME st' =>
   113           let
   114             val _ = proof_status tr st';
   115             val do_print =
   116               not is_init andalso
   117                 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   118           in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
   119     end;
   120 
   121 end;
   122 
   123 end;
   124