# HG changeset patch
# User wenzelm
# Date 876159580 -7200
# Node ID 05e47c7cc6fd82b77d9973fa690642be41c49ada
# Parent  60c788035e54d4e583e3208e169250adba60cf74
optional begin keyword;

diff -r 60c788035e54 -r 05e47c7cc6fd src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Oct 06 19:16:57 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 06 19:39:40 1997 +0200
@@ -451,7 +451,7 @@
 
 (* theory definition *)
 
-fun mk_structure tname ((thy_name, old_thys), opt_txts) =
+fun mk_structure tname (((thy_name, old_thys), has_begin), opt_txts) =
   if thy_name <> tname then
     error ("Filename \"" ^ tname ^ ".thy\" and theory name "
       ^ quote thy_name ^ " are different")
@@ -469,7 +469,9 @@
         ^ mltxt ^ "\n\
         \\n\
         \val thy = thy\n\
-        \\n\
+        \\n" ^
+        (if has_begin then "Theory.add_path " ^ quote tname else "") ^
+        "\n\
         \|> Theory.add_trfuns\n"
         ^ trfun_args ^ "\n\
         \|> Theory.add_trfunsT typed_print_translation \n\
@@ -507,7 +509,8 @@
 
 
 fun theory_defn sectab tname =
-  header -- optional (extension sectab >> Some) None -- eof
+  header -- optional ($$ "begin" >> K true) false --
+    optional (extension sectab >> Some) None -- eof
   >> (mk_structure tname o #1);
 
 fun parse_thy (lex, sectab) tname str =
@@ -530,7 +533,7 @@
 
 
 val pure_keywords =
- ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
+ ["end", "ML", "mixfix", "infixr", "infixl", "begin", "binder", "output", "=",
   "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
 
 val pure_sections =