Present.token_source after load (better errors!?);
authorwenzelm
Thu Oct 07 12:36:39 1999 +0200 (1999-10-07)
changeset 77746da9b544a12d
parent 7773 ce86227f29d0
child 7775 26898fbd19ca
Present.token_source after load (better errors!?);
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 12:33:54 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 12:36:39 1999 +0200
     1.3 @@ -387,8 +387,8 @@
     1.4      Present.init_theory name;
     1.5      Present.verbatim_source name (present_text text);
     1.6      if is_old_theory (src, pos) then ThySyn.load_thy name text
     1.7 -    else (Present.token_source name (present_toks text pos);
     1.8 -      Toplevel.excursion_error (parse_thy (src, pos)))
     1.9 +    else (Toplevel.excursion_error (parse_thy (src, pos));
    1.10 +      Present.token_source name (present_toks text pos))
    1.11    end;
    1.12  
    1.13  in