# HG changeset patch # User wenzelm # Date 1113670581 -7200 # Node ID 44260d72de35ec5d0a456b58e7ea1b9e102b48a5 # Parent 33bb955b2e733f2bf8f947764908c7b9a57ba0fe added del_modesyntax(_i); added print_all_data; diff -r 33bb955b2e73 -r 44260d72de35 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Apr 16 18:55:51 2005 +0200 +++ b/src/Pure/sign.ML Sat Apr 16 18:56:21 2005 +0200 @@ -138,6 +138,8 @@ val add_syntax_i: (bstring * typ * mixfix) list -> sg -> sg val add_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg val add_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg + val del_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg + val del_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg val add_trfuns: (string * (ast list -> ast)) list * (string * (term list -> term)) list * @@ -162,6 +164,7 @@ val hide_space_i: bool -> string * string list -> sg -> sg val add_name: string -> sg -> sg val data_kinds: data -> string list + val print_all_data: sg -> unit val merge_refs: sg_ref * sg_ref -> sg_ref val merge: sg * sg -> sg val copy: sg -> sg @@ -302,7 +305,7 @@ fun make_syntax sg (Syn (syntax, (atrs, trs, tr's, atr's))) = let - fun apply (s, (f, _: stamp)) = (s, f sg); + fun apply (c, (f, s)) = (c, (f sg, s)); fun prep tab = map apply (Symtab.dest tab); fun prep' tab = map apply (Symtab.dest_multi tab); in syntax |> Syntax.extend_trfuns (prep atrs, prep trs, prep' tr's, prep' atr's) end; @@ -314,16 +317,16 @@ fun extend_trfuns (atrs, trs, tr's, atr's) (Syn (syn, (parse_ast_trtab, parse_trtab, print_trtab, print_ast_trtab))) = - Syn (syn, (Syntax.extend_trtab parse_ast_trtab atrs "parse ast translation", - Syntax.extend_trtab parse_trtab trs "parse translation", - Syntax.extend_tr'tab print_trtab tr's, - Syntax.extend_tr'tab print_ast_trtab atr's)); + Syn (syn, (Syntax.extend_trtab "parse ast translation" atrs parse_ast_trtab, + Syntax.extend_trtab "parse translation" trs parse_trtab, + Syntax.extend_tr'tab tr's print_trtab, + Syntax.extend_tr'tab atr's print_ast_trtab)); fun merge_trfuns (parse_ast_trtab1, parse_trtab1, print_trtab1, print_ast_trtab1) (parse_ast_trtab2, parse_trtab2, print_trtab2, print_ast_trtab2) = - (Syntax.merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation", - Syntax.merge_trtabs parse_trtab1 parse_trtab2 "parse translation", + (Syntax.merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2, + Syntax.merge_trtabs "parse translation" parse_trtab1 parse_trtab2, Syntax.merge_tr'tabs print_trtab1 print_trtab2, Syntax.merge_tr'tabs print_ast_trtab1 print_ast_trtab2); @@ -424,6 +427,9 @@ let val (e, (_, _, _, prt)) = lookup_data sg tab kind in prt sg e handle exn => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn end; +fun print_all_data (sg as Sg (_, {data = Data tab, ...})) = + app (fn kind => print_data kind sg) (map (#1 o #2) (Symtab.dest tab)); + fun put_data_sg sg (Data tab) kind f x = Data (Symtab.update ((Object.name_of_kind kind, (kind, (f x, snd (lookup_data sg tab kind)))), tab)); @@ -1001,7 +1007,7 @@ (c, rd_raw_typ (make_syntax sg syn) tsig spaces (K NONE) ty_src, mx) handle ERROR => err_in_const (const_name path c mx); -fun ext_cnsts rd_const syn_only prmode sg (syn, tsig, ctab, (path, spaces), data) +fun change_cnsts change_gram rd_const syn_only prmode sg (syn, tsig, ctab, (path, spaces), data) raw_consts = let val prep_typ = compress_type o Type.varifyT o Type.no_tvars o @@ -1014,18 +1020,24 @@ if syn_only then [] else decls_of path Syntax.const_name consts; in - (map_syntax (Syntax.extend_const_gram (is_logtype sg) prmode consts) syn, tsig, + (map_syntax (change_gram (is_logtype sg) prmode consts) syn, tsig, Symtab.extend (ctab, map (fn (c, T) => (c, (T, stamp ()))) decls) handle Symtab.DUPS cs => err_dup_consts cs, (path, add_names spaces constK (map fst decls)), data) end; +fun ext_cnsts rd = change_cnsts Syntax.extend_const_gram rd; +fun rem_cnsts rd = change_cnsts Syntax.remove_const_gram rd; + fun ext_consts_i x = ext_cnsts no_read false Syntax.default_mode x; -fun ext_consts x = ext_cnsts read_cnst false Syntax.default_mode x; +fun ext_consts x = ext_cnsts read_cnst false Syntax.default_mode x; fun ext_syntax_i x = ext_cnsts no_read true Syntax.default_mode x; -fun ext_syntax x = ext_cnsts read_cnst true Syntax.default_mode x; -fun ext_modesyntax_i x y (prmode, consts) = ext_cnsts no_read true prmode x y consts; -fun ext_modesyntax x y (prmode, consts) = ext_cnsts read_cnst true prmode x y consts; +fun ext_syntax x = ext_cnsts read_cnst true Syntax.default_mode x; + +fun ext_modesyntax_i x y (m, cs) = ext_cnsts no_read true m x y cs; +fun ext_modesyntax x y (m, cs) = ext_cnsts read_cnst true m x y cs; +fun rem_modesyntax_i x y (m, cs) = rem_cnsts no_read true m x y cs; +fun rem_modesyntax x y (m, cs) = rem_cnsts read_cnst true m x y cs; (* add type classes *) @@ -1070,19 +1082,27 @@ (* add translation functions *) +local + +fun mk trs = map Syntax.mk_trfun trs; + fun ext_trfs ext non_typed sg (syn, tsig, ctab, names, data) (atrs, trs, tr's, atr's) = - let val syn' = syn |> ext (atrs, trs, map (apsnd non_typed) tr's, atr's) + let val syn' = syn |> ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's) in make_syntax sg syn'; (syn', tsig, ctab, names, data) end; fun ext_trfsT ext sg (syn, tsig, ctab, names, data) tr's = - let val syn' = syn |> ext ([], [], tr's, []) + let val syn' = syn |> ext ([], [], mk tr's, []) in make_syntax sg syn'; (syn', tsig, ctab, names, data) end; +in + fun ext_trfuns sg = ext_trfs (map_syntax o Syntax.extend_trfuns) Syntax.non_typed_tr' sg; fun ext_trfunsT sg = ext_trfsT (map_syntax o Syntax.extend_trfuns) sg; fun ext_advanced_trfuns sg = ext_trfs extend_trfuns Syntax.non_typed_tr'' sg; fun ext_advanced_trfunsT sg = ext_trfsT extend_trfuns sg; +end; + (* add token translation functions *) @@ -1169,6 +1189,8 @@ val add_syntax_i = extend_sign true ext_syntax_i "#"; val add_modesyntax = extend_sign true ext_modesyntax "#"; val add_modesyntax_i = extend_sign true ext_modesyntax_i "#"; +val del_modesyntax = extend_sign true rem_modesyntax "#"; +val del_modesyntax_i = extend_sign true rem_modesyntax_i "#"; val add_trfuns = extend_sign true ext_trfuns "#"; val add_trfunsT = extend_sign true ext_trfunsT "#"; val add_advanced_trfuns = extend_sign true ext_advanced_trfuns "#";