present source *before* theory load;
authorwenzelm
Thu, 07 Oct 1999 12:19:47 +0200
changeset 7768 b106e4af1301
parent 7767 659648e14c3e
child 7769 700439dc581e
present source *before* theory load;
src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 12:19:21 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 12:19:47 1999 +0200
@@ -385,11 +385,10 @@
     val pos = Path.position path;
   in
     Present.init_theory name;
+    Present.verbatim_source name (present_text text);
     if is_old_theory (src, pos) then ThySyn.load_thy name text
-    else
-     (Toplevel.excursion_error (parse_thy (src, pos));
-      Present.token_source name (present_toks text pos));
-    Present.verbatim_source name (present_text text)
+    else (Present.token_source name (present_toks text pos);
+      Toplevel.excursion_error (parse_thy (src, pos)))
   end;
 
 in