177 (Thy_Output.check_text (Token.source_position_of cmt) st'; []) |
177 (Thy_Output.check_text (Token.source_position_of cmt) st'; []) |
178 handle exn => |
178 handle exn => |
179 if Exn.is_interrupt exn then reraise exn |
179 if Exn.is_interrupt exn then reraise exn |
180 else ML_Compiler.exn_messages_ids exn)) (); |
180 else ML_Compiler.exn_messages_ids exn)) (); |
181 |
181 |
|
182 fun report tr m = |
|
183 Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) (); |
|
184 |
|
185 fun status tr m = |
|
186 Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); |
|
187 |
182 fun proof_status tr st = |
188 fun proof_status tr st = |
183 (case try Toplevel.proof_of st of |
189 (case try Toplevel.proof_of st of |
184 SOME prf => Toplevel.status tr (Proof.status_markup prf) |
190 SOME prf => status tr (Proof.status_markup prf) |
185 | NONE => ()); |
191 | NONE => ()); |
186 |
192 |
187 fun eval_state span tr ({malformed, state = st, ...}: eval_state) = |
193 fun eval_state span tr ({malformed, state = st, ...}: eval_state) = |
188 if malformed then |
194 if malformed then |
189 {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel} |
195 {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel} |
192 val malformed' = Toplevel.is_malformed tr; |
198 val malformed' = Toplevel.is_malformed tr; |
193 val is_init = Toplevel.is_init tr; |
199 val is_init = Toplevel.is_init tr; |
194 val is_proof = Keyword.is_proof (Toplevel.name_of tr); |
200 val is_proof = Keyword.is_proof (Toplevel.name_of tr); |
195 |
201 |
196 val _ = Multithreading.interrupted (); |
202 val _ = Multithreading.interrupted (); |
197 val _ = Toplevel.status tr Markup.running; |
203 val _ = status tr Markup.running; |
198 val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; |
204 val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; |
199 val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); |
205 val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); |
200 val errs = errs1 @ errs2; |
206 val errs = errs1 @ errs2; |
201 val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs; |
207 val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs; |
202 in |
208 in |
203 (case result of |
209 (case result of |
204 NONE => |
210 NONE => |
205 let |
211 let |
206 val _ = Toplevel.status tr Markup.failed; |
212 val _ = status tr Markup.failed; |
207 val _ = Toplevel.status tr Markup.finished; |
213 val _ = status tr Markup.finished; |
208 val _ = if null errs then Exn.interrupt () else (); |
214 val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else (); |
209 in {failed = true, malformed = malformed', command = tr, state = st} end |
215 in {failed = true, malformed = malformed', command = tr, state = st} end |
210 | SOME st' => |
216 | SOME st' => |
211 let |
217 let |
212 val _ = proof_status tr st'; |
218 val _ = proof_status tr st'; |
213 val _ = Toplevel.status tr Markup.finished; |
219 val _ = status tr Markup.finished; |
214 in {failed = false, malformed = malformed', command = tr, state = st'} end) |
220 in {failed = false, malformed = malformed', command = tr, state = st'} end) |
215 end; |
221 end; |
216 |
222 |
217 in |
223 in |
218 |
224 |