35 fn thy => |
35 fn thy => |
36 thy |> set_generating_thy thyname |
36 thy |> set_generating_thy thyname |
37 |> Theory.add_path thyname |
37 |> Theory.add_path thyname |
38 |> add_dump (";setup_theory " ^ thyname)) |
38 |> add_dump (";setup_theory " ^ thyname)) |
39 |
39 |
40 val end_import = Scan.succeed |
40 fun end_import toks = |
41 (fn thy => |
41 Scan.succeed |
42 let |
42 (fn thy => |
43 val thyname = get_generating_thy thy |
43 let |
44 val segname = get_import_segment thy |
44 val thyname = get_generating_thy thy |
45 val (int_thms,facts) = Replay.setup_int_thms thyname thy |
45 val segname = get_import_segment thy |
46 val thmnames = filter (not o should_ignore thyname thy) facts |
46 val (int_thms,facts) = Replay.setup_int_thms thyname thy |
47 in |
47 val thmnames = filter (not o should_ignore thyname thy) facts |
48 thy |> clear_import_thy |
48 in |
49 |> set_segment thyname segname |
49 thy |> clear_import_thy |
50 |> set_used_names facts |
50 |> set_segment thyname segname |
51 |> Replay.import_thms thyname int_thms thmnames |
51 |> set_used_names facts |
52 |> clear_used_names |
52 |> Replay.import_thms thyname int_thms thmnames |
53 |> export_hol4_pending |
53 |> clear_used_names |
54 |> Theory.parent_path |
54 |> export_hol4_pending |
55 |> dump_import_thy thyname |
55 |> Theory.parent_path |
56 |> add_dump ";end_setup" |
56 |> dump_import_thy thyname |
57 end) |
57 |> add_dump ";end_setup" |
|
58 end) toks |
58 |
59 |
59 val ignore_thms = Scan.repeat1 P.name |
60 val ignore_thms = Scan.repeat1 P.name |
60 >> (fn ignored => |
61 >> (fn ignored => |
61 fn thy => |
62 fn thy => |
62 let |
63 let |
156 case HOL4DefThy.get thy of |
157 case HOL4DefThy.get thy of |
157 NoImport => thy |> import_thy thyname |
158 NoImport => thy |> import_thy thyname |
158 | Generating _ => error "Currently generating a theory!" |
159 | Generating _ => error "Currently generating a theory!" |
159 | Replaying _ => thy |> clear_import_thy |> import_thy thyname) |
160 | Replaying _ => thy |> clear_import_thy |> import_thy thyname) |
160 |
161 |
161 val end_setup = Scan.succeed (fn thy => |
162 fun end_setup toks = |
162 let |
163 Scan.succeed |
163 val thyname = get_import_thy thy |
164 (fn thy => |
164 val segname = get_import_segment thy |
165 let |
165 in |
166 val thyname = get_import_thy thy |
166 thy |> set_segment thyname segname |
167 val segname = get_import_segment thy |
167 |> clear_import_thy |
168 in |
168 |> Theory.parent_path |
169 thy |> set_segment thyname segname |
169 end) |
170 |> clear_import_thy |
|
171 |> Theory.parent_path |
|
172 end) toks |
170 |
173 |
171 val set_dump = P.string -- P.string >> setup_dump |
174 val set_dump = P.string -- P.string >> setup_dump |
172 val fl_dump = Scan.succeed flush_dump |
175 fun fl_dump toks = Scan.succeed flush_dump toks |
173 val append_dump = (P.verbatim || P.string) >> add_dump |
176 val append_dump = (P.verbatim || P.string) >> add_dump |
174 |
177 |
175 val parsers = |
178 val parsers = |
176 [OuterSyntax.command "import_segment" |
179 [OuterSyntax.command "import_segment" |
177 "Set import segment name" |
180 "Set import segment name" |