--- a/src/Pure/Syntax/printer.ML Sat Nov 24 17:00:35 2001 +0100
+++ b/src/Pure/Syntax/printer.ML Sat Nov 24 17:01:00 2001 +0100
@@ -48,11 +48,11 @@
(* apply print (ast) translation function *)
-fun apply_last [] x = raise Match
- | apply_last (f :: fs) x = apply_last fs x handle Match => f x;
+fun apply_first [] x = raise Match
+ | apply_first (f :: fs) x = f x handle Match => apply_first fs x;
fun apply_trans name a fs args =
- (apply_last fs args handle
+ (apply_first fs args handle
Match => raise Match
| exn => (priority ("Error in " ^ name ^ " for " ^ quote a); raise exn));
@@ -77,7 +77,6 @@
fun ast_of_termT trf tm =
let
- (* FIXME improve: lookup token classes *)
fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
| ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
| ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
@@ -236,23 +235,16 @@
fun extend_prtabs prtabs mode xprods =
let
- val fmts = rev (mapfilter xprod_to_fmt xprods);
+ val fmts = mapfilter xprod_to_fmt xprods;
val tab = get_tab prtabs mode;
- val new_tab =
- if null fmts then tab
- else Symtab.make_multi (fmts @ Symtab.dest_multi tab) (*prefer new entries*)
+ val new_tab = foldr Symtab.update_multi (rev fmts, tab);
in overwrite (prtabs, (mode, new_tab)) end;
fun merge_prtabs prtabs1 prtabs2 =
let
val modes = distinct (map fst (prtabs1 @ prtabs2));
- fun merge mode =
- (mode,
- generic_merge (op =) Symtab.dest_multi Symtab.make_multi
- (get_tab prtabs2 mode) (get_tab prtabs1 mode)); (*prefer 2nd over 1st*)
- in
- map merge modes
- end;
+ fun merge m = (m, Symtab.merge_multi' (op =) (get_tab prtabs1 m, get_tab prtabs2 m));
+ in map merge modes end;
--- a/src/Pure/Syntax/syntax.ML Sat Nov 24 17:00:35 2001 +0100
+++ b/src/Pure/Syntax/syntax.ML Sat Nov 24 17:01:00 2001 +0100
@@ -69,7 +69,7 @@
(** tables of translation functions **)
fun mk_trfun (c, f) = (c, (f, stamp ()));
-fun eq_trfuns ((c1:string, (_, s1:stamp)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
+fun eq_trfuns ((_, s1:stamp), (_, s2)) = s1 = s2;
(* parse (ast) translations *)
@@ -91,11 +91,8 @@
(* print (ast) translations *)
fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
-
-fun extend_tr'tab tab trfuns =
- generic_extend eq_trfuns Symtab.dest_multi Symtab.make_multi tab (map mk_trfun trfuns);
-
-fun merge_tr'tabs tabs = generic_merge eq_trfuns Symtab.dest_multi Symtab.make_multi tabs;
+fun extend_tr'tab tab trfuns = foldr Symtab.update_multi (map mk_trfun trfuns, tab);
+fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' eq_trfuns (tab1, tab2);
@@ -147,11 +144,9 @@
(* empty, extend, merge ruletabs *)
fun extend_ruletab tab rules =
- generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab
- (map (fn r => (Ast.head_of_rule r, r)) (distinct rules));
+ foldr Symtab.update_multi (map (fn r => (Ast.head_of_rule r, r)) rules, tab);
-fun merge_ruletabs tab1 tab2 =
- generic_merge (op =) Symtab.dest_multi Symtab.make_multi tab1 tab2;
+fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
@@ -206,7 +201,7 @@
in
Syntax {
lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon,
- logtypes = extend_list logtypes1 logtypes2,
+ logtypes = merge_lists logtypes1 logtypes2,
gram = if inout then Parser.extend_gram gram xprods else gram,
consts = consts2 @ consts1,
prmodes = (mode ins_string prmodes2) union_string prmodes1,
@@ -350,8 +345,8 @@
val chars = Symbol.explode str;
val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
- fun show_pt pt = warning (Pretty.string_of
- (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
+ fun show_pt pt =
+ warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
in
if length pts > ! ambiguity_level then
(warning ("Ambiguous input " ^ quote str);