removed begin;
authorwenzelm
Thu Oct 16 14:48:10 1997 +0200 (1997-10-16)
changeset 3900e30bd27a4910
parent 3899 41a4abfa60fe
child 3901 8b09bc500f65
removed begin;
added global section;
added global_names flag (tmp), default true;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Thu Oct 16 14:46:55 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Thu Oct 16 14:48:10 1997 +0200
     1.3 @@ -5,6 +5,10 @@
     1.4  The parser for theory files.
     1.5  *)
     1.6  
     1.7 +(* FIXME tmp *)
     1.8 +val global_names = ref true;
     1.9 +
    1.10 +
    1.11  infix 5 -- --$$ $$-- ^^;
    1.12  infix 3 >>;
    1.13  infix 0 ||;
    1.14 @@ -409,6 +413,11 @@
    1.15    >> (fn ((x, y), z) => (cat_lines [x, y, z]));
    1.16  
    1.17  
    1.18 +(* global *)
    1.19 +
    1.20 +val global_decl = empty >> K "\"/\"";
    1.21 +
    1.22 +
    1.23  
    1.24  (** theory syntax **)
    1.25  
    1.26 @@ -435,12 +444,12 @@
    1.27  
    1.28  (* extension *)
    1.29  
    1.30 -fun mk_extension ((begin, txts), mltxt) =
    1.31 +fun mk_extension (txts, mltxt) =
    1.32    let
    1.33      val cat_sects = space_implode "\n\n" o filter_out (equal "");
    1.34      val (extxts, postxts) = split_list txts;
    1.35    in
    1.36 -    (begin, cat_sects extxts, cat_sects postxts, mltxt)
    1.37 +    (cat_sects extxts, cat_sects postxts, mltxt)
    1.38    end;
    1.39  
    1.40  fun sect tab ((Keyword, s, n) :: toks) =
    1.41 @@ -450,19 +459,16 @@
    1.42    | sect _ ((_, s, n) :: _) = syn_err "section" s n
    1.43    | sect _ [] = eof_err ();
    1.44  
    1.45 -val opt_begin =
    1.46 -  optional ("begin" $$-- optional name "" >> Some) None;
    1.47 +fun extension sectab = "+" $$-- !!
    1.48 +  (repeat (sect sectab) --$$ "end" -- optional ("ML" $$-- verbatim) "")
    1.49 +    >> mk_extension;
    1.50  
    1.51 -fun extension sectab = "+" $$-- !!
    1.52 -  (opt_begin -- (repeat (sect sectab) --$$ "end") --
    1.53 -    optional ("ML" $$-- verbatim) "") >> mk_extension;
    1.54 -
    1.55 -fun opt_extension sectab = optional (extension sectab) (None, "", "", "");
    1.56 +fun opt_extension sectab = optional (extension sectab) ("", "", "");
    1.57  
    1.58  
    1.59  (* theory definition *)
    1.60  
    1.61 -fun mk_structure tname ((thy_name, old_thys), (begin, extxt, postxt, mltxt)) =
    1.62 +fun mk_structure tname ((thy_name, old_thys), (extxt, postxt, mltxt)) =
    1.63    if thy_name <> tname then
    1.64      error ("Filename \"" ^ tname ^ ".thy\" and theory name "
    1.65        ^ quote thy_name ^ " are different")
    1.66 @@ -478,12 +484,8 @@
    1.67      ^ mltxt ^ "\n\
    1.68      \\n\
    1.69      \val thy = thy\n\
    1.70 -    \\n\
    1.71 -    \|> Theory.add_path \"/\"\n" ^
    1.72 -    (case begin of
    1.73 -      None => (warning ("Flat name space for theory " ^ tname ^ "?  Consider begin ..."); "")
    1.74 -    | Some "" => "|> Theory.add_path " ^ quote tname ^ "\n"
    1.75 -    | Some path => "|> Theory.add_path " ^ path ^ "\n") ^
    1.76 +    \\n" ^
    1.77 +    (if ! global_names then "" else "|> Theory.add_path " ^ quote tname ^ "\n") ^
    1.78      "\n\
    1.79      \|> Theory.add_trfuns\n"
    1.80      ^ trfun_args ^ "\n\
    1.81 @@ -528,8 +530,9 @@
    1.82  
    1.83  
    1.84  val pure_keywords =
    1.85 - ["end", "ML", "mixfix", "infixr", "infixl", "begin", "binder", "output", "=",
    1.86 -  "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
    1.87 + ["end", "ML", "mixfix", "infixr", "infixl", "binder", "global",
    1.88 +  "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]", "::",
    1.89 +  "==", "=>", "<="];
    1.90  
    1.91  val pure_sections =
    1.92   [section "classes" "|> Theory.add_classes" class_decls,
    1.93 @@ -545,7 +548,8 @@
    1.94    axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
    1.95    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.96    section "instance" "" instance_decl,
    1.97 -  section "path" "|> Theory.add_path" name];
    1.98 +  section "path" "|> Theory.add_path" name,
    1.99 +  section "global" "|> Theory.add_path" global_decl];
   1.100  
   1.101  
   1.102  end;