206 |
206 |
207 local structure P = OuterParse and K = OuterSyntax.Keyword in |
207 local structure P = OuterParse and K = OuterSyntax.Keyword in |
208 |
208 |
209 val old_undoP = (* FIXME same name for compatibility with PG/Isabelle99 *) |
209 val old_undoP = (* FIXME same name for compatibility with PG/Isabelle99 *) |
210 OuterSyntax.improper_command "undo" "undo last command (no output)" K.control |
210 OuterSyntax.improper_command "undo" "undo last command (no output)" K.control |
211 (Scan.succeed IsarCmd.undo); |
211 (Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); |
212 |
212 |
213 val undoP = |
213 val undoP = |
214 OuterSyntax.improper_command "ProofGeneral.undo" "undo last command (no output)" K.control |
214 OuterSyntax.improper_command "ProofGeneral.undo" "undo last command (no output)" K.control |
215 (Scan.succeed IsarCmd.undo); |
215 (Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); |
216 |
216 |
217 val context_thy_onlyP = |
217 val context_thy_onlyP = |
218 OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control |
218 OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control |
219 (P.name >> IsarThy.init_context update_thy_only); |
219 (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only)); |
220 |
220 |
221 val try_context_thy_onlyP = |
221 val try_context_thy_onlyP = |
222 OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control |
222 OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control |
223 (P.name >> (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)); |
223 (P.name >> (Toplevel.no_timing oo |
|
224 (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only))); |
224 |
225 |
225 val restartP = |
226 val restartP = |
226 OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control |
227 OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control |
227 (P.opt_unit >> K (Toplevel.imperative isar_restart)); |
228 (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart))); |
228 |
229 |
229 val kill_proofP = |
230 val kill_proofP = |
230 OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control |
231 OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control |
231 (Scan.succeed (IsarCmd.kill_proof_notify tell_clear_goals)); |
232 (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals)); |
232 |
233 |
233 val inform_file_processedP = |
234 val inform_file_processedP = |
234 OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control |
235 OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control |
235 (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_processed name))); |
236 (P.name >> (Toplevel.no_timing oo |
|
237 (fn name => Toplevel.imperative (fn () => inform_file_processed name)))); |
236 |
238 |
237 val inform_file_retractedP = |
239 val inform_file_retractedP = |
238 OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control |
240 OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control |
239 (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name))); |
241 (P.name >> (Toplevel.no_timing oo |
|
242 (fn name => Toplevel.imperative (fn () => inform_file_retracted name)))); |
240 |
243 |
241 fun init_outer_syntax () = OuterSyntax.add_parsers |
244 fun init_outer_syntax () = OuterSyntax.add_parsers |
242 [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP, |
245 [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP, |
243 inform_file_processedP, inform_file_retractedP]; |
246 inform_file_processedP, inform_file_retractedP]; |
244 |
247 |