src/Pure/PIDE/command.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 47395 e6261a493f04
child 48771 2ea997196d04
permissions -rw-r--r--
more official command specifications, including source position;
     1 (*  Title:      Pure/PIDE/command.ML
     2     Author:     Makarius
     3 
     4 Prover command execution.
     5 *)
     6 
     7 signature COMMAND =
     8 sig
     9   type 'a memo
    10   val memo: (unit -> 'a) -> 'a memo
    11   val memo_value: 'a -> 'a memo
    12   val memo_eval: 'a memo -> 'a
    13   val memo_result: 'a memo -> 'a
    14   val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
    15 end;
    16 
    17 structure Command: COMMAND =
    18 struct
    19 
    20 (* memo results *)
    21 
    22 datatype 'a expr =
    23   Expr of unit -> 'a |
    24   Result of 'a Exn.result;
    25 
    26 abstype 'a memo = Memo of 'a expr Synchronized.var
    27 with
    28 
    29 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    30 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    31 
    32 fun memo_eval (Memo v) =
    33   (case Synchronized.value v of
    34     Result res => res
    35   | _ =>
    36       Synchronized.guarded_access v
    37         (fn Result res => SOME (res, Result res)
    38           | Expr e =>
    39               let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
    40               in SOME (res, Result res) end))
    41   |> Exn.release;
    42 
    43 fun memo_result (Memo v) =
    44   (case Synchronized.value v of
    45     Result res => Exn.release res
    46   | _ => raise Fail "Unfinished memo result");
    47 
    48 end;
    49 
    50 
    51 (* run command *)
    52 
    53 local
    54 
    55 fun run int tr st =
    56   (case Toplevel.transition int tr st of
    57     SOME (st', NONE) => ([], SOME st')
    58   | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
    59   | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
    60 
    61 fun timing tr t =
    62   if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
    63 
    64 fun proof_status tr st =
    65   (case try Toplevel.proof_of st of
    66     SOME prf => Toplevel.status tr (Proof.status_markup prf)
    67   | NONE => ());
    68 
    69 val no_print = Lazy.value ();
    70 
    71 fun print_state tr st =
    72   (Lazy.lazy o Toplevel.setmp_thread_position tr)
    73     (fn () => Toplevel.print_state false st);
    74 
    75 in
    76 
    77 fun run_command tr st =
    78   let
    79     val is_init = Toplevel.is_init tr;
    80     val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    81 
    82     val _ = Multithreading.interrupted ();
    83     val _ = Toplevel.status tr Isabelle_Markup.forked;
    84     val start = Timing.start ();
    85     val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    86     val _ = timing tr (Timing.result start);
    87     val _ = Toplevel.status tr Isabelle_Markup.joined;
    88     val _ = List.app (Toplevel.error_msg tr) errs;
    89   in
    90     (case result of
    91       NONE =>
    92         let
    93           val _ = if null errs then Exn.interrupt () else ();
    94           val _ = Toplevel.status tr Isabelle_Markup.failed;
    95         in (st, no_print) end
    96     | SOME st' =>
    97         let
    98           val _ = Toplevel.status tr Isabelle_Markup.finished;
    99           val _ = proof_status tr st';
   100           val do_print =
   101             not is_init andalso
   102               (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   103         in (st', if do_print then print_state tr st' else no_print) end)
   104   end;
   105 
   106 end;
   107 
   108 end;
   109