# HG changeset patch
# User wenzelm
# Date 877006090 -7200
# Node ID e30bd27a49103006979be333794ea1ba9cc4fd2c
# Parent  41a4abfa60fe5a06f1a4e567757ac56247328c6f
removed begin;
added global section;
added global_names flag (tmp), default true;

diff -r 41a4abfa60fe -r e30bd27a4910 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Thu Oct 16 14:46:55 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Thu Oct 16 14:48:10 1997 +0200
@@ -5,6 +5,10 @@
 The parser for theory files.
 *)
 
+(* FIXME tmp *)
+val global_names = ref true;
+
+
 infix 5 -- --$$ $$-- ^^;
 infix 3 >>;
 infix 0 ||;
@@ -409,6 +413,11 @@
   >> (fn ((x, y), z) => (cat_lines [x, y, z]));
 
 
+(* global *)
+
+val global_decl = empty >> K "\"/\"";
+
+
 
 (** theory syntax **)
 
@@ -435,12 +444,12 @@
 
 (* extension *)
 
-fun mk_extension ((begin, txts), mltxt) =
+fun mk_extension (txts, mltxt) =
   let
     val cat_sects = space_implode "\n\n" o filter_out (equal "");
     val (extxts, postxts) = split_list txts;
   in
-    (begin, cat_sects extxts, cat_sects postxts, mltxt)
+    (cat_sects extxts, cat_sects postxts, mltxt)
   end;
 
 fun sect tab ((Keyword, s, n) :: toks) =
@@ -450,19 +459,16 @@
   | sect _ ((_, s, n) :: _) = syn_err "section" s n
   | sect _ [] = eof_err ();
 
-val opt_begin =
-  optional ("begin" $$-- optional name "" >> Some) None;
+fun extension sectab = "+" $$-- !!
+  (repeat (sect sectab) --$$ "end" -- optional ("ML" $$-- verbatim) "")
+    >> mk_extension;
 
-fun extension sectab = "+" $$-- !!
-  (opt_begin -- (repeat (sect sectab) --$$ "end") --
-    optional ("ML" $$-- verbatim) "") >> mk_extension;
-
-fun opt_extension sectab = optional (extension sectab) (None, "", "", "");
+fun opt_extension sectab = optional (extension sectab) ("", "", "");
 
 
 (* theory definition *)
 
-fun mk_structure tname ((thy_name, old_thys), (begin, extxt, postxt, mltxt)) =
+fun mk_structure tname ((thy_name, old_thys), (extxt, postxt, mltxt)) =
   if thy_name <> tname then
     error ("Filename \"" ^ tname ^ ".thy\" and theory name "
       ^ quote thy_name ^ " are different")
@@ -478,12 +484,8 @@
     ^ mltxt ^ "\n\
     \\n\
     \val thy = thy\n\
-    \\n\
-    \|> Theory.add_path \"/\"\n" ^
-    (case begin of
-      None => (warning ("Flat name space for theory " ^ tname ^ "?  Consider begin ..."); "")
-    | Some "" => "|> Theory.add_path " ^ quote tname ^ "\n"
-    | Some path => "|> Theory.add_path " ^ path ^ "\n") ^
+    \\n" ^
+    (if ! global_names then "" else "|> Theory.add_path " ^ quote tname ^ "\n") ^
     "\n\
     \|> Theory.add_trfuns\n"
     ^ trfun_args ^ "\n\
@@ -528,8 +530,9 @@
 
 
 val pure_keywords =
- ["end", "ML", "mixfix", "infixr", "infixl", "begin", "binder", "output", "=",
-  "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
+ ["end", "ML", "mixfix", "infixr", "infixl", "binder", "global",
+  "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
+  "==", "=>", "<="];
 
 val pure_sections =
  [section "classes" "|> Theory.add_classes" class_decls,
@@ -545,7 +548,8 @@
   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   section "instance" "" instance_decl,
-  section "path" "|> Theory.add_path" name];
+  section "path" "|> Theory.add_path" name,
+  section "global" "|> Theory.add_path" global_decl];
 
 
 end;