# HG changeset patch # User wenzelm # Date 1177581605 -7200 # Node ID 34c316d7b630c8c96c76b6de972d0445ae78559a # Parent 702542e7f88ce11e52dcc79ee6563b73e2f3a2ad renamed some old names Theory.xxx to Sign.xxx; diff -r 702542e7f88c -r 34c316d7b630 src/HOLCF/cont_consts.ML --- a/src/HOLCF/cont_consts.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/HOLCF/cont_consts.ML Thu Apr 26 12:00:05 2007 +0200 @@ -85,10 +85,10 @@ val transformed_decls = map transform contconst_decls; in thy - |> Theory.add_consts_i normal_decls - |> Theory.add_consts_i (map first transformed_decls) - |> Theory.add_syntax_i (map second transformed_decls) - |> Theory.add_trrules_i (List.concat (map third transformed_decls)) + |> Sign.add_consts_i normal_decls + |> Sign.add_consts_i (map first transformed_decls) + |> Sign.add_syntax_i (map second transformed_decls) + |> Sign.add_trrules_i (List.concat (map third transformed_decls)) end; val add_consts = gen_add_consts Sign.read_typ; diff -r 702542e7f88c -r 34c316d7b630 src/HOLCF/domain/syntax.ML --- a/src/HOLCF/domain/syntax.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/HOLCF/domain/syntax.ML Thu Apr 26 12:00:05 2007 +0200 @@ -144,7 +144,7 @@ in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ (if length eqs'>1 then [const_copy] else[])@ [const_bisim]) - |> Theory.add_trrules_i (List.concat(map snd ctt)) + |> Sign.add_trrules_i (List.concat(map snd ctt)) end; (* let *) end; (* local *) diff -r 702542e7f88c -r 34c316d7b630 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/Isar/constdefs.ML Thu Apr 26 12:00:05 2007 +0200 @@ -49,7 +49,7 @@ val thy' = thy - |> Theory.add_consts_i [(c, T, mx)] + |> Sign.add_consts_i [(c, T, mx)] |> PureThy.add_defs_i false [((name, def), atts)] |-> (fn [thm] => CodegenData.add_func false thm); in ((c, T), thy') end; diff -r 702542e7f88c -r 34c316d7b630 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Apr 26 12:00:05 2007 +0200 @@ -82,7 +82,7 @@ val defaultsortP = OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl - (P.sort >> (Toplevel.theory o Theory.add_defsort)); + (P.sort >> (Toplevel.theory o Sign.add_defsort)); val axclassP = OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl @@ -97,18 +97,18 @@ val typedeclP = OuterSyntax.command "typedecl" "type declaration" K.thy_decl (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => - Toplevel.theory (Theory.add_typedecls [(a, args, mx)]))); + Toplevel.theory (Sign.add_typedecls [(a, args, mx)]))); val typeabbrP = OuterSyntax.command "types" "declare type abbreviations" K.thy_decl (Scan.repeat1 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) - >> (Toplevel.theory o Theory.add_tyabbrs o + >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); val nontermP = OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" - K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals)); + K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals)); val aritiesP = OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl @@ -123,7 +123,7 @@ val constsP = OuterSyntax.command "consts" "declare constants" K.thy_decl - (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts)); + (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts)); val opt_overloaded = P.opt_keyword "overloaded"; @@ -139,11 +139,11 @@ val syntaxP = OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl - (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax)); + (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax)); val no_syntaxP = OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl - (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax)); + (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax)); (* translations *) @@ -162,11 +162,11 @@ val translationsP = OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl - (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules)); + (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules)); val no_translationsP = OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl - (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules)); + (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules)); (* axioms and definitions *) diff -r 702542e7f88c -r 34c316d7b630 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/Isar/locale.ML Thu Apr 26 12:00:05 2007 +0200 @@ -1551,10 +1551,10 @@ fun global_note_prefix_i kind (fully_qualified, prfx) args thy = thy - |> Theory.qualified_names - |> (if fully_qualified then Theory.sticky_prefix prfx else Theory.add_path prfx) + |> Sign.qualified_names + |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx) |> PureThy.note_thmss_i kind args - ||> Theory.restore_naming thy; + ||> Sign.restore_naming thy; fun local_note_prefix_i kind (fully_qualified, prfx) args ctxt = ctxt @@ -1726,8 +1726,8 @@ val ([pred_def], defs_thy) = thy |> (if bodyT <> propT then I else - Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), [])) - |> Theory.add_consts_i [(bname, predT, NoSyn)] + Sign.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), [])) + |> Sign.add_consts_i [(bname, predT, NoSyn)] |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])]; val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; diff -r 702542e7f88c -r 34c316d7b630 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/Isar/object_logic.ML Thu Apr 26 12:00:05 2007 +0200 @@ -80,8 +80,8 @@ in -val add_judgment = gen_add_judgment Theory.add_consts; -val add_judgment_i = gen_add_judgment Theory.add_consts_i; +val add_judgment = gen_add_judgment Sign.add_consts; +val add_judgment_i = gen_add_judgment Sign.add_consts_i; end; diff -r 702542e7f88c -r 34c316d7b630 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Apr 26 12:00:05 2007 +0200 @@ -38,8 +38,8 @@ thy |> Theory.copy |> Theory.root_path - |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)] - |> Theory.add_consts + |> Sign.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)] + |> Sign.add_consts [("typeof", "'b::{} => Type", NoSyn), ("Type", "'a::{} itself => Type", NoSyn), ("Null", "Null", NoSyn), @@ -735,7 +735,7 @@ val fu = Type.freeze u; val (def_thms, thy') = if t = nullt then ([], thy) else thy - |> Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] + |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |> PureThy.add_defs_i false [((extr_name s vs ^ "_def", Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])] in @@ -752,9 +752,9 @@ in thy - |> Theory.absolute_path + |> Sign.absolute_path |> fold_rev add_def defs - |> Theory.restore_naming thy + |> Sign.restore_naming thy end; diff -r 702542e7f88c -r 34c316d7b630 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Thu Apr 26 12:00:05 2007 +0200 @@ -41,18 +41,18 @@ fun add_proof_atom_consts names thy = thy - |> Theory.absolute_path - |> Theory.add_consts_i (map (fn name => (name, proofT, NoSyn)) names); + |> Sign.absolute_path + |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names); (** constants for application and abstraction **) fun add_proof_syntax thy = thy |> Theory.copy - |> Theory.root_path - |> Theory.add_defsort_i [] - |> Theory.add_types [("proof", 0, NoSyn)] - |> Theory.add_consts_i + |> Sign.root_path + |> Sign.add_defsort_i [] + |> Sign.add_types [("proof", 0, NoSyn)] + |> Sign.add_consts_i [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), ("Abst", (aT --> proofT) --> proofT, NoSyn), @@ -60,8 +60,8 @@ ("Hyp", propT --> proofT, NoSyn), ("Oracle", propT --> proofT, NoSyn), ("MinProof", proofT, Delimfix "?")] - |> Theory.add_nonterminals ["param", "params"] - |> Theory.add_syntax_i + |> Sign.add_nonterminals ["param", "params"] + |> Sign.add_syntax_i [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), @@ -69,13 +69,13 @@ ("", paramT --> paramT, Delimfix "'(_')"), ("", idtT --> paramsT, Delimfix "_"), ("", paramT --> paramsT, Delimfix "_")] - |> Theory.add_modesyntax_i ("xsymbols", true) + |> Sign.add_modesyntax_i ("xsymbols", true) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\_./ _)", [0, 3], 3)), ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] - |> Theory.add_modesyntax_i ("latex", false) + |> Sign.add_modesyntax_i ("latex", false) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3))] - |> Theory.add_trrules_i (map Syntax.ParsePrintRule + |> Sign.add_trrules_i (map Syntax.ParsePrintRule [(Syntax.mk_appl (Constant "_Lam") [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"], Syntax.mk_appl (Constant "_Lam") diff -r 702542e7f88c -r 34c316d7b630 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/ROOT.ML Thu Apr 26 12:00:05 2007 +0200 @@ -101,8 +101,8 @@ structure Pure = struct val thy = theory "Pure" end; Context.add_setup - (Theory.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> - Theory.add_syntax Syntax.applC_syntax); + (Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #> + Sign.add_syntax Syntax.applC_syntax); use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end; diff -r 702542e7f88c -r 34c316d7b630 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/Thy/html.ML Thu Apr 26 12:00:05 2007 +0200 @@ -250,7 +250,7 @@ ("var", style "var"), ("xstr", style "xstr")]; -val _ = Context.add_setup (Theory.add_mode_tokentrfuns htmlN html_trans); +val _ = Context.add_setup (Sign.add_mode_tokentrfuns htmlN html_trans); diff -r 702542e7f88c -r 34c316d7b630 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/pure_thy.ML Thu Apr 26 12:00:05 2007 +0200 @@ -408,10 +408,10 @@ fun note_thmss_qualified k path facts thy = thy - |> Theory.add_path path - |> Theory.no_base_names + |> Sign.add_path path + |> Sign.no_base_names |> note_thmss_i k facts - ||> Theory.restore_naming thy; + ||> Sign.restore_naming thy; (* store_thm *) @@ -487,12 +487,12 @@ val add_axioms_i = add_singles Theory.add_axioms_i; val add_axiomss = add_multis Theory.add_axioms; val add_axiomss_i = add_multis Theory.add_axioms_i; - val add_defs = add_singles o (Theory.add_defs false); - val add_defs_i = add_singles o (Theory.add_defs_i false); - val add_defs_unchecked = add_singles o (Theory.add_defs true); - val add_defs_unchecked_i = add_singles o (Theory.add_defs_i true); - val add_defss = add_multis o (Theory.add_defs false); - val add_defss_i = add_multis o (Theory.add_defs_i false); + val add_defs = add_singles o Theory.add_defs false; + val add_defs_i = add_singles o Theory.add_defs_i false; + val add_defs_unchecked = add_singles o Theory.add_defs true; + val add_defs_unchecked_i = add_singles o Theory.add_defs_i true; + val add_defss = add_multis o Theory.add_defs false; + val add_defss_i = add_multis o Theory.add_defs_i false; end; @@ -509,13 +509,13 @@ |> Theory.init_data |> Proofterm.init_data |> TheoremsData.init - |> Theory.add_types + |> Sign.add_types [("fun", 2, NoSyn), ("prop", 0, NoSyn), ("itself", 1, NoSyn), ("dummy", 0, NoSyn)] - |> Theory.add_nonterminals Syntax.basic_nonterms - |> Theory.add_syntax + |> Sign.add_nonterminals Syntax.basic_nonterms + |> Sign.add_syntax [("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), ("_abs", "'a", NoSyn), ("", "'a => args", Delimfix "_"), @@ -553,8 +553,8 @@ ("_struct", "index => logic", Mixfix ("\\_", [1000], 1000)), ("==>", "prop => prop => prop", Delimfix "op ==>"), (Term.dummy_patternN, "aprop", Delimfix "'_")] - |> Theory.add_syntax Syntax.appl_syntax - |> Theory.add_modesyntax (Symbol.xsymbolsN, true) + |> Sign.add_syntax Syntax.appl_syntax + |> Sign.add_modesyntax (Symbol.xsymbolsN, true) [("fun", "[type, type] => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), ("_bracket", "[types, type] => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", "[tid, sort] => type", Mixfix ("_\\_", [1000, 0], 1000)), @@ -569,13 +569,13 @@ ("_DDDOT", "aprop", Delimfix "\\"), ("_bigimpl", "[asms, prop] => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", "logic", Delimfix "\\")] - |> Theory.add_modesyntax ("", false) + |> Sign.add_modesyntax ("", false) [("prop", "prop => prop", Mixfix ("_", [0], 0)), ("ProtoPure.term", "'a => prop", Delimfix "TERM _"), ("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))] - |> Theory.add_modesyntax ("HTML", false) + |> Sign.add_modesyntax ("HTML", false) [("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\_./ _)", [0, 3], 3))] - |> Theory.add_consts + |> Sign.add_consts [("==", "'a => 'a => prop", InfixrName ("==", 2)), ("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), ("all", "('a => prop) => prop", Binder ("!!", 0, 0)), @@ -588,10 +588,10 @@ Const ("all", (aT --> propT) --> propT), Const ("TYPE", Term.a_itselfT), Const (Term.dummy_patternN, aT)] - |> Theory.add_trfuns Syntax.pure_trfuns - |> Theory.add_trfunsT Syntax.pure_trfunsT + |> Sign.add_trfuns Syntax.pure_trfuns + |> Sign.add_trfunsT Syntax.pure_trfunsT |> Sign.local_path - |> Theory.add_consts + |> Sign.add_consts [("term", "'a => prop", NoSyn), ("conjunction", "prop => prop => prop", NoSyn)] |> (add_defs false o map Thm.no_attributes) diff -r 702542e7f88c -r 34c316d7b630 src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Apr 26 12:00:01 2007 +0200 +++ b/src/Pure/sign.ML Thu Apr 26 12:00:05 2007 +0200 @@ -61,14 +61,6 @@ val set_policy: (string -> bstring -> string) * (string list -> string list list) -> theory -> theory val restore_naming: theory -> theory -> theory - val hide_classes: bool -> xstring list -> theory -> theory - val hide_classes_i: bool -> string list -> theory -> theory - val hide_types: bool -> xstring list -> theory -> theory - val hide_types_i: bool -> string list -> theory -> theory - val hide_consts: bool -> xstring list -> theory -> theory - val hide_consts_i: bool -> string list -> theory -> theory - val hide_names: bool -> string * xstring list -> theory -> theory - val hide_names_i: bool -> string * string list -> theory -> theory end signature SIGN = @@ -186,6 +178,14 @@ val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory include SIGN_THEORY + val hide_classes: bool -> xstring list -> theory -> theory + val hide_classes_i: bool -> string list -> theory -> theory + val hide_types: bool -> xstring list -> theory -> theory + val hide_types_i: bool -> string list -> theory -> theory + val hide_consts: bool -> xstring list -> theory -> theory + val hide_consts_i: bool -> string list -> theory -> theory + val hide_names: bool -> string * xstring list -> theory -> theory + val hide_names_i: bool -> string * string list -> theory -> theory end structure Sign: SIGN =