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 read: span -> Toplevel.transition
18 val eval: span -> Toplevel.transition ->
19 Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
20 type print = {name: string, pri: int, pr: unit lazy}
21 val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
23 {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
25 val print_function: string -> int -> print_function -> unit
28 structure Command: COMMAND =
33 type span = Token.T list;
35 val range = Token.position_range_of;
36 val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
43 Result of 'a Exn.result;
45 abstype 'a memo = Memo of 'a expr Synchronized.var
48 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
49 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
51 fun memo_eval (Memo v) =
52 (case Synchronized.value v of
55 Synchronized.guarded_access v
56 (fn Result res => SOME (res, Result res)
58 let val res = Exn.capture e (); (*memoing of physical interrupts!*)
59 in SOME (res, Result res) end))
62 fun memo_result (Memo v) =
63 (case Synchronized.value v of
64 Result res => Exn.release res
65 | _ => raise Fail "Unfinished memo result");
74 val outer_syntax = #2 (Outer_Syntax.get_syntax ());
75 val command_reports = Outer_Syntax.command_reports outer_syntax;
77 val proper_range = Position.set_range (proper_range span);
79 (case find_first Token.is_command span of
80 SOME tok => Token.position_of tok
81 | NONE => proper_range);
83 val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
84 val _ = Position.reports_text (token_reports @ maps command_reports span);
86 if is_malformed then Toplevel.malformed pos "Malformed command syntax"
88 (case Outer_Syntax.read_spans outer_syntax span of
90 if Keyword.is_control (Toplevel.name_of tr) then
91 Toplevel.malformed pos "Illegal control command"
93 | [] => Toplevel.ignored (Position.set_range (range span))
94 | _ => Toplevel.malformed proper_range "Exactly one command expected")
95 handle ERROR msg => Toplevel.malformed proper_range msg
104 if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
105 (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
106 (fn () => Toplevel.command_exception int tr st); ([], SOME st))
107 else Toplevel.command_errors int tr st;
109 fun check_cmts span tr st' =
110 Toplevel.setmp_thread_position tr
112 Outer_Syntax.side_comments span |> maps (fn cmt =>
113 (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
114 handle exn => ML_Compiler.exn_messages_ids exn)) ();
116 fun proof_status tr st =
117 (case try Toplevel.proof_of st of
118 SOME prf => Toplevel.status tr (Proof.status_markup prf)
123 fun eval span tr (st, {malformed}) =
125 ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
128 val malformed' = Toplevel.is_malformed tr;
129 val is_init = Toplevel.is_init tr;
130 val is_proof = Keyword.is_proof (Toplevel.name_of tr);
132 val _ = Multithreading.interrupted ();
133 val _ = Toplevel.status tr Markup.running;
134 val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
135 val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
136 val errs = errs1 @ errs2;
137 val _ = Toplevel.status tr Markup.finished;
138 val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
143 val _ = if null errs then Exn.interrupt () else ();
144 val _ = Toplevel.status tr Markup.failed;
145 in ({failed = true}, (st, {malformed = malformed'})) end
148 val _ = proof_status tr st';
149 in ({failed = false}, (st', {malformed = malformed'})) end)
157 type print_function =
158 {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
159 (unit -> unit) option;
161 type print = {name: string, pri: int, pr: unit lazy};
165 val print_functions =
166 Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
170 fun print st tr st' =
171 rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
172 (case f {old_state = st, tr = tr, state = st'} of
174 SOME {name = name, pri = pri, pr = (Lazy.lazy o Toplevel.setmp_thread_position tr) pr}
177 fun print_function name pri f =
178 Synchronized.change print_functions (fn funs =>
179 (if not (AList.defined (op =) funs name) then ()
180 else warning ("Redefining command print function: " ^ quote name);
181 AList.update (op =) (name, (pri, f)) funs));
185 val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
187 val is_init = Toplevel.is_init tr;
188 val is_proof = Keyword.is_proof (Toplevel.name_of tr);
191 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
192 in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);