equal
deleted
inserted
replaced
203 |
203 |
204 (* outer syntax *) |
204 (* outer syntax *) |
205 |
205 |
206 local structure P = OuterParse and K = OuterSyntax.Keyword in |
206 local structure P = OuterParse and K = OuterSyntax.Keyword in |
207 |
207 |
208 val silent_undoP = (* FIXME same name for compatibility with PG/Isabelle99 *) |
208 val old_undoP = (* FIXME same name for compatibility with PG/Isabelle99 *) |
209 OuterSyntax.improper_command "undo" "undo last command (no output)" K.control |
209 OuterSyntax.improper_command "undo" "undo last command (no output)" K.control |
|
210 (Scan.succeed IsarCmd.undo); |
|
211 |
|
212 val undoP = |
|
213 OuterSyntax.improper_command "ProofGeneral.undo" "undo last command (no output)" K.control |
210 (Scan.succeed IsarCmd.undo); |
214 (Scan.succeed IsarCmd.undo); |
211 |
215 |
212 val context_thy_onlyP = |
216 val context_thy_onlyP = |
213 OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control |
217 OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control |
214 (P.name >> IsarThy.init_context update_thy_only); |
218 (P.name >> IsarThy.init_context update_thy_only); |
232 val inform_file_retractedP = |
236 val inform_file_retractedP = |
233 OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control |
237 OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control |
234 (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name))); |
238 (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name))); |
235 |
239 |
236 fun init_outer_syntax () = OuterSyntax.add_parsers |
240 fun init_outer_syntax () = OuterSyntax.add_parsers |
237 [silent_undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP, |
241 [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP, |
238 inform_file_processedP, inform_file_retractedP]; |
242 inform_file_processedP, inform_file_retractedP]; |
239 |
243 |
240 end; |
244 end; |
241 |
245 |
242 |
246 |