# HG changeset patch
# User wenzelm
# Date 939291587 -7200
# Node ID b106e4af13014dbf19c33cb3ea38109ca9371de8
# Parent  659648e14c3ef050c38377c28436a717953f8319
present source *before* theory load;

diff -r 659648e14c3e -r b106e4af1301 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