1.1 --- a/src/Pure/Syntax/syntax.ML	Wed Jan 18 10:17:55 1995 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Jan 18 11:36:04 1995 +0100
     1.3 @@ -43,8 +43,7 @@
     1.4      (string * (term list -> term)) list *
     1.5      (string * (term list -> term)) list *
     1.6      (string * (ast list -> ast)) list -> syntax
     1.7 -  val extend_trrules: syntax ->
     1.8 -    (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax
     1.9 +  val extend_trrules: syntax -> xrule list -> syntax
    1.10    val merge_syntaxes: syntax -> syntax -> syntax
    1.11    val type_syn: syntax
    1.12    val pure_syn: syntax
    1.13 @@ -303,7 +302,7 @@
    1.14  
    1.15  (* read_ast *)
    1.16  
    1.17 -fun read_asts (Syntax tabs) print_msg xids root str =
    1.18 +fun read_asts (Syntax tabs) xids root str =
    1.19    let
    1.20      val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
    1.21      val root' = if root mem logtypes then logic else root;
    1.22 @@ -311,7 +310,7 @@
    1.23  
    1.24      fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
    1.25    in
    1.26 -    if print_msg andalso length pts > 1 then
    1.27 +    if length pts > 1 then
    1.28        (writeln ("Warning: Ambiguous input " ^ quote str);
    1.29         writeln "produces the following parse trees:"; seq show_pt pts)
    1.30      else ();
    1.31 @@ -324,7 +323,7 @@
    1.32  fun read (syn as Syntax tabs) ty str =
    1.33    let
    1.34      val {parse_ruletab, parse_trtab, ...} = tabs;
    1.35 -    val asts = read_asts syn true false (typ_to_nonterm ty) str;
    1.36 +    val asts = read_asts syn false (typ_to_nonterm ty) str;
    1.37    in
    1.38      map (ast_to_term (lookup_trtab parse_trtab))
    1.39        (map (normalize_ast (lookup_ruletab parse_ruletab)) asts)
    1.40 @@ -348,10 +347,9 @@
    1.41  fun simple_read_typ str = read_typ type_syn (K []) str;
    1.42  
    1.43  
    1.44 -(* read rules *)
    1.45 +(* read translation rules *)
    1.46  
    1.47 -fun read_rule (syn as Syntax tabs) print_msg
    1.48 -              (check_types: bool -> term list * typ -> int * term * 'a)
    1.49 +fun read_xrule (syn as Syntax tabs)
    1.50                (xrule as ((_, lhs_src), (_, rhs_src))) =
    1.51    let
    1.52      val Syntax {consts, ...} = syn;
    1.53 @@ -362,19 +360,12 @@
    1.54        | constantify (Appl asts) = Appl (map constantify asts);
    1.55  
    1.56      fun read_pat (root, str) =
    1.57 -      let val {parse_ruletab, parse_trtab, ...} = tabs;
    1.58 -          val asts = read_asts syn print_msg true root str;
    1.59 -          val ts = map (ast_to_term (lookup_trtab parse_trtab))
    1.60 -                     (map (normalize_ast (lookup_ruletab parse_ruletab)) asts);
    1.61 -
    1.62 -          val idx = if length ts = 1 then 0
    1.63 -            else (if print_msg then
    1.64 -                    writeln ("This occured in syntax translation rule: " ^
    1.65 -                             quote lhs_src ^ "  ->  " ^ quote rhs_src)
    1.66 -                  else ();
    1.67 -                  #1 (check_types print_msg (ts, Type (root, []))))
    1.68 -      in constantify (nth_elem (idx, asts))
    1.69 -           handle ERROR => error ("The error above occurred in " ^ quote str)
    1.70 +      let val asts = read_asts syn true root str;
    1.71 +      in if length asts > 1 then
    1.72 +           error "Error: This should not happen while parsing a syntax \
    1.73 +                  \translation rule."
    1.74 +         else constantify (hd asts)
    1.75 +            handle ERROR => error ("The error above occurred in " ^ quote str)
    1.76        end;
    1.77  
    1.78      val rule as (lhs, rhs) = (pairself read_pat) xrule;
    1.79 @@ -393,7 +384,7 @@
    1.80    op <-| of (string * string) * (string * string) |
    1.81    op <-> of (string * string) * (string * string);
    1.82  
    1.83 -fun read_xrules syn check_types xrules =
    1.84 +fun read_xrules syn xrules =
    1.85    let
    1.86      fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
    1.87        | right_rule (xpat1 <-| xpat2) = None
    1.88 @@ -402,12 +393,8 @@
    1.89      fun left_rule (xpat1 |-> xpat2) = None
    1.90        | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
    1.91        | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
    1.92 -
    1.93 -    val rrules = mapfilter right_rule xrules;
    1.94 -    val lrules = mapfilter left_rule xrules;
    1.95 -  in
    1.96 -    (map (read_rule syn true check_types) rrules,
    1.97 -     map (read_rule syn (rrules = []) check_types) lrules)
    1.98 +  in (map (read_xrule syn) (mapfilter right_rule xrules),
    1.99 +      map (read_xrule syn) (mapfilter left_rule xrules))
   1.100    end;
   1.101  
   1.102  
   1.103 @@ -451,7 +438,7 @@
   1.104  
   1.105  val extend_trfuns = ext_syntax syn_ext_trfuns;
   1.106  
   1.107 -fun extend_trrules syn check_types xrules =
   1.108 -  ext_syntax syn_ext_rules syn (read_xrules syn check_types xrules);
   1.109 +fun extend_trrules syn xrules =
   1.110 +  ext_syntax syn_ext_rules syn (read_xrules syn xrules);
   1.111  
   1.112  end;