# HG changeset patch # User wenzelm # Date 1183917118 -7200 # Node ID d2d1138e0ddcf7063dae968a84162b35ae524b01 # Parent a2ad1c166ac8b736cb1f18259e55bcb519196a01 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP; diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/General/graph.ML Sun Jul 08 19:51:58 2007 +0200 @@ -10,7 +10,6 @@ type key type 'a T exception DUP of key - exception DUPS of key list exception SAME exception UNDEF of key val empty: 'a T @@ -36,9 +35,9 @@ val is_edge: 'a T -> key * key -> bool val add_edge: key * key -> 'a T -> 'a T val del_edge: key * key -> 'a T -> 'a T - val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUPS*) + val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*) val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> - 'a T * 'a T -> 'a T (*exception DUPS*) + 'a T * 'a T -> 'a T (*exception DUP*) val irreducible_paths: 'a T -> key * key -> key list list val all_paths: 'a T -> key * key -> key list list exception CYCLES of key list list @@ -78,7 +77,6 @@ datatype 'a T = Graph of ('a * (key list * key list)) Table.table; exception DUP = Table.DUP; -exception DUPS = Table.DUPS; exception UNDEF = Table.UNDEF; exception SAME = Table.SAME; diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/General/table.ML --- a/src/Pure/General/table.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/General/table.ML Sun Jul 08 19:51:58 2007 +0200 @@ -17,7 +17,6 @@ type key type 'a table exception DUP of key - exception DUPS of key list exception SAME exception UNDEF of key val empty: 'a table @@ -39,11 +38,11 @@ val default: key * 'a -> 'a table -> 'a table val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table - val make: (key * 'a) list -> 'a table (*exception DUPS*) - val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*) + val make: (key * 'a) list -> 'a table (*exception DUP*) + val extend: 'a table * (key * 'a) list -> 'a table (*exception DUP*) val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> - 'a table * 'a table -> 'a table (*exception DUPS*) - val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUPS*) + 'a table * 'a table -> 'a table (*exception DUP*) + val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*) val delete: key -> 'a table -> 'a table (*exception UNDEF*) val delete_safe: key -> 'a table -> 'a table val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool @@ -56,7 +55,7 @@ val make_list: (key * 'a) list -> 'a list table val dest_list: 'a list table -> (key * 'a) list val merge_list: ('a * 'a -> bool) -> - 'a list table * 'a list table -> 'a list table (*exception DUPS*) + 'a list table * 'a list table -> 'a list table (*exception DUP*) end; functor TableFun(Key: KEY): TABLE = @@ -73,7 +72,6 @@ Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table; exception DUP of key; -exception DUPS of key list; (* empty *) @@ -350,23 +348,13 @@ (* simultaneous modifications *) -fun reject_dups (tab, []) = tab - | reject_dups (_, dups) = raise DUPS (rev dups); - -fun extend (table, args) = - let - fun add (key, x) (tab, dups) = - (update_new (key, x) tab, dups) handle DUP dup => (tab, dup :: dups); - in reject_dups (fold add args (table, [])) end; +fun extend (table, args) = fold update_new args table; fun make entries = extend (empty, entries); fun join f (table1, table2) = - let - fun add (key, y) (tab, dups) = - let val tab' = modify key (fn NONE => y | SOME x => f key (x, y)) tab - in (tab', dups) end handle DUP dup => (tab, dup :: dups); - in reject_dups (fold_table add table2 (table1, [])) end; + let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab; + in fold_table add table2 table1 end; fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key); diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/Isar/attrib.ML Sun Jul 08 19:51:58 2007 +0200 @@ -54,8 +54,8 @@ val empty = NameSpace.empty_table; val copy = I; val extend = I; - fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups => - error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups); + fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup => + error ("Attempt to merge different versions of attribute " ^ quote dup); ); fun print_attributes thy = @@ -128,8 +128,7 @@ val new_attrs = raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ()))); fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs - handle Symtab.DUPS dups => - error ("Duplicate declaration of attributes(s) " ^ commas_quote dups); + handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup); in AttributesData.map add thy end; @@ -138,7 +137,7 @@ (* tags *) -fun tag x = Scan.lift (Args.name -- Scan.repeat Args.name) x; +fun tag x = Scan.lift (Args.name -- Args.name) x; (* theorems *) diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/Isar/locale.ML Sun Jul 08 19:51:58 2007 +0200 @@ -623,8 +623,8 @@ fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss - handle Symtab.DUPS xs => err_in_locale ctxt - ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids); + handle Symtab.DUP x => err_in_locale ctxt + ("Conflicting syntax for parameter: " ^ quote x) (map fst ids); (* Distinction of assumed vs. derived identifiers. @@ -722,8 +722,8 @@ fun merge_syn expr syn1 syn2 = Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2) - handle Symtab.DUPS xs => err_in_expr ctxt - ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr; + handle Symtab.DUP x => err_in_expr ctxt + ("Conflicting syntax for parameter: " ^ quote x) expr; fun params_of (expr as Locale name) = let @@ -1063,8 +1063,8 @@ ((ids', merge_syntax ctxt ids' (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes)) - handle Symtab.DUPS xs => err_in_locale ctxt - ("Conflicting syntax for parameters: " ^ commas_quote xs) + handle Symtab.DUP x => err_in_locale ctxt + ("Conflicting syntax for parameter: " ^ quote x) (map #1 ids')), [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))]) end @@ -2062,9 +2062,9 @@ val eqns' = case get_reg thy_ctxt'' id of NONE => eqns | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns') -(* handle Termtab.DUPS ts => - error (implode ("Conflicting equations for terms" :: - map (quote o ProofContext.string_of_term ctxt) ts)) +(* handle Termtab.DUP t => + error (implode ("Conflicting equations for term " :: + quote (ProofContext.string_of_term ctxt t))) *) in ((id, eqns'), eqns') end; val all_eqns = fold_map add_eqns all_elemss Termtab.empty |> fst diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/Isar/method.ML Sun Jul 08 19:51:58 2007 +0200 @@ -389,8 +389,8 @@ val empty = NameSpace.empty_table; val copy = I; val extend = I; - fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups => - error ("Attempt to merge different versions of method(s) " ^ commas_quote dups); + fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup => + error ("Attempt to merge different versions of method " ^ quote dup); ); fun print_methods thy = @@ -430,8 +430,7 @@ (name, ((f, comment), stamp ()))); fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths - handle Symtab.DUPS dups => - error ("Duplicate declaration of method(s) " ^ commas_quote dups); + handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup); in MethodsData.map add thy end; val add_method = add_methods o Library.single; diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/Syntax/syntax.ML Sun Jul 08 19:51:58 2007 +0200 @@ -98,16 +98,16 @@ fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c); -fun err_dup_trfuns name cs = - error ("More than one " ^ name ^ " for " ^ commas_quote cs); +fun err_dup_trfun name c = + error ("More than one " ^ name ^ " for " ^ quote c); fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns; fun extend_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns) - handle Symtab.DUPS cs => err_dup_trfuns name cs; + handle Symtab.DUP c => err_dup_trfun name c; fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2) - handle Symtab.DUPS cs => err_dup_trfuns name cs; + handle Symtab.DUP c => err_dup_trfun name c; (* print (ast) translations *) diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/Thy/term_style.ML --- a/src/Pure/Thy/term_style.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/Thy/term_style.ML Sun Jul 08 19:51:58 2007 +0200 @@ -18,8 +18,8 @@ (* style data *) -fun err_dup_styles names = - error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names); +fun err_dup_style name = + error ("Duplicate declaration of antiquote style: " ^ quote name); structure StyleData = TheoryDataFun ( @@ -28,7 +28,7 @@ val copy = I; val extend = I; fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs - handle Symtab.DUPS dups => err_dup_styles dups; + handle Symtab.DUP dup => err_dup_style dup; ); fun print_styles thy = @@ -44,7 +44,7 @@ fun add_style name style thy = StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy - handle Symtab.DUP _ => err_dup_styles [name]; + handle Symtab.DUP _ => err_dup_style name; (* predefined styles *) diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/codegen.ML Sun Jul 08 19:51:58 2007 +0200 @@ -894,7 +894,7 @@ (map (fn s => case Symtab.lookup graphs s of NONE => error ("Undefined code module: " ^ s) | SOME gr => gr) modules)) - handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); + handle Graph.DUP k => error ("Duplicate code for " ^ k); fun expand (t as Abs _) = t | expand t = (case fastype_of t of Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t); diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/consts.ML --- a/src/Pure/consts.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/consts.ML Sun Jul 08 19:51:58 2007 +0200 @@ -196,14 +196,14 @@ (** build consts **) -fun err_dup_consts cs = - error ("Duplicate declaration of constant(s) " ^ commas_quote cs); +fun err_dup_const c = + error ("Duplicate declaration of constant " ^ quote c); -fun err_inconsistent_constraints cs = - error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs); +fun err_inconsistent_constraints c = + error ("Inconsistent type constraints for constant " ^ quote c); fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab - handle Symtab.DUPS cs => err_dup_consts cs; + handle Symtab.DUP c => err_dup_const c; (* name space *) @@ -303,9 +303,9 @@ rev_abbrevs = rev_abbrevs2, do_expand = do_expand2}, _)) = let val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2) - handle Symtab.DUPS cs => err_dup_consts cs; + handle Symtab.DUP c => err_dup_const c; val constraints' = Symtab.merge (op =) (constraints1, constraints2) - handle Symtab.DUPS cs => err_inconsistent_constraints cs; + handle Symtab.DUP c => err_inconsistent_constraints c; val rev_abbrevs' = (rev_abbrevs1, rev_abbrevs2) |> Symtab.join (K (Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u'))); val do_expand' = do_expand1 orelse do_expand2; diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/simplifier.ML Sun Jul 08 19:51:58 2007 +0200 @@ -167,8 +167,7 @@ (** named simprocs **) -fun err_dup_simprocs ds = - error ("Duplicate simproc(s): " ^ commas_quote ds); +fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name); (* data *) @@ -179,7 +178,7 @@ val empty = NameSpace.empty_table; val extend = I; fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs - handle Symtab.DUPS ds => err_dup_simprocs ds; + handle Symtab.DUP dup => err_dup_simproc dup; ); @@ -229,7 +228,7 @@ context |> Simprocs.map (fn simprocs => NameSpace.extend_table naming [(name', simproc')] simprocs - handle Symtab.DUPS ds => err_dup_simprocs ds) + handle Symtab.DUP dup => err_dup_simproc dup) |> map_ss (fn ss => ss addsimprocs [simproc']) end) end; diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/sorts.ML --- a/src/Pure/sorts.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/sorts.ML Sun Jul 08 19:51:58 2007 +0200 @@ -183,8 +183,7 @@ (* classes *) -fun err_dup_classes cs = - error ("Duplicate declaration of class(es): " ^ commas_quote cs); +fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c); fun err_cyclic_classes pp css = error (cat_lines (map (fn cs => @@ -193,7 +192,7 @@ fun add_class pp (c, cs) = map_classes (fn classes => let val classes' = classes |> Graph.new_node (c, serial ()) - handle Graph.DUP dup => err_dup_classes [dup]; + handle Graph.DUP dup => err_dup_class dup; val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs) handle Graph.CYCLES css => err_cyclic_classes pp css; in classes'' end); @@ -274,7 +273,7 @@ Algebra {classes = classes2, arities = arities2}) = let val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2) - handle Graph.DUPS cs => err_dup_classes cs + handle Graph.DUP c => err_dup_class c | Graph.CYCLES css => err_cyclic_classes pp css; val algebra0 = make_algebra (classes', Symtab.empty); val arities' = Symtab.empty diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/theory.ML --- a/src/Pure/theory.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/theory.ML Sun Jul 08 19:51:58 2007 +0200 @@ -96,8 +96,8 @@ fun make_thy (axioms, defs, oracles) = Thy {axioms = axioms, defs = defs, oracles = oracles}; -fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups); -fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups); +fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup); +fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup); structure ThyData = TheoryDataFun ( @@ -115,7 +115,7 @@ val axioms = NameSpace.empty_table; val defs = Defs.merge pp (defs1, defs2); val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2) - handle Symtab.DUPS dups => err_dup_oras dups; + handle Symtab.DUP dup => err_dup_ora dup; in make_thy (axioms, defs, oracles) end; ); @@ -182,7 +182,7 @@ let val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms; val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms - handle Symtab.DUPS dups => err_dup_axms dups; + handle Symtab.DUP dup => err_dup_axm dup; in axioms' end); in @@ -307,7 +307,7 @@ fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles => NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles - handle Symtab.DUPS dups => err_dup_oras dups); + handle Symtab.DUP dup => err_dup_ora dup); end; diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/type.ML --- a/src/Pure/type.ML Sun Jul 08 19:51:55 2007 +0200 +++ b/src/Pure/type.ML Sun Jul 08 19:51:58 2007 +0200 @@ -570,7 +570,7 @@ fun merge_types (types1, types2) = NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2) - handle Symtab.DUPS (d :: _) => err_in_decls d (the_decl types1 d) (the_decl types2 d); + handle Symtab.DUP d => err_in_decls d (the_decl types1 d) (the_decl types2 d); end;