equal
deleted
inserted
replaced
276 fun present_text () = Source.exhaust (Symbol.source false text_src); |
276 fun present_text () = Source.exhaust (Symbol.source false text_src); |
277 in |
277 in |
278 Present.init_theory name; |
278 Present.init_theory name; |
279 Present.verbatim_source name present_text; |
279 Present.verbatim_source name present_text; |
280 if ThyHeader.is_old (text_src, pos) then |
280 if ThyHeader.is_old (text_src, pos) then |
281 (warning ("Non-Isar file format for theory " ^ quote name ^ " (deprecated)"); |
281 (warning ("Non-Isar file format for theory " ^ quote name ^ " -- deprecated"); |
282 ThySyn.load_thy name text; |
282 ThySyn.load_thy name text; |
283 Present.old_symbol_source name present_text) (*note: text presented twice*) |
283 Present.old_symbol_source name present_text) (*note: text presented twice*) |
284 else |
284 else |
285 let |
285 let |
286 val tok_src = text_src |
286 val tok_src = text_src |