changeset 27835 | ff8b8513965a |
parent 27775 | a9d16f8b997a |
child 32740 | 9dd0a2f83429 |
27834:04562d200f02 | 27835:ff8b8513965a |
---|---|
154 let |
154 let |
155 val is = TextIO.openIn(s ^ ".imp") |
155 val is = TextIO.openIn(s ^ ".imp") |
156 val inp = TextIO.inputAll is |
156 val inp = TextIO.inputAll is |
157 val _ = TextIO.closeIn is |
157 val _ = TextIO.closeIn is |
158 val orig_source = Source.of_string inp |
158 val orig_source = Source.of_string inp |
159 val symb_source = Symbol.source false orig_source |
159 val symb_source = Symbol.source {do_recover = false} orig_source |
160 val lexes = ref (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]), |
160 val lexes = ref (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]), |
161 Scan.empty_lexicon) |
161 Scan.empty_lexicon) |
162 val get_lexes = fn () => !lexes |
162 val get_lexes = fn () => !lexes |
163 val token_source = OuterLex.source NONE get_lexes Position.start symb_source |
163 val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source |
164 val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source) |
164 val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source) |
165 val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment |
165 val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment |
166 val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps |
166 val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps |
167 val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps |
167 val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps |
168 val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps |
168 val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps |