src/Pure/PIDE/command.ML
author wenzelm
Thu Dec 13 18:00:24 2012 +0100 (2012-12-13 ago)
changeset 50503 50f141b34bb7
parent 50201 c26369c9eda6
child 50911 ee7fe4230642
permissions -rw-r--r--
enable Isabelle/ML to produce uninterpreted result messages as well;
     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_space;
    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   (case Toplevel.transition int tr st of
    66     SOME (st', NONE) => ([], SOME st')
    67   | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
    68   | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
    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 exn)) ();
    76 
    77 fun timing tr t =
    78   if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
    79 
    80 fun proof_status tr st =
    81   (case try Toplevel.proof_of st of
    82     SOME prf => Toplevel.status tr (Proof.status_markup prf)
    83   | NONE => ());
    84 
    85 val no_print = Lazy.value ();
    86 
    87 fun print_state tr st =
    88   (Lazy.lazy o Toplevel.setmp_thread_position tr)
    89     (fn () => Toplevel.print_state false st);
    90 
    91 in
    92 
    93 fun run_command (tr, cmts) (st, malformed) =
    94   if malformed then ((Toplevel.toplevel, malformed), no_print)
    95   else
    96     let
    97       val malformed' = Toplevel.is_malformed tr;
    98       val is_init = Toplevel.is_init tr;
    99       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   100 
   101       val _ = Multithreading.interrupted ();
   102       val _ = Toplevel.status tr Markup.running;
   103       val start = Timing.start ();
   104       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   105       val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
   106       val errs = errs1 @ errs2;
   107       val _ = timing tr (Timing.result start);
   108       val _ = Toplevel.status tr Markup.finished;
   109       val _ = List.app (Toplevel.error_msg tr) errs;
   110     in
   111       (case result of
   112         NONE =>
   113           let
   114             val _ = if null errs then Exn.interrupt () else ();
   115             val _ = Toplevel.status tr Markup.failed;
   116           in ((st, malformed'), no_print) end
   117       | SOME st' =>
   118           let
   119             val _ = proof_status tr st';
   120             val do_print =
   121               not is_init andalso
   122                 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   123           in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
   124     end;
   125 
   126 end;
   127 
   128 end;
   129