Present.theory_source;
authorwenzelm
Tue Mar 09 12:20:22 1999 +0100 (1999-03-09)
changeset 63327cee353c7f2a
parent 6331 fb7b8d6c2bd1
child 6333 b1dec44d0018
Present.theory_source;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Mar 09 12:20:04 1999 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Mar 09 12:20:22 1999 +0100
     1.3 @@ -242,6 +242,7 @@
     1.4  
     1.5  fun run_thy name path =
     1.6    let val (src, pos) = Source.of_file path in
     1.7 +    Present.theory_source name src;
     1.8      if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src)
     1.9      else (Toplevel.excursion (parse_thy (src, pos))
    1.10        handle exn => error (Toplevel.exn_message exn))