1 (* Title: Pure/PIDE/command.ML
4 Prover command execution.
9 type span = Token.T list
10 val range: span -> Position.range
11 val proper_range: span -> Position.range
13 val memo: (unit -> 'a) -> 'a memo
14 val memo_value: 'a -> 'a memo
15 val memo_eval: 'a memo -> 'a
16 val memo_result: 'a memo -> 'a
17 val eval: span -> Toplevel.transition ->
18 Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
19 val no_print: unit lazy
20 val print: Toplevel.transition -> Toplevel.state -> unit lazy
23 structure Command: COMMAND =
28 type span = Token.T list;
30 val range = Token.position_range_of;
31 val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
38 Result of 'a Exn.result;
40 abstype 'a memo = Memo of 'a expr Synchronized.var
43 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
44 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
46 fun memo_eval (Memo v) =
47 (case Synchronized.value v of
50 Synchronized.guarded_access v
51 (fn Result res => SOME (res, Result res)
53 let val res = Exn.capture e (); (*memoing of physical interrupts!*)
54 in SOME (res, Result res) end))
57 fun memo_result (Memo v) =
58 (case Synchronized.value v of
59 Result res => Exn.release res
60 | _ => raise Fail "Unfinished memo result");
69 fun cmts (t1 :: t2 :: toks) =
70 if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
71 else cmts (t2 :: toks)
74 val span_cmts = filter Token.is_proper #> cmts;
78 fun check_cmts span tr st' =
79 Toplevel.setmp_thread_position tr
81 span_cmts span |> maps (fn cmt =>
82 (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
83 handle exn => ML_Compiler.exn_messages_ids exn)) ();
93 if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
94 (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
95 (fn () => Toplevel.command_exception int tr st); ([], SOME st))
96 else Toplevel.command_errors int tr st;
98 fun proof_status tr st =
99 (case try Toplevel.proof_of st of
100 SOME prf => Toplevel.status tr (Proof.status_markup prf)
105 fun eval span tr (st, {malformed}) =
107 ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
110 val malformed' = Toplevel.is_malformed tr;
111 val is_init = Toplevel.is_init tr;
112 val is_proof = Keyword.is_proof (Toplevel.name_of tr);
114 val _ = Multithreading.interrupted ();
115 val _ = Toplevel.status tr Markup.running;
116 val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
117 val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
118 val errs = errs1 @ errs2;
119 val _ = Toplevel.status tr Markup.finished;
120 val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
125 val _ = if null errs then Exn.interrupt () else ();
126 val _ = Toplevel.status tr Markup.failed;
127 in ({failed = true}, (st, {malformed = malformed'})) end
130 val _ = proof_status tr st';
131 in ({failed = false}, (st', {malformed = malformed'})) end)
139 val no_print = Lazy.value ();
143 val is_init = Toplevel.is_init tr;
144 val is_proof = Keyword.is_proof (Toplevel.name_of tr);
147 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
150 (Lazy.lazy o Toplevel.setmp_thread_position tr)
151 (fn () => Toplevel.print_state false st')