|
1 (* Title: Pure/PIDE/command.ML |
|
2 Author: Makarius |
|
3 |
|
4 Prover command execution. |
|
5 *) |
|
6 |
|
7 signature COMMAND = |
|
8 sig |
|
9 val parse_command: string -> string -> Token.T list |
|
10 val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy |
|
11 end; |
|
12 |
|
13 structure Command: COMMAND = |
|
14 struct |
|
15 |
|
16 (* parse *) |
|
17 |
|
18 fun parse_command id text = |
|
19 Position.setmp_thread_data (Position.id_only id) |
|
20 (fn () => |
|
21 let |
|
22 val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text; |
|
23 val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed); |
|
24 in toks end) (); |
|
25 |
|
26 |
|
27 (* run *) |
|
28 |
|
29 local |
|
30 |
|
31 fun run int tr st = |
|
32 (case Toplevel.transition int tr st of |
|
33 SOME (st', NONE) => ([], SOME st') |
|
34 | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) |
|
35 | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); |
|
36 |
|
37 fun timing tr t = |
|
38 if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else (); |
|
39 |
|
40 fun proof_status tr st = |
|
41 (case try Toplevel.proof_of st of |
|
42 SOME prf => Toplevel.status tr (Proof.status_markup prf) |
|
43 | NONE => ()); |
|
44 |
|
45 val no_print = Lazy.value (); |
|
46 |
|
47 fun print_state tr st = |
|
48 (Lazy.lazy o Toplevel.setmp_thread_position tr) |
|
49 (fn () => Toplevel.print_state false st); |
|
50 |
|
51 in |
|
52 |
|
53 fun run_command tr st = |
|
54 let |
|
55 val is_init = Toplevel.is_init tr; |
|
56 val is_proof = Keyword.is_proof (Toplevel.name_of tr); |
|
57 |
|
58 val _ = Multithreading.interrupted (); |
|
59 val _ = Toplevel.status tr Isabelle_Markup.forked; |
|
60 val start = Timing.start (); |
|
61 val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; |
|
62 val _ = timing tr (Timing.result start); |
|
63 val _ = Toplevel.status tr Isabelle_Markup.joined; |
|
64 val _ = List.app (Toplevel.error_msg tr) errs; |
|
65 in |
|
66 (case result of |
|
67 NONE => |
|
68 let |
|
69 val _ = if null errs then Exn.interrupt () else (); |
|
70 val _ = Toplevel.status tr Isabelle_Markup.failed; |
|
71 in (st, no_print) end |
|
72 | SOME st' => |
|
73 let |
|
74 val _ = Toplevel.status tr Isabelle_Markup.finished; |
|
75 val _ = proof_status tr st'; |
|
76 val do_print = |
|
77 not is_init andalso |
|
78 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); |
|
79 in (st', if do_print then print_state tr st' else no_print) end) |
|
80 end; |
|
81 |
|
82 end; |
|
83 |
|
84 end; |
|
85 |