src/Pure/Thy/thy_parse.ML

     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 The parser for theory files.
 *)
+
+(* FIXME tmp *)
+val global_names = ref true;
+
 
 infix 5 -- --$$ $$-- ^^;
 infix 3 >>;
 infix 0 ||;
 

     name --$$ "::" -- arity >> (pair "|> AxClass.add_inst_arity" o mk_triple2))
   -- opt_witness
   >> (fn ((x, y), z) => (cat_lines [x, y, z]));
 
 
+(* global *)
+
+val global_decl = empty >> K "\"/\"";
+
+
 
 (** theory syntax **)
 
 type syntax =
   lexicon * (token list -> (string * string) * token list) Symtab.table;

 val header = ident --$$ "=" -- enum1 "+" base >> mk_header;
 
 
 (* 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) =
       (case Symtab.lookup (tab, s) of
         Some parse => !! parse toks
       | None => syn_err "section" s n)
   | sect _ ((_, s, n) :: _) = syn_err "section" s n
   | sect _ [] = eof_err ();
 
-val opt_begin =
-  optional ("begin" $$-- optional name "" >> Some) None;
-
 fun extension sectab = "+" $$-- !!
-  (opt_begin -- (repeat (sect sectab) --$$ "end") --
-    optional ("ML" $$-- verbatim) "") >> mk_extension;
-
-fun opt_extension sectab = optional (extension sectab) (None, "", "", "");
+  (repeat (sect sectab) --$$ "end" -- optional ("ML" $$-- verbatim) "")
+    >> mk_extension;
+
+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")
   else
     "val thy = " ^ old_thys ^ ";\n\n\

     \in\n\
     \\n"
     ^ 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\
     \|> Theory.add_trfunsT typed_print_translation \n\
     \|> Theory.add_tokentrfuns token_translation \n\

 fun section name pretxt parse =
   axm_section name pretxt (parse >> rpair []);
 
 
 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,
   section "default" "|> Theory.add_defsort" sort,
   section "types" "" type_decls,

   axm_section "defs" "|> Theory.add_defs" axiom_decls,
   section "oracle" "|> Theory.add_oracle" oracle_decl,
   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;