src/Pure/Syntax/syntax.ML
changeset 174 319ff2d6760b
parent 171 ab0f93a291b5
child 175 c02750f7f604
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 30 11:08:18 1993 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 30 12:12:18 1993 +0100
     1.3 @@ -430,12 +430,17 @@
     1.4  
     1.5  (* extend *)  (* FIXME *)
     1.6  
     1.7 -fun old_extend syn read_ty (roots, xconsts, sext) =
     1.8 +fun extend syn read_ty (roots, xconsts, sext) =
     1.9    let
    1.10 -    val Syntax (ggr0, Tabs {roots = roots0, ...}) = syn;
    1.11 +    val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn;
    1.12  
    1.13      val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
    1.14 -    val (syn1 as Syntax (ggr1, tabs1)) = mk_syntax (ref (ExtGG (ggr0, ext1)));
    1.15 +
    1.16 +    val (syn1 as Syntax (ggr1, tabs1)) = 
    1.17 +      (case mk_xgram ext1 of
    1.18 +        xg1 as XGram {prods = [], ...} => 
    1.19 +          Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 xg1)
    1.20 +      | _ => mk_syntax (ref (ExtGG (ggr0, ext1))));
    1.21  
    1.22      val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
    1.23      val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
    1.24 @@ -444,28 +449,6 @@
    1.25    end;
    1.26  
    1.27  
    1.28 -fun new_extend syn read_ty (roots, xconsts, sext) =
    1.29 -  let
    1.30 -    val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn;
    1.31 -
    1.32 -    val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
    1.33 -    val (syn1 as Syntax (ggr1, tabs1)) =
    1.34 -      Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1));
    1.35 -
    1.36 -    val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
    1.37 -    val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
    1.38 -  in
    1.39 -    Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
    1.40 -  end;
    1.41 -
    1.42 -
    1.43 -fun extend syn read_ty (ex as (roots, _, sext)) =
    1.44 -  (case (roots, sext) of
    1.45 -    ([], Sext {mixfix = [], ...}) => new_extend
    1.46 -  | ([], NewSext {mixfix = [], ...}) => new_extend
    1.47 -  | _ => old_extend) syn read_ty ex;
    1.48 -
    1.49 -
    1.50  (* merge *)
    1.51  
    1.52  fun merge roots syn1 syn2 =