equal
deleted
inserted
replaced
2 Author: Sebastian Skalberg (TU Muenchen) |
2 Author: Sebastian Skalberg (TU Muenchen) |
3 *) |
3 *) |
4 |
4 |
5 signature IMPORTER_IMPORT_SYNTAX = |
5 signature IMPORTER_IMPORT_SYNTAX = |
6 sig |
6 sig |
7 val import_segment: (theory -> theory) parser |
|
8 val import_theory : (theory -> theory) parser |
|
9 val end_import : (theory -> theory) parser |
|
10 |
|
11 val setup_theory : (theory -> theory) parser |
|
12 val end_setup : (theory -> theory) parser |
|
13 |
|
14 val thm_maps : (theory -> theory) parser |
|
15 val ignore_thms : (theory -> theory) parser |
|
16 val type_maps : (theory -> theory) parser |
|
17 val def_maps : (theory -> theory) parser |
|
18 val const_maps : (theory -> theory) parser |
|
19 val const_moves : (theory -> theory) parser |
|
20 val const_renames : (theory -> theory) parser |
|
21 |
|
22 val setup : unit -> unit |
|
23 end |
7 end |
24 |
8 |
25 structure Importer_Import_Syntax : IMPORTER_IMPORT_SYNTAX = |
9 structure Importer_Import_Syntax : IMPORTER_IMPORT_SYNTAX = |
26 struct |
10 struct |
27 |
11 |
194 |
178 |
195 val set_dump = Parse.string -- Parse.string >> setup_dump |
179 val set_dump = Parse.string -- Parse.string >> setup_dump |
196 fun fl_dump toks = Scan.succeed flush_dump toks |
180 fun fl_dump toks = Scan.succeed flush_dump toks |
197 val append_dump = (Parse.verbatim || Parse.string) >> add_dump |
181 val append_dump = (Parse.verbatim || Parse.string) >> add_dump |
198 |
182 |
199 fun setup () = |
183 val _ = |
200 (Keyword.keyword ">"; |
184 (Keyword.keyword ">"; |
201 Outer_Syntax.command "import_segment" |
185 Outer_Syntax.command "import_segment" |
202 "Set import segment name" |
186 "Set import segment name" |
203 Keyword.thy_decl (import_segment >> Toplevel.theory); |
187 Keyword.thy_decl (import_segment >> Toplevel.theory); |
204 Outer_Syntax.command "import_theory" |
188 Outer_Syntax.command "import_theory" |