eliminated aliasing merge: now always extends;
authorwenzelm
Wed Oct 15 15:14:56 1997 +0200 (1997-10-15)
changeset 3875f62a4edb1888
parent 3874 552ce5ad6a2e
child 3876 e6f918979f2d
eliminated aliasing merge: now always extends;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Oct 15 15:13:43 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Oct 15 15:14:56 1997 +0200
     1.3 @@ -457,73 +457,56 @@
     1.4    (opt_begin -- (repeat (sect sectab) --$$ "end") --
     1.5      optional ("ML" $$-- verbatim) "") >> mk_extension;
     1.6  
     1.7 +fun opt_extension sectab = optional (extension sectab) (None, "", "", "");
     1.8 +
     1.9  
    1.10  (* theory definition *)
    1.11  
    1.12 -fun mk_structure tname ((thy_name, old_thys), opt_ext) =
    1.13 +fun mk_structure tname ((thy_name, old_thys), (begin, extxt, postxt, mltxt)) =
    1.14    if thy_name <> tname then
    1.15      error ("Filename \"" ^ tname ^ ".thy\" and theory name "
    1.16        ^ quote thy_name ^ " are different")
    1.17    else
    1.18 -    (case opt_ext of
    1.19 -      Some (begin, extxt, postxt, mltxt) =>
    1.20 -        "val thy = " ^ old_thys ^ " true;\n\n\
    1.21 -        \structure " ^ thy_name ^ " =\n\
    1.22 -        \struct\n\
    1.23 -        \\n\
    1.24 -        \local\n"
    1.25 -        ^ trfun_defs ^ "\n\
    1.26 -        \in\n\
    1.27 -        \\n"
    1.28 -        ^ mltxt ^ "\n\
    1.29 -        \\n\
    1.30 -        \val thy = thy\n\
    1.31 -        \\n\
    1.32 -        \|> Theory.add_path \"/\"\n" ^
    1.33 -        (case begin of
    1.34 -          None => (warning ("Flat name space for theory " ^ tname ^ "?  \
    1.35 -            \Consider begin ..."); "")
    1.36 -        | Some "" => "|> Theory.add_path " ^ quote tname ^ "\n"
    1.37 -        | Some path => "|> Theory.add_path " ^ path ^ "\n") ^
    1.38 -        "\n\
    1.39 -        \|> Theory.add_trfuns\n"
    1.40 -        ^ trfun_args ^ "\n\
    1.41 -        \|> Theory.add_trfunsT typed_print_translation \n\
    1.42 -        \|> Theory.add_tokentrfuns token_translation \n\
    1.43 -        \\n"
    1.44 -        ^ extxt ^ "\n\
    1.45 -        \\n\
    1.46 -        \|> Theory.add_name " ^ quote thy_name ^ ";\n\
    1.47 -        \\n\
    1.48 -        \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.49 -        \\n\
    1.50 -        \\n"
    1.51 -        ^ postxt ^ "\n\
    1.52 -        \\n\
    1.53 -        \end;\n\
    1.54 -        \end;\n\
    1.55 -        \\n\
    1.56 -        \open " ^ thy_name ^ ";\n\
    1.57 -        \\n"
    1.58 -    | None =>
    1.59 -        "val thy = " ^ old_thys ^ " false;\n\
    1.60 -        \\n\
    1.61 -        \structure " ^ thy_name ^ " =\n\
    1.62 -        \struct\n\
    1.63 -        \\n\
    1.64 -        \val thy = thy\n\
    1.65 -        \\n\
    1.66 -        \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.67 -        \\n\
    1.68 -        \end;\n\
    1.69 -        \\n\
    1.70 -        \open " ^ thy_name ^ ";\n\
    1.71 -        \\n");
    1.72 -
    1.73 +    "val thy = " ^ old_thys ^ ";\n\n\
    1.74 +    \structure " ^ thy_name ^ " =\n\
    1.75 +    \struct\n\
    1.76 +    \\n\
    1.77 +    \local\n"
    1.78 +    ^ trfun_defs ^ "\n\
    1.79 +    \in\n\
    1.80 +    \\n"
    1.81 +    ^ mltxt ^ "\n\
    1.82 +    \\n\
    1.83 +    \val thy = thy\n\
    1.84 +    \\n\
    1.85 +    \|> Theory.add_path \"/\"\n" ^
    1.86 +    (case begin of
    1.87 +      None => (warning ("Flat name space for theory " ^ tname ^ "?  Consider begin ..."); "")
    1.88 +    | Some "" => "|> Theory.add_path " ^ quote tname ^ "\n"
    1.89 +    | Some path => "|> Theory.add_path " ^ path ^ "\n") ^
    1.90 +    "\n\
    1.91 +    \|> Theory.add_trfuns\n"
    1.92 +    ^ trfun_args ^ "\n\
    1.93 +    \|> Theory.add_trfunsT typed_print_translation \n\
    1.94 +    \|> Theory.add_tokentrfuns token_translation \n\
    1.95 +    \\n"
    1.96 +    ^ extxt ^ "\n\
    1.97 +    \\n\
    1.98 +    \|> Theory.add_name " ^ quote thy_name ^ ";\n\
    1.99 +    \\n\
   1.100 +    \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
   1.101 +    \\n\
   1.102 +    \\n"
   1.103 +    ^ postxt ^ "\n\
   1.104 +    \\n\
   1.105 +    \end;\n\
   1.106 +    \end;\n\
   1.107 +    \\n\
   1.108 +    \open " ^ thy_name ^ ";\n\
   1.109 +    \\n";
   1.110  
   1.111  fun theory_defn sectab tname =
   1.112 -  header -- optional (extension sectab >> Some) None -- eof
   1.113 -  >> (mk_structure tname o #1);
   1.114 +  header -- opt_extension sectab -- eof >> (mk_structure tname o #1);
   1.115  
   1.116  fun parse_thy (lex, sectab) tname str =
   1.117    #1 (!! (theory_defn sectab tname) (tokenize lex str));