236 val set_dump = Parse.string -- Parse.string >> setup_dump |
236 val set_dump = Parse.string -- Parse.string >> setup_dump |
237 fun fl_dump toks = Scan.succeed flush_dump toks |
237 fun fl_dump toks = Scan.succeed flush_dump toks |
238 val append_dump = (Parse.verbatim || Parse.string) >> add_dump |
238 val append_dump = (Parse.verbatim || Parse.string) >> add_dump |
239 |
239 |
240 val _ = |
240 val _ = |
241 (Outer_Syntax.command "import_segment" |
241 (Outer_Syntax.command @{command_spec "import_segment"} "set import segment name" |
242 "Set import segment name" |
242 (import_segment >> Toplevel.theory); |
243 Keyword.thy_decl (import_segment >> Toplevel.theory); |
243 Outer_Syntax.command @{command_spec "import_theory"} "set default external theory name" |
244 Outer_Syntax.command "import_theory" |
244 (import_theory >> Toplevel.theory); |
245 "Set default external theory name" |
245 Outer_Syntax.command @{command_spec "end_import"} "end external import" |
246 Keyword.thy_decl (import_theory >> Toplevel.theory); |
246 (end_import >> Toplevel.theory); |
247 Outer_Syntax.command "end_import" |
247 Outer_Syntax.command @{command_spec "setup_theory"} "setup external theory replaying" |
248 "End external import" |
248 (setup_theory >> Toplevel.theory); |
249 Keyword.thy_decl (end_import >> Toplevel.theory); |
249 Outer_Syntax.command @{command_spec "end_setup"} "end external setup" |
250 Outer_Syntax.command "setup_theory" |
250 (end_setup >> Toplevel.theory); |
251 "Setup external theory replaying" |
251 Outer_Syntax.command @{command_spec "setup_dump"} "setup the dump file name" |
252 Keyword.thy_decl (setup_theory >> Toplevel.theory); |
252 (set_dump >> Toplevel.theory); |
253 Outer_Syntax.command "end_setup" |
253 Outer_Syntax.command @{command_spec "append_dump"} "add text to dump file" |
254 "End external setup" |
254 (append_dump >> Toplevel.theory); |
255 Keyword.thy_decl (end_setup >> Toplevel.theory); |
255 Outer_Syntax.command @{command_spec "flush_dump"} "write the dump to file" |
256 Outer_Syntax.command "setup_dump" |
256 (fl_dump >> Toplevel.theory); |
257 "Setup the dump file name" |
257 Outer_Syntax.command @{command_spec "ignore_thms"} |
258 Keyword.thy_decl (set_dump >> Toplevel.theory); |
258 "theorems to ignore in next external theory import" |
259 Outer_Syntax.command "append_dump" |
259 (ignore_thms >> Toplevel.theory); |
260 "Add text to dump file" |
260 Outer_Syntax.command @{command_spec "type_maps"} |
261 Keyword.thy_decl (append_dump >> Toplevel.theory); |
261 "map external type names to existing Isabelle/HOL type names" |
262 Outer_Syntax.command "flush_dump" |
262 (type_maps >> Toplevel.theory); |
263 "Write the dump to file" |
263 Outer_Syntax.command @{command_spec "def_maps"} |
264 Keyword.thy_decl (fl_dump >> Toplevel.theory); |
264 "map external constant names to their primitive definitions" |
265 Outer_Syntax.command "ignore_thms" |
265 (def_maps >> Toplevel.theory); |
266 "Theorems to ignore in next external theory import" |
266 Outer_Syntax.command @{command_spec "thm_maps"} |
267 Keyword.thy_decl (ignore_thms >> Toplevel.theory); |
267 "map external theorem names to existing Isabelle/HOL theorem names" |
268 Outer_Syntax.command "type_maps" |
268 (thm_maps >> Toplevel.theory); |
269 "Map external type names to existing Isabelle/HOL type names" |
269 Outer_Syntax.command @{command_spec "const_renames"} |
270 Keyword.thy_decl (type_maps >> Toplevel.theory); |
270 "rename external const names" |
271 Outer_Syntax.command "def_maps" |
271 (const_renames >> Toplevel.theory); |
272 "Map external constant names to their primitive definitions" |
272 Outer_Syntax.command @{command_spec "const_moves"} |
273 Keyword.thy_decl (def_maps >> Toplevel.theory); |
273 "rename external const names to other external constants" |
274 Outer_Syntax.command "thm_maps" |
274 (const_moves >> Toplevel.theory); |
275 "Map external theorem names to existing Isabelle/HOL theorem names" |
275 Outer_Syntax.command @{command_spec "const_maps"} |
276 Keyword.thy_decl (thm_maps >> Toplevel.theory); |
276 "map external const names to existing Isabelle/HOL const names" |
277 Outer_Syntax.command "const_renames" |
277 (const_maps >> Toplevel.theory)); |
278 "Rename external const names" |
|
279 Keyword.thy_decl (const_renames >> Toplevel.theory); |
|
280 Outer_Syntax.command "const_moves" |
|
281 "Rename external const names to other external constants" |
|
282 Keyword.thy_decl (const_moves >> Toplevel.theory); |
|
283 Outer_Syntax.command "const_maps" |
|
284 "Map external const names to existing Isabelle/HOL const names" |
|
285 Keyword.thy_decl (const_maps >> Toplevel.theory)); |
|
286 |
278 |
287 end |
279 end |
288 |
280 |