src/Pure/Isar/outer_syntax.ML
changeset 17250 158ef530c153
parent 17237 75407a6f02d2
child 17265 12d99bb4304b
equal deleted inserted replaced
17249:e89fbfd778c1 17250:158ef530c153
   277     fun present_text () = Source.exhaust (Symbol.source false text_src);
   277     fun present_text () = Source.exhaust (Symbol.source false text_src);
   278   in
   278   in
   279     Present.init_theory name;
   279     Present.init_theory name;
   280     Present.verbatim_source name present_text;
   280     Present.verbatim_source name present_text;
   281     if ThyHeader.is_old (text_src, pos) then
   281     if ThyHeader.is_old (text_src, pos) then
   282      (warning ("Non-Isar file format for theory " ^ quote name ^ " -- deprecated!");
   282      (warning ("Non-Isar file format for theory " ^ quote name ^ " (deprecated)");
   283       ThySyn.load_thy name text;
   283       ThySyn.load_thy name text;
   284       Present.old_symbol_source name present_text)   (*note: text presented twice*)
   284       Present.old_symbol_source name present_text)   (*note: text presented twice*)
   285     else
   285     else
   286       let
   286       let
   287         val tok_src = text_src
   287         val tok_src = text_src