fixed 'begin';
authorwenzelm
Mon Oct 06 20:00:31 1997 +0200 (1997-10-06)
changeset 379860ae17f6f378
parent 3797 05e47c7cc6fd
child 3799 d00f6460ac4d
fixed 'begin';
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Oct 06 19:39:40 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 06 20:00:31 1997 +0200
     1.3 @@ -430,12 +430,12 @@
     1.4  
     1.5  (* extension *)
     1.6  
     1.7 -fun mk_extension (txts, mltxt) =
     1.8 +fun mk_extension ((has_begin, txts), mltxt) =
     1.9    let
    1.10      val cat_sects = space_implode "\n\n" o filter_out (equal "");
    1.11      val (extxts, postxts) = split_list txts;
    1.12    in
    1.13 -    (cat_sects extxts, cat_sects postxts, mltxt)
    1.14 +    (has_begin, cat_sects extxts, cat_sects postxts, mltxt)
    1.15    end;
    1.16  
    1.17  fun sect tab ((Keyword, s, n) :: toks) =
    1.18 @@ -445,19 +445,20 @@
    1.19    | sect _ ((_, s, n) :: _) = syn_err "section" s n
    1.20    | sect _ [] = eof_err ();
    1.21  
    1.22 -fun extension sectab = "+" $$-- !! (repeat (sect sectab) --$$ "end") --
    1.23 -  optional ("ML" $$-- verbatim) "" >> mk_extension;
    1.24 +fun extension sectab = "+" $$-- !!
    1.25 +  (optional ($$ "begin" >> K true) false -- (repeat (sect sectab) --$$ "end") --
    1.26 +    optional ("ML" $$-- verbatim) "") >> mk_extension;
    1.27  
    1.28  
    1.29  (* theory definition *)
    1.30  
    1.31 -fun mk_structure tname (((thy_name, old_thys), has_begin), opt_txts) =
    1.32 +fun mk_structure tname ((thy_name, old_thys), opt_ext) =
    1.33    if thy_name <> tname then
    1.34      error ("Filename \"" ^ tname ^ ".thy\" and theory name "
    1.35        ^ quote thy_name ^ " are different")
    1.36    else
    1.37 -    (case opt_txts of
    1.38 -      Some (extxt, postxt, mltxt) =>
    1.39 +    (case opt_ext of
    1.40 +      Some (has_begin, extxt, postxt, mltxt) =>
    1.41          "val thy = " ^ old_thys ^ " true;\n\n\
    1.42          \structure " ^ thy_name ^ " =\n\
    1.43          \struct\n\
    1.44 @@ -470,7 +471,7 @@
    1.45          \\n\
    1.46          \val thy = thy\n\
    1.47          \\n" ^
    1.48 -        (if has_begin then "Theory.add_path " ^ quote tname else "") ^
    1.49 +        (if has_begin then "|> Theory.add_path " ^ quote tname ^ "\n" else "") ^
    1.50          "\n\
    1.51          \|> Theory.add_trfuns\n"
    1.52          ^ trfun_args ^ "\n\
    1.53 @@ -509,8 +510,7 @@
    1.54  
    1.55  
    1.56  fun theory_defn sectab tname =
    1.57 -  header -- optional ($$ "begin" >> K true) false --
    1.58 -    optional (extension sectab >> Some) None -- eof
    1.59 +  header -- optional (extension sectab >> Some) None -- eof
    1.60    >> (mk_structure tname o #1);
    1.61  
    1.62  fun parse_thy (lex, sectab) tname str =