src/Pure/Isar/outer_syntax.ML
changeset 17283 881f5873bac0
parent 17265 12d99bb4304b
child 17412 e26cb20ef0cc
equal deleted inserted replaced
17282:43c86fedec82 17283:881f5873bac0
   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