# HG changeset patch # User wenzelm # Date 1282906675 -7200 # Node ID abe92b33ac9f656d2b289f1489f2e42aa1438a37 # Parent c421cfe2eadae8c2731cddd33d753fe06f26d007# Parent d8da44a8dd2562fb8587a8dbdbdc6b095c11886a merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML; diff -r c421cfe2eada -r abe92b33ac9f NEWS --- a/NEWS Fri Aug 27 10:57:32 2010 +0200 +++ b/NEWS Fri Aug 27 12:57:55 2010 +0200 @@ -23,6 +23,22 @@ at the cost of clarity of file dependencies. Recall that Isabelle/ML files exclusively use the .ML extension. Minor INCOMPATIBILTY. +* Various options that affect document antiquotations are now properly +handled within the context via configuration options, instead of +unsynchronized references. There are both ML Config.T entities and +Isar declaration attributes to access these. + + ML: Isar: + + Thy_Output.display thy_output_display + Thy_Output.quotes thy_output_quotes + Thy_Output.indent thy_output_indent + Thy_Output.source thy_output_source + Thy_Output.break thy_output_break + +Note that the corresponding "..._default" references may be only +changed globally at the ROOT session setup, but *not* within a theory. + *** Pure *** diff -r c421cfe2eada -r abe92b33ac9f doc-src/IsarRef/Thy/ROOT-HOLCF.ML --- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Fri Aug 27 12:57:55 2010 +0200 @@ -1,4 +1,4 @@ -Unsynchronized.set Thy_Output.source; +Thy_Output.source_default := true; use "../../antiquote_setup.ML"; use_thy "HOLCF_Specific"; diff -r c421cfe2eada -r abe92b33ac9f doc-src/IsarRef/Thy/ROOT-ZF.ML --- a/doc-src/IsarRef/Thy/ROOT-ZF.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML Fri Aug 27 12:57:55 2010 +0200 @@ -1,4 +1,4 @@ -Unsynchronized.set Thy_Output.source; +Thy_Output.source_default := true; use "../../antiquote_setup.ML"; use_thy "ZF_Specific"; diff -r c421cfe2eada -r abe92b33ac9f doc-src/IsarRef/Thy/ROOT.ML --- a/doc-src/IsarRef/Thy/ROOT.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/IsarRef/Thy/ROOT.ML Fri Aug 27 12:57:55 2010 +0200 @@ -1,5 +1,5 @@ -Unsynchronized.set quick_and_dirty; -Unsynchronized.set Thy_Output.source; +quick_and_dirty := true; +Thy_Output.source_default := true; use "../../antiquote_setup.ML"; use_thys [ diff -r c421cfe2eada -r abe92b33ac9f doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/Main/Docs/Main_Doc.thy Fri Aug 27 12:57:55 2010 +0200 @@ -10,9 +10,9 @@ Syntax.pretty_typ ctxt T) val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev) - (fn {source, context, ...} => fn arg => - Thy_Output.output - (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg])); + (fn {source, context = ctxt, ...} => fn arg => + Thy_Output.output ctxt + (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg])); *} (*>*) text{* diff -r c421cfe2eada -r abe92b33ac9f doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/System/Thy/ROOT.ML Fri Aug 27 12:57:55 2010 +0200 @@ -1,4 +1,4 @@ -Unsynchronized.set Thy_Output.source; +Thy_Output.source_default := true; use "../../antiquote_setup.ML"; use_thys ["Basics", "Interfaces", "Presentation", "Misc"]; diff -r c421cfe2eada -r abe92b33ac9f doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/TutorialI/Documents/Documents.thy Fri Aug 27 12:57:55 2010 +0200 @@ -144,7 +144,7 @@ definition xor :: "bool \ bool \ bool" (infixl "\" 60) where "A \ B \ (A \ \ B) \ (\ A \ B)" (*<*) -local +setup {* Sign.local_path *} (*>*) text {* @@ -169,7 +169,7 @@ notation (xsymbols) xor (infixl "\\" 60) (*<*) -local +setup {* Sign.local_path *} (*>*) text {*\noindent diff -r c421cfe2eada -r abe92b33ac9f doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Fri Aug 27 12:57:55 2010 +0200 @@ -168,6 +168,19 @@ \isacommand{definition}\isamarkupfalse% \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% \begin{isamarkuptext}% \noindent The X-Symbol package within Proof~General provides several input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may @@ -200,6 +213,19 @@ \isanewline \isacommand{notation}\isamarkupfalse% \ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% \begin{isamarkuptext}% \noindent The \commdx{notation} command associates a mixfix diff -r c421cfe2eada -r abe92b33ac9f doc-src/TutorialI/Rules/Primes.thy --- a/doc-src/TutorialI/Rules/Primes.thy Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/TutorialI/Rules/Primes.thy Fri Aug 27 12:57:55 2010 +0200 @@ -1,4 +1,3 @@ -(* ID: $Id$ *) (* EXTRACT from HOL/ex/Primes.thy*) (*Euclid's algorithm @@ -10,7 +9,7 @@ ML "Pretty.margin_default := 64" -ML "Thy_Output.indent := 5" (*that is, Doc/TutorialI/settings.ML*) +declare [[thy_output_indent = 5]] (*that is, Doc/TutorialI/settings.ML*) text {*Now in Basic.thy! diff -r c421cfe2eada -r abe92b33ac9f doc-src/TutorialI/Types/Numbers.thy --- a/doc-src/TutorialI/Types/Numbers.thy Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/TutorialI/Types/Numbers.thy Fri Aug 27 12:57:55 2010 +0200 @@ -3,7 +3,7 @@ begin ML "Pretty.margin_default := 64" -ML "Thy_Output.indent := 0" (*we don't want 5 for listing theorems*) +declare [[thy_output_indent = 0]] (*we don't want 5 for listing theorems*) text{* diff -r c421cfe2eada -r abe92b33ac9f doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Fri Aug 27 12:57:55 2010 +0200 @@ -26,16 +26,16 @@ % \isatagML \isacommand{ML}\isamarkupfalse% -\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline -\isacommand{ML}\isamarkupfalse% -\ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}% +\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}% \endisatagML {\isafoldML}% % \isadelimML +\isanewline % \endisadelimML -% +\isacommand{declare}\isamarkupfalse% +\ {\isacharbrackleft}{\isacharbrackleft}thy{\isacharunderscore}output{\isacharunderscore}indent\ {\isacharequal}\ {\isadigit{0}}{\isacharbrackright}{\isacharbrackright}% \begin{isamarkuptext}% numeric literals; default simprules; can re-orient% \end{isamarkuptext}% diff -r c421cfe2eada -r abe92b33ac9f doc-src/TutorialI/settings.ML --- a/doc-src/TutorialI/settings.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/TutorialI/settings.ML Fri Aug 27 12:57:55 2010 +0200 @@ -1,3 +1,1 @@ -(* $Id$ *) - -Thy_Output.indent := 5; +Thy_Output.indent_default := 5; diff -r c421cfe2eada -r abe92b33ac9f doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/antiquote_setup.ML Fri Aug 27 12:57:55 2010 +0200 @@ -71,8 +71,8 @@ in "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^ (txt' - |> (if ! Thy_Output.quotes then quote else I) - |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" + |> (if Config.get ctxt Thy_Output.quotes then quote else I) + |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) end); @@ -93,18 +93,18 @@ (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) (fn {context = ctxt, ...} => map (apfst (Thy_Output.pretty_thm ctxt)) - #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I) - #> (if ! Thy_Output.display + #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I) + #> (if Config.get ctxt Thy_Output.display then map (fn (p, name) => - Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^ - "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}") + Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ + "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") #> space_implode "\\par\\smallskip%\n" #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" else map (fn (p, name) => Output.output (Pretty.str_of p) ^ - "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}") + "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") #> space_implode "\\par\\smallskip%\n" #> enclose "\\isa{" "}")); @@ -112,7 +112,8 @@ (* theory file *) val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name) - (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name])); + (fn {context = ctxt, ...} => + fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])); (* Isabelle/Isar entities (with index) *) @@ -152,8 +153,9 @@ idx ^ (Output.output name |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") - |> (if ! Thy_Output.quotes then quote else I) - |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" + |> (if Config.get ctxt Thy_Output.quotes then quote else I) + |> (if Config.get ctxt Thy_Output.display + then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" else hyper o enclose "\\mbox{\\isa{" "}}")) else error ("Bad " ^ kind ^ " " ^ quote name) end); diff -r c421cfe2eada -r abe92b33ac9f doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/more_antiquote.ML Fri Aug 27 12:57:55 2010 +0200 @@ -95,7 +95,7 @@ |> snd |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |> map (holize o no_vars ctxt o AxClass.overload thy); - in Thy_Output.output (Thy_Output.maybe_pretty_source (pretty_thm ctxt) src thms) end; + in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end; in diff -r c421cfe2eada -r abe92b33ac9f doc-src/rail.ML --- a/doc-src/rail.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/doc-src/rail.ML Fri Aug 27 12:57:55 2010 +0200 @@ -97,8 +97,9 @@ (idx ^ (Output.output name |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") - |> (if ! Thy_Output.quotes then quote else I) - |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" + |> (if Config.get ctxt Thy_Output.quotes then quote else I) + |> (if Config.get ctxt Thy_Output.display + then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" else hyper o enclose "\\mbox{\\isa{" "}}")), style) else ("Bad " ^ kind ^ " " ^ name, false) end; diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Aug 27 12:57:55 2010 +0200 @@ -91,7 +91,7 @@ | _ => (pair ts, K I)) val discharge = fold (Boogie_VCs.discharge o pair vc_name) - fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms)) + fun after_qed [thms] = ProofContext.background_theory (discharge (vcs ~~ thms)) | after_qed _ = I in ProofContext.init_global thy diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Aug 27 12:57:55 2010 +0200 @@ -257,7 +257,9 @@ Pretty.str " =" :: Pretty.brk 1 :: flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos))); - in Thy_Output.output (Thy_Output.maybe_pretty_source (K pretty_datatype) src [()]) end); + in + Thy_Output.output ctxt (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()]) + end); @@ -428,7 +430,7 @@ unflat rules (map Drule.zero_var_indexes_list raw_thms); (*FIXME somehow dubious*) in - ProofContext.theory_result + ProofContext.background_theory_result (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct) #-> after_qed diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Fri Aug 27 12:57:55 2010 +0200 @@ -164,7 +164,7 @@ structure Termination_Simps = Named_Thms ( val name = "termination_simp" - val description = "Simplification rule for termination proofs" + val description = "simplification rules for termination proofs" ) @@ -175,7 +175,7 @@ type T = Proof.context -> tactic val empty = (fn _ => error "Termination prover not configured") val extend = I - fun merge (a, b) = b (* FIXME ? *) + fun merge (a, _) = a ) val set_termination_prover = TerminationProver.put diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Function/measure_functions.ML --- a/src/HOL/Tools/Function/measure_functions.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Function/measure_functions.ML Fri Aug 27 12:57:55 2010 +0200 @@ -20,7 +20,7 @@ ( val name = "measure_function" val description = - "Rules that guide the heuristic generation of measure functions" + "rules that guide the heuristic generation of measure functions" ); fun mk_is_measure t = diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Aug 27 12:57:55 2010 +0200 @@ -68,7 +68,7 @@ type T = multiset_setup option val empty = NONE val extend = I; - fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *) + fun merge (v1, v2) = if is_some v1 then v1 else v2 ) val multiset_setup = Multiset_Setup.put o SOME diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 12:57:55 2010 +0200 @@ -596,13 +596,14 @@ val _ = tracing "Preprocessing specification..." val T = Sign.the_const_type (ProofContext.theory_of ctxt) name val t = Const (name, T) - val ctxt' = ProofContext.theory (Context.copy_thy) ctxt - val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt') - val ctxt'' = ProofContext.init_global thy' + val thy' = + Theory.copy (ProofContext.theory_of ctxt) + |> Predicate_Compile.preprocess preprocess_options t + val ctxt' = ProofContext.init_global thy' val _ = tracing "Generating prolog program..." - val (p, constant_table) = generate (#ensure_groundness options) ctxt'' name + val (p, constant_table) = generate (#ensure_groundness options) ctxt' name |> (if #ensure_groundness options then - add_ground_predicates ctxt'' (#limited_types options) + add_ground_predicates ctxt' (#limited_types options) else I) val _ = tracing "Running prolog program..." val tss = run (#prolog_system options) @@ -622,7 +623,7 @@ mk_set_compr (t :: in_insert) ts xs else let - val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt'' [t]) ("uu", fastype_of t) + val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t) val set_compr = HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"}))) @@ -633,7 +634,7 @@ end in foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr [] - (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt'' constant_table) (ts ~~ Ts))) tss) []) + (map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt' constant_table) (ts ~~ Ts))) tss) []) end fun values_cmd print_modes soln raw_t state = @@ -674,10 +675,9 @@ fun quickcheck ctxt report t size = let - val ctxt' = ProofContext.theory (Context.copy_thy) ctxt - val thy = (ProofContext.theory_of ctxt') + val thy = Theory.copy (ProofContext.theory_of ctxt) val (vs, t') = strip_abs t - val vs' = Variable.variant_frees ctxt' [] vs + val vs' = Variable.variant_frees ctxt [] vs val Ts = map snd vs' val t'' = subst_bounds (map Free (rev vs'), t') val (prems, concl) = strip_horn t'' @@ -693,15 +693,15 @@ val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 val thy3 = Predicate_Compile.preprocess preprocess_options const thy2 - val ctxt'' = ProofContext.init_global thy3 + val ctxt' = ProofContext.init_global thy3 val _ = tracing "Generating prolog program..." - val (p, constant_table) = generate true ctxt'' full_constname - |> add_ground_predicates ctxt'' (#limited_types (!options)) + val (p, constant_table) = generate true ctxt' full_constname + |> add_ground_predicates ctxt' (#limited_types (!options)) val _ = tracing "Running prolog program..." val [ts] = run (#prolog_system (!options)) p (translate_const constant_table full_constname) (map fst vs') (SOME 1) val _ = tracing "Restoring terms..." - val res = SOME (map (restore_term ctxt'' constant_table) (ts ~~ Ts)) + val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts)) val empty_report = ([], false) in (res, empty_report) diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Aug 27 12:57:55 2010 +0200 @@ -176,9 +176,9 @@ val t = Const (const, T) val options = extract_options (((expected_modes, proposed_modes), raw_options), const) in - if (is_inductify options) then + if is_inductify options then let - val lthy' = Local_Theory.theory (preprocess options t) lthy + val lthy' = Local_Theory.background_theory (preprocess options t) lthy val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of SOME c => c diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 27 12:57:55 2010 +0200 @@ -730,9 +730,7 @@ type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table; val empty = Symtab.empty; val extend = I; - val merge = Symtab.merge ((K true) - : ((mode * (compilation_funs -> typ -> term)) list * - (mode * (compilation_funs -> typ -> term)) list -> bool)); + fun merge data : T = Symtab.merge (K true) data; ); fun alternative_compilation_of_global thy pred_name mode = @@ -3033,12 +3031,13 @@ "adding alternative introduction rules for code generation of inductive predicates" (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *) +(* FIXME ... this is important to avoid changing the background theory below *) fun generic_code_pred prep_const options raw_const lthy = let val thy = ProofContext.theory_of lthy val const = prep_const thy raw_const val ctxt = ProofContext.init_global thy - val lthy' = Local_Theory.theory (PredData.map + val lthy' = Local_Theory.background_theory (PredData.map (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy val thy' = ProofContext.theory_of lthy' val ctxt' = ProofContext.init_global thy' @@ -3063,7 +3062,7 @@ val global_thms = ProofContext.export goal_ctxt (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms) in - goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #> + goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #> ((case compilation options of Pred => add_equations | DSeq => add_dseq_equations diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Aug 27 12:57:55 2010 +0200 @@ -21,8 +21,7 @@ structure Fun_Pred = Theory_Data ( type T = (term * term) Item_Net.T; - val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool) - (single o fst); + val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); val extend = I; val merge = Item_Net.merge; ) diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 12:57:55 2010 +0200 @@ -185,10 +185,9 @@ fun compile_term compilation options ctxt t = let - val ctxt' = ProofContext.theory (Context.copy_thy) ctxt - val thy = (ProofContext.theory_of ctxt') + val thy = Theory.copy (ProofContext.theory_of ctxt) val (vs, t') = strip_abs t - val vs' = Variable.variant_frees ctxt' [] vs + val vs' = Variable.variant_frees ctxt [] vs val t'' = subst_bounds (map Free (rev vs'), t') val (prems, concl) = strip_horn t'' val constname = "pred_compile_quickcheck" diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Aug 27 12:57:55 2010 +0200 @@ -18,8 +18,7 @@ structure Specialisations = Theory_Data ( type T = (term * term) Item_Net.T; - val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool) - (single o fst); + val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); val extend = I; val merge = Item_Net.merge; ) diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Aug 27 12:57:55 2010 +0200 @@ -56,10 +56,12 @@ type maps_info = {mapfun: string, relmap: string} structure MapsData = Theory_Data - (type T = maps_info Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data) +( + type T = maps_info Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) fun maps_defined thy s = Symtab.defined (MapsData.get thy) s @@ -70,7 +72,7 @@ | NONE => raise NotFound fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) -fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) +fun maps_update k minfo = ProofContext.background_theory (maps_update_thy k minfo) (* FIXME *) fun maps_attribute_aux s minfo = Thm.declaration_attribute (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) @@ -120,10 +122,12 @@ type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} structure QuotData = Theory_Data - (type T = quotdata_info Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data) +( + type T = quotdata_info Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = {qtyp = Morphism.typ phi qtyp, @@ -174,10 +178,12 @@ for example given "nat fset" we need to find "'a fset"; but overloaded constants share the same name *) structure QConstsData = Theory_Data - (type T = (qconsts_info list) Symtab.table - val empty = Symtab.empty - val extend = I - val merge = Symtab.merge_list qconsts_info_eq) +( + type T = qconsts_info list Symtab.table + val empty = Symtab.empty + val extend = I + val merge = Symtab.merge_list qconsts_info_eq +) fun transform_qconsts phi {qconst, rconst, def} = {qconst = Morphism.term phi qconst, @@ -229,39 +235,49 @@ (* equivalence relation theorems *) structure EquivRules = Named_Thms - (val name = "quot_equiv" - val description = "Equivalence relation theorems.") +( + val name = "quot_equiv" + val description = "equivalence relation theorems" +) val equiv_rules_get = EquivRules.get val equiv_rules_add = EquivRules.add (* respectfulness theorems *) structure RspRules = Named_Thms - (val name = "quot_respect" - val description = "Respectfulness theorems.") +( + val name = "quot_respect" + val description = "respectfulness theorems" +) val rsp_rules_get = RspRules.get val rsp_rules_add = RspRules.add (* preservation theorems *) structure PrsRules = Named_Thms - (val name = "quot_preserve" - val description = "Preservation theorems.") +( + val name = "quot_preserve" + val description = "preservation theorems" +) val prs_rules_get = PrsRules.get val prs_rules_add = PrsRules.add (* id simplification theorems *) structure IdSimps = Named_Thms - (val name = "id_simps" - val description = "Identity simp rules for maps.") +( + val name = "id_simps" + val description = "identity simp rules for maps" +) val id_simps_get = IdSimps.get (* quotient theorems *) structure QuotientRules = Named_Thms - (val name = "quot_thm" - val description = "Quotient theorems.") +( + val name = "quot_thm" + val description = "quotient theorems" +) val quotient_rules_get = QuotientRules.get val quotient_rules_add = QuotientRules.add diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Aug 27 12:57:55 2010 +0200 @@ -77,7 +77,8 @@ Typedef.add_typedef false NONE (qty_name, vs, mx) (typedef_term rel rty lthy) NONE typedef_tac lthy *) - Local_Theory.theory_result +(* FIXME should really use local typedef here *) + Local_Theory.background_theory_result (Typedef.add_typedef_global false NONE (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/choice_specification.ML Fri Aug 27 12:57:55 2010 +0200 @@ -220,8 +220,8 @@ |> process_all (zip3 alt_names rew_imps frees) end - fun after_qed [[thm]] = (ProofContext.theory (fn thy => - #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))))); + fun after_qed [[thm]] = ProofContext.background_theory (fn thy => + #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))); in thy |> ProofContext.init_global diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/int_arith.ML Fri Aug 27 12:57:55 2010 +0200 @@ -91,7 +91,7 @@ fun number_of thy T n = if not (Sign.of_sort thy (T, @{sort number})) then raise CTERM ("number_of", []) - else Numeral.mk_cnumber (Thm.ctyp_of thy T) n + else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; val setup = Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/lin_arith.ML Fri Aug 27 12:57:55 2010 +0200 @@ -16,8 +16,7 @@ val add_simprocs: simproc list -> Context.generic -> Context.generic val add_inj_const: string * typ -> Context.generic -> Context.generic val add_discrete_type: string -> Context.generic -> Context.generic - val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> - Context.generic + val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic val setup: Context.generic -> Context.generic val global_setup: theory -> theory val split_limit: int Config.T @@ -769,29 +768,11 @@ structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data); -fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms, - lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of}; - -fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, - lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of}; - -fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, - lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of}; - -fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, - lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of}; - -fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms)); -fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm])); -fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms)); -fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs)); - -fun set_number_of f = Fast_Arith.map_data (map_number_of (K (serial (), f))) - +val add_inj_thms = Fast_Arith.add_inj_thms; +val add_lessD = Fast_Arith.add_lessD; +val add_simps = Fast_Arith.add_simps; +val add_simprocs = Fast_Arith.add_simprocs; +val set_number_of = Fast_Arith.set_number_of; fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; val lin_arith_tac = Fast_Arith.lin_arith_tac; diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/record.ML Fri Aug 27 12:57:55 2010 +0200 @@ -420,7 +420,7 @@ equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, extfields = extfields, fieldext = fieldext }: data; -structure Records_Data = Theory_Data +structure Data = Theory_Data ( type T = data; val empty = @@ -474,25 +474,22 @@ (* access 'records' *) -val get_info = Symtab.lookup o #records o Records_Data.get; +val get_info = Symtab.lookup o #records o Data.get; fun the_info thy name = (case get_info thy name of SOME info => info | NONE => error ("Unknown record type " ^ quote name)); -fun put_record name info thy = - let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = - Records_Data.get thy; - val data = make_data (Symtab.update (name, info) records) - sel_upd equalities extinjects extsplit splits extfields fieldext; - in Records_Data.put data thy end; +fun put_record name info = + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} => + make_data (Symtab.update (name, info) records) + sel_upd equalities extinjects extsplit splits extfields fieldext); (* access 'sel_upd' *) -val get_sel_upd = #sel_upd o Records_Data.get; +val get_sel_upd = #sel_upd o Data.get; val is_selector = Symtab.defined o #selectors o get_sel_upd; val get_updates = Symtab.lookup o #updates o get_sel_upd; @@ -517,7 +514,7 @@ val upds = map (suffix updateN) all ~~ all; val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong}, - equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy; + equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy; val data = make_data records {selectors = fold Symtab.update_new sels selectors, updates = fold Symtab.update_new upds updates, @@ -526,80 +523,61 @@ foldcong = foldcong addcongs folds, unfoldcong = unfoldcong addcongs unfolds} equalities extinjects extsplit splits extfields fieldext; - in Records_Data.put data thy end; + in Data.put data thy end; (* access 'equalities' *) -fun add_equalities name thm thy = - let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = - Records_Data.get thy; - val data = make_data records sel_upd - (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext; - in Records_Data.put data thy end; - -val get_equalities = Symtab.lookup o #equalities o Records_Data.get; +fun add_equalities name thm = + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} => + make_data records sel_upd + (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext); + +val get_equalities = Symtab.lookup o #equalities o Data.get; (* access 'extinjects' *) -fun add_extinjects thm thy = - let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = - Records_Data.get thy; - val data = - make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) - extsplit splits extfields fieldext; - in Records_Data.put data thy end; - -val get_extinjects = rev o #extinjects o Records_Data.get; +fun add_extinjects thm = + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} => + make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) + extsplit splits extfields fieldext); + +val get_extinjects = rev o #extinjects o Data.get; (* access 'extsplit' *) -fun add_extsplit name thm thy = - let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = - Records_Data.get thy; - val data = - make_data records sel_upd equalities extinjects - (Symtab.update_new (name, thm) extsplit) splits extfields fieldext; - in Records_Data.put data thy end; +fun add_extsplit name thm = + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} => + make_data records sel_upd equalities extinjects + (Symtab.update_new (name, thm) extsplit) splits extfields fieldext); (* access 'splits' *) -fun add_splits name thmP thy = - let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = - Records_Data.get thy; - val data = - make_data records sel_upd equalities extinjects extsplit - (Symtab.update_new (name, thmP) splits) extfields fieldext; - in Records_Data.put data thy end; - -val get_splits = Symtab.lookup o #splits o Records_Data.get; +fun add_splits name thmP = + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} => + make_data records sel_upd equalities extinjects extsplit + (Symtab.update_new (name, thmP) splits) extfields fieldext); + +val get_splits = Symtab.lookup o #splits o Data.get; (* parent/extension of named record *) -val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Records_Data.get); -val get_extension = Option.map #extension oo (Symtab.lookup o #records o Records_Data.get); +val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get); +val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get); (* access 'extfields' *) -fun add_extfields name fields thy = - let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = - Records_Data.get thy; - val data = - make_data records sel_upd equalities extinjects extsplit splits - (Symtab.update_new (name, fields) extfields) fieldext; - in Records_Data.put data thy end; - -val get_extfields = Symtab.lookup o #extfields o Records_Data.get; +fun add_extfields name fields = + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} => + make_data records sel_upd equalities extinjects extsplit splits + (Symtab.update_new (name, fields) extfields) fieldext); + +val get_extfields = Symtab.lookup o #extfields o Data.get; fun get_extT_fields thy T = let @@ -609,7 +587,7 @@ in Long_Name.implode (rev (nm :: rst)) end; val midx = maxidx_of_typs (moreT :: Ts); val varifyT = varifyT midx; - val {records, extfields, ...} = Records_Data.get thy; + val {records, extfields, ...} = Data.get thy; val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name); val args = map varifyT (snd (#extension (the (Symtab.lookup records recname)))); @@ -628,18 +606,14 @@ (* access 'fieldext' *) -fun add_fieldext extname_types fields thy = - let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = - Records_Data.get thy; - val fieldext' = - fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext; - val data = - make_data records sel_upd equalities extinjects - extsplit splits extfields fieldext'; - in Records_Data.put data thy end; - -val get_fieldext = Symtab.lookup o #fieldext o Records_Data.get; +fun add_fieldext extname_types fields = + Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} => + let + val fieldext' = + fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext; + in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end); + +val get_fieldext = Symtab.lookup o #fieldext o Data.get; (* parent records *) @@ -1179,7 +1153,7 @@ ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) => if is_selector thy s andalso is_some (get_updates thy u) then let - val {sel_upd = {updates, ...}, extfields, ...} = Records_Data.get thy; + val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy; fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) = (case Symtab.lookup updates u of @@ -1598,15 +1572,17 @@ [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true) | [x] => (head_of x, false)); - val rule'' = cterm_instantiate (map (pairself cert) - (case rev params of - [] => - (case AList.lookup (op =) (Term.add_frees g []) s of - NONE => sys_error "try_param_tac: no such variable" - | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))]) - | (_, T) :: _ => - [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))), - (x, list_abs (params, Bound 0))])) rule'; + val rule'' = + cterm_instantiate + (map (pairself cert) + (case rev params of + [] => + (case AList.lookup (op =) (Term.add_frees g []) s of + NONE => sys_error "try_param_tac: no such variable" + | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))]) + | (_, T) :: _ => + [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))), + (x, list_abs (params, Bound 0))])) rule'; in compose_tac (false, rule'', nprems_of rule) i end); @@ -1635,7 +1611,8 @@ val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i; val ((_, cons), thy') = thy |> Iso_Tuple_Support.add_iso_tuple_type - (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right); + (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) + (fastype_of left, fastype_of right); in (cons $ left $ right, (thy', i + 1)) end; @@ -1778,7 +1755,10 @@ ("ext_surjective", surject), ("ext_split", split_meta)]); - in (((ext_name, ext_type), (ext_tyco, alphas_zeta), extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end; + in + (((ext_name, ext_type), (ext_tyco, alphas_zeta), + extT, induct', inject', surjective', split_meta', ext_def), thm_thy) + end; fun chunks [] [] = [] | chunks [] xs = [xs] @@ -1795,7 +1775,7 @@ (* mk_recordT *) -(*builds up the record type from the current extension tpye extT and a list +(*build up the record type from the current extension tpye extT and a list of parent extensions, starting with the root of the record hierarchy*) fun mk_recordT extT = fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT; @@ -1834,8 +1814,10 @@ val lhs = HOLogic.mk_random T size; val tc = HOLogic.mk_return Tm @{typ Random.seed} (HOLogic.mk_valtermify_app extN params T); - val rhs = HOLogic.mk_ST - (map (fn (v, T') => ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params) + val rhs = + HOLogic.mk_ST + (map (fn (v, T') => + ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params) tc @{typ Random.seed} (SOME Tm, @{typ Random.seed}); val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); in @@ -1860,17 +1842,20 @@ fun add_code ext_tyco vs extT ext simps inject thy = let - val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) - (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT), - Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT)); - fun tac eq_def = Class.intro_classes_tac [] + val eq = + (HOLogic.mk_Trueprop o HOLogic.mk_eq) + (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT), + Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT)); + fun tac eq_def = + Class.intro_classes_tac [] THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def]) THEN ALLGOALS (rtac @{thm refl}); fun mk_eq thy eq_def = Simplifier.rewrite_rule [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject; - fun mk_eq_refl thy = @{thm HOL.eq_refl} + fun mk_eq_refl thy = + @{thm HOL.eq_refl} |> Thm.instantiate - ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], []) + ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], []) |> AxClass.unoverload thy; in thy @@ -1944,7 +1929,8 @@ val extension_name = full binding; - val ((ext, (ext_tyco, vs), extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) = + val ((ext, (ext_tyco, vs), + extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) = thy |> Sign.qualified_path false binding |> extension_definition extension_name fields alphas_ext zeta moreT more vars; diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/typedef.ML Fri Aug 27 12:57:55 2010 +0200 @@ -186,7 +186,8 @@ ||> Thm.term_of; val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |> - Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A); + Local_Theory.background_theory_result + (primitive_typedef typedef_name newT oldT Rep_name Abs_name A); val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy); val typedef = @@ -246,7 +247,7 @@ in lthy2 |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info)) - |> Local_Theory.theory (Typedef_Interpretation.data full_tname) + |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname) |> pair (full_tname, info) end; diff -r c421cfe2eada -r abe92b33ac9f src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/ex/Numeral.thy Fri Aug 27 12:57:55 2010 +0200 @@ -97,7 +97,7 @@ structure Dig_Simps = Named_Thms ( val name = "numeral" - val description = "Simplification rules for numerals" + val description = "simplification rules for numerals" ) *} diff -r c421cfe2eada -r abe92b33ac9f src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOLCF/Tools/pcpodef.ML Fri Aug 27 12:57:55 2010 +0200 @@ -326,7 +326,7 @@ val args = map (apsnd (prep_constraint ctxt)) raw_args; val (goal1, goal2, make_result) = prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy; - fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2) + fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) | after_qed _ = raise Fail "cpodef_proof"; in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end; @@ -337,7 +337,7 @@ val args = map (apsnd (prep_constraint ctxt)) raw_args; val (goal1, goal2, make_result) = prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy; - fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2) + fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) | after_qed _ = raise Fail "pcpodef_proof"; in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end; diff -r c421cfe2eada -r abe92b33ac9f src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri Aug 27 12:57:55 2010 +0200 @@ -88,13 +88,19 @@ val cut_lin_arith_tac: simpset -> int -> tactic val lin_arith_tac: Proof.context -> bool -> int -> tactic val lin_arith_simproc: simpset -> term -> thm option - val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, - lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, - number_of : serial * (theory -> typ -> int -> cterm)} - -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, - lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, - number_of : serial * (theory -> typ -> int -> cterm)}) - -> Context.generic -> Context.generic + val map_data: + ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, + lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, + number_of: (theory -> typ -> int -> cterm) option} -> + {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, + lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, + number_of: (theory -> typ -> int -> cterm) option}) -> + Context.generic -> Context.generic + val add_inj_thms: thm list -> Context.generic -> Context.generic + val add_lessD: thm -> Context.generic -> Context.generic + val add_simps: thm list -> Context.generic -> Context.generic + val add_simprocs: simproc list -> Context.generic -> Context.generic + val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic val trace: bool Unsynchronized.ref end; @@ -105,8 +111,6 @@ (** theory data **) -fun no_number_of _ _ _ = raise CTERM ("number_of", []) - structure Data = Generic_Data ( type T = @@ -116,32 +120,57 @@ lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, - number_of : serial * (theory -> typ -> int -> cterm)}; + number_of: (theory -> typ -> int -> cterm) option}; - val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], - lessD = [], neqE = [], simpset = Simplifier.empty_ss, - number_of = (serial (), no_number_of) } : T; + val empty : T = + {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], + lessD = [], neqE = [], simpset = Simplifier.empty_ss, + number_of = NONE}; val extend = I; fun merge - ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, - lessD = lessD1, neqE=neqE1, simpset = simpset1, - number_of = (number_of1 as (s1, _))}, - {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, - lessD = lessD2, neqE=neqE2, simpset = simpset2, - number_of = (number_of2 as (s2, _))}) = + ({add_mono_thms = add_mono_thms1, mult_mono_thms = mult_mono_thms1, inj_thms = inj_thms1, + lessD = lessD1, neqE = neqE1, simpset = simpset1, number_of = number_of1}, + {add_mono_thms = add_mono_thms2, mult_mono_thms = mult_mono_thms2, inj_thms = inj_thms2, + lessD = lessD2, neqE = neqE2, simpset = simpset2, number_of = number_of2}) : T = {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2), mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2), inj_thms = Thm.merge_thms (inj_thms1, inj_thms2), lessD = Thm.merge_thms (lessD1, lessD2), neqE = Thm.merge_thms (neqE1, neqE2), simpset = Simplifier.merge_ss (simpset1, simpset2), - (* FIXME depends on accidental load order !?! *) - number_of = if s1 > s2 then number_of1 else number_of2}; + number_of = if is_some number_of1 then number_of1 else number_of2}; ); val map_data = Data.map; val get_data = Data.get o Context.Proof; +fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms, + lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of}; + +fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, + lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of}; + +fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, + lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of}; + +fun add_inj_thms thms = map_data (map_inj_thms (append thms)); +fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [thm])); +fun add_simps thms = map_data (map_simpset (fn simpset => simpset addsimps thms)); +fun add_simprocs procs = map_data (map_simpset (fn simpset => simpset addsimprocs procs)); + +fun set_number_of f = + map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, ...} => + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, + lessD = lessD, neqE = neqE, simpset = simpset, number_of = SOME f}); + +fun number_of ctxt = + (case Data.get (Context.Proof ctxt) of + {number_of = SOME f, ...} => f (ProofContext.theory_of ctxt) + | _ => fn _ => fn _ => raise CTERM ("number_of", [])); + (*** A fast decision procedure ***) @@ -446,8 +475,8 @@ let val ctxt = Simplifier.the_context ss; val thy = ProofContext.theory_of ctxt; - val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, - number_of = (_, num_of), ...} = get_data ctxt; + val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt; + val number_of = number_of ctxt; val simpset' = Simplifier.inherit_context ss simpset; fun only_concl f thm = if Thm.no_prems thm then f (Thm.concl_of thm) else NONE; @@ -493,7 +522,7 @@ val T = #T (Thm.rep_cterm cv) in mth - |> Thm.instantiate ([], [(cv, num_of thy T n)]) + |> Thm.instantiate ([], [(cv, number_of T n)]) |> rewrite_concl |> discharge_prem handle CTERM _ => mult_by_add n thm diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/class.ML Fri Aug 27 12:57:55 2010 +0200 @@ -368,7 +368,7 @@ fun gen_classrel mk_prop classrel thy = let fun after_qed results = - ProofContext.theory ((fold o fold) AxClass.add_classrel results); + ProofContext.background_theory ((fold o fold) AxClass.add_classrel results); in thy |> ProofContext.init_global @@ -482,7 +482,7 @@ val type_name = sanitize_name o Long_Name.base_name; -fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result +fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs)) ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v)) ##> Local_Theory.target synchronize_inst_syntax; @@ -572,7 +572,7 @@ val (tycos, vs, sort) = (#arities o the_instantiation) lthy; val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; fun after_qed' results = - Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) + Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results) #> after_qed; in lthy @@ -608,7 +608,7 @@ val (tycos, vs, sort) = read_multi_arity thy raw_arities; val sorts = map snd vs; val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; - fun after_qed results = ProofContext.theory + fun after_qed results = ProofContext.background_theory ((fold o fold) AxClass.add_arity results); in thy diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/class_declaration.ML Fri Aug 27 12:57:55 2010 +0200 @@ -330,7 +330,7 @@ val some_prop = try the_single props; val some_dep_morph = try the_single (map snd deps); fun after_qed some_wit = - ProofContext.theory (Class.register_subclass (sub, sup) + ProofContext.background_theory (Class.register_subclass (sub, sup) some_dep_morph some_wit export) #> ProofContext.theory_of #> Named_Target.init sub; in do_proof after_qed some_prop goal_ctxt end; diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/expression.ML Fri Aug 27 12:57:55 2010 +0200 @@ -824,8 +824,9 @@ val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; - fun after_qed witss eqns = (ProofContext.theory o Context.theory_map) - (note_eqns_register deps witss attrss eqns export export'); + fun after_qed witss eqns = + (ProofContext.background_theory o Context.theory_map) + (note_eqns_register deps witss attrss eqns export export'); in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end; @@ -872,7 +873,7 @@ val target = intern thy raw_target; val target_ctxt = Named_Target.init target thy; val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt; - fun after_qed witss = ProofContext.theory + fun after_qed witss = ProofContext.background_theory (fold (fn ((dep, morph), wits) => Locale.add_dependency target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss)); in Element.witness_proof after_qed propss goal_ctxt end; diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/generic_target.ML Fri Aug 27 12:57:55 2010 +0200 @@ -195,16 +195,16 @@ (Morphism.transform (Local_Theory.global_morphism lthy) decl); in lthy - |> Local_Theory.theory (Context.theory_map global_decl) + |> Local_Theory.background_theory (Context.theory_map global_decl) |> Local_Theory.target (Context.proof_map global_decl) end; fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = let - val (const, lthy2) = lthy |> Local_Theory.theory_result + val (const, lthy2) = lthy |> Local_Theory.background_theory_result (Sign.declare_const ((b, U), mx)); val lhs = list_comb (const, type_params @ term_params); - val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result + val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs))); in ((lhs, def), lthy3) end; @@ -214,12 +214,13 @@ val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts; in lthy - |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd) + |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd) |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd) end; -fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory - (Sign.add_abbrev (#1 prmode) (b, t) #-> - (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)])); +fun theory_abbrev prmode ((b, mx), t) = + Local_Theory.background_theory + (Sign.add_abbrev (#1 prmode) (b, t) #-> + (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)])); end; diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/local_theory.ML Fri Aug 27 12:57:55 2010 +0200 @@ -21,8 +21,8 @@ val target_of: local_theory -> Proof.context val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val raw_theory: (theory -> theory) -> local_theory -> local_theory - val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory - val theory: (theory -> theory) -> local_theory -> local_theory + val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory + val background_theory: (theory -> theory) -> local_theory -> local_theory val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory val target: (Proof.context -> Proof.context) -> local_theory -> local_theory val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory @@ -144,7 +144,7 @@ val checkpoint = raw_theory Theory.checkpoint; -fun theory_result f lthy = +fun background_theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |> Sign.map_naming (K (naming_of lthy)) @@ -152,7 +152,7 @@ ||> Sign.restore_naming thy ||> Theory.checkpoint); -fun theory f = #2 o theory_result (f #> pair ()); +fun background_theory f = #2 o background_theory_result (f #> pair ()); fun target_result f lthy = let @@ -169,7 +169,7 @@ fun target f = #2 o target_result (f #> pair ()); fun map_contexts f = - theory (Context.theory_map f) #> + background_theory (Context.theory_map f) #> target (Context.proof_map f) #> Context.proof_map f; @@ -261,7 +261,7 @@ (* exit *) -val exit = ProofContext.theory Theory.checkpoint o operation #exit; +val exit = ProofContext.background_theory Theory.checkpoint o operation #exit; val exit_global = ProofContext.theory_of o exit; fun exit_result f (x, lthy) = diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/locale.ML Fri Aug 27 12:57:55 2010 +0200 @@ -497,8 +497,8 @@ fun add_thmss loc kind args ctxt = let val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt; - val ctxt'' = ctxt' |> ProofContext.theory ( - (change_locale loc o apfst o apsnd) (cons (args', serial ())) + val ctxt'' = ctxt' |> ProofContext.background_theory + ((change_locale loc o apfst o apsnd) (cons (args', serial ())) #> (* Registrations *) (fn thy => fold_rev (fn (_, morph) => @@ -519,7 +519,7 @@ [([Drule.dummy_thm], [])])]; fun add_syntax_declaration loc decl = - ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ()))) + ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ()))) #> add_declaration loc decl; diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/named_target.ML Fri Aug 27 12:57:55 2010 +0200 @@ -118,7 +118,7 @@ (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts; in lthy - |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd) + |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd) |> Local_Theory.target (Locale.add_thmss locale kind local_facts') end @@ -129,19 +129,21 @@ (* abbrev *) -fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result - (Sign.add_abbrev Print_Mode.internal (b, t)) #-> - (fn (lhs, _) => locale_const_declaration ta prmode - ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); +fun locale_abbrev ta prmode ((b, mx), t) xs = + Local_Theory.background_theory_result + (Sign.add_abbrev Print_Mode.internal (b, t)) #-> + (fn (lhs, _) => locale_const_declaration ta prmode + ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (global_rhs, t') xs lthy = - if is_locale - then lthy - |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs - |> is_class ? Class.abbrev target prmode ((b, mx), t') - else lthy - |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); + if is_locale then + lthy + |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs + |> is_class ? Class.abbrev target prmode ((b, mx), t') + else + lthy + |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); (* pretty *) @@ -200,9 +202,10 @@ fun init target thy = init_target (named_target thy target) thy; -fun reinit lthy = case peek lthy - of SOME {target, ...} => init target o Local_Theory.exit_global - | NONE => error "Not in a named target"; +fun reinit lthy = + (case peek lthy of + SOME {target, ...} => init target o Local_Theory.exit_global + | NONE => error "Not in a named target"); val theory_init = init_target global_target; diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/overloading.ML Fri Aug 27 12:57:55 2010 +0200 @@ -140,7 +140,7 @@ end fun define_overloaded (c, U) (v, checked) (b_def, rhs) = - Local_Theory.theory_result + Local_Theory.background_theory_result (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) ##> Local_Theory.target synchronize_syntax diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Aug 27 12:57:55 2010 +0200 @@ -38,8 +38,8 @@ val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list val transfer_syntax: theory -> Proof.context -> Proof.context val transfer: theory -> Proof.context -> Proof.context - val theory: (theory -> theory) -> Proof.context -> Proof.context - val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context + val background_theory: (theory -> theory) -> Proof.context -> Proof.context + val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context val extern_fact: Proof.context -> string -> xstring val pretty_term_abbrev: Proof.context -> term -> Pretty.T val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T @@ -283,9 +283,9 @@ fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; -fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt; +fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; -fun theory_result f ctxt = +fun background_theory_result f ctxt = let val (res, thy') = f (theory_of ctxt) in (res, ctxt |> transfer thy') end; diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Isar/typedecl.ML Fri Aug 27 12:57:55 2010 +0200 @@ -34,7 +34,7 @@ fun basic_decl decl (b, n, mx) lthy = let val name = Local_Theory.full_name lthy b in lthy - |> Local_Theory.theory (decl name) + |> Local_Theory.background_theory (decl name) |> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)] |> Local_Theory.type_alias b name |> pair name diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Fri Aug 27 12:57:55 2010 +0200 @@ -204,7 +204,7 @@ realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2), defs = Library.merge Thm.eq_thm (defs1, defs2), expand = Library.merge (op =) (expand1, expand2), - prep = (case prep1 of NONE => prep2 | _ => prep1)}; + prep = if is_some prep1 then prep1 else prep2}; ); fun read_condeq thy = diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Thy/thy_load.ML Fri Aug 27 12:57:55 2010 +0200 @@ -195,7 +195,7 @@ val _ = Context.>> Local_Theory.propagate_ml_env; val provide = provide (src_path, (path, id)); - val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide)); + val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide)); in () end; fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path); diff -r c421cfe2eada -r abe92b33ac9f src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Pure/Thy/thy_output.ML Fri Aug 27 12:57:55 2010 +0200 @@ -6,31 +6,37 @@ signature THY_OUTPUT = sig - val display: bool Unsynchronized.ref - val quotes: bool Unsynchronized.ref - val indent: int Unsynchronized.ref - val source: bool Unsynchronized.ref - val break: bool Unsynchronized.ref - val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit - val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit + val display_default: bool Unsynchronized.ref + val quotes_default: bool Unsynchronized.ref + val indent_default: int Unsynchronized.ref + val source_default: bool Unsynchronized.ref + val break_default: bool Unsynchronized.ref + val display: bool Config.T + val quotes: bool Config.T + val indent: int Config.T + val source: bool Config.T + val break: bool Config.T + val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context + val add_option: string -> (string -> Proof.context -> Proof.context) -> unit val defined_command: string -> bool val defined_option: string -> bool val print_antiquotations: unit -> unit val boolean: string -> bool val integer: string -> int val antiquotation: string -> 'a context_parser -> - ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit + ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit datatype markup = Markup | MarkupEnv | Verbatim val modes: string list Unsynchronized.ref val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) -> (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T - val pretty_text: string -> Pretty.T + val pretty_text: Proof.context -> string -> Pretty.T val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val str_of_source: Args.src -> string - val maybe_pretty_source: ('a -> Pretty.T) -> Args.src -> 'a list -> Pretty.T list - val output: Pretty.T list -> string + val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context -> + Args.src -> 'a list -> Pretty.T list + val output: Proof.context -> Pretty.T list -> string end; structure Thy_Output: THY_OUTPUT = @@ -38,11 +44,31 @@ (** global options **) -val display = Unsynchronized.ref false; -val quotes = Unsynchronized.ref false; -val indent = Unsynchronized.ref 0; -val source = Unsynchronized.ref false; -val break = Unsynchronized.ref false; +val display_default = Unsynchronized.ref false; +val quotes_default = Unsynchronized.ref false; +val indent_default = Unsynchronized.ref 0; +val source_default = Unsynchronized.ref false; +val break_default = Unsynchronized.ref false; + +val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default); +val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default); +val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default); +val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default); +val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default); + +val _ = Context.>> (Context.map_theory + (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break)); + + +structure Wrappers = Proof_Data +( + type T = ((unit -> string) -> unit -> string) list; + fun init _ = []; +); + +fun add_wrapper wrapper = Wrappers.map (cons wrapper); + +val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f); @@ -51,22 +77,23 @@ local val global_commands = - Unsynchronized.ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table); + Unsynchronized.ref + (Symtab.empty: (Args.src -> Toplevel.state -> Proof.context -> string) Symtab.table); val global_options = - Unsynchronized.ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table); + Unsynchronized.ref (Symtab.empty: (string -> Proof.context -> Proof.context) Symtab.table); -fun add_item kind (name, x) tab = +fun add_item kind name item tab = (if not (Symtab.defined tab name) then () else warning ("Redefined document antiquotation " ^ kind ^ ": " ^ quote name); - Symtab.update (name, x) tab); + Symtab.update (name, item) tab); in -fun add_commands xs = - CRITICAL (fn () => Unsynchronized.change global_commands (fold (add_item "command") xs)); -fun add_options xs = - CRITICAL (fn () => Unsynchronized.change global_options (fold (add_item "option") xs)); +fun add_command name cmd = + CRITICAL (fn () => Unsynchronized.change global_commands (add_item "command" name cmd)); +fun add_option name opt = + CRITICAL (fn () => Unsynchronized.change global_options (add_item "option" name opt)); fun defined_command name = Symtab.defined (! global_commands) name; fun defined_option name = Symtab.defined (! global_options) name; @@ -77,18 +104,15 @@ NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos) | SOME f => (Position.report (Markup.doc_antiq name) pos; - (fn state => f src state handle ERROR msg => + (fn state => fn ctxt => f src state ctxt handle ERROR msg => cat_error msg ("The error(s) above occurred in document antiquotation: " ^ quote name ^ Position.str_of pos)))) end; -fun option (name, s) f () = +fun option (name, s) ctxt = (case Symtab.lookup (! global_options) name of NONE => error ("Unknown document antiquotation option: " ^ quote name) - | SOME opt => opt s f ()); - -fun options [] f = f - | options (opt :: opts) f = option opt (options opts f); + | SOME opt => opt s ctxt); fun print_antiquotations () = @@ -100,10 +124,11 @@ end; -fun antiquotation name scan out = add_commands [(name, fn src => fn state => - let val (x, ctxt) = Args.context_syntax "document antiquotation" - scan src (Toplevel.presentation_context_of state) - in out {source = src, state = state, context = ctxt} x end)]; +fun antiquotation name scan out = + add_command name + (fn src => fn state => fn ctxt => + let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt + in out {source = src, state = state, context = ctxt'} x end); @@ -151,10 +176,13 @@ let fun expand (Antiquote.Text ss) = Symbol_Pos.content ss | expand (Antiquote.Antiq (ss, (pos, _))) = - let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in - options opts (fn () => command src state) (); (*preview errors!*) - Print_Mode.with_modes (! modes @ Latex.modes) - (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) () + let + val (opts, src) = Token.read_antiq lex antiq (ss, pos); + val opts_ctxt = fold option opts (Toplevel.presentation_context_of state); + val cmd = wrap opts_ctxt (fn () => command src state opts_ctxt); + val _ = cmd (); (*preview errors!*) + in + Print_Mode.with_modes (! modes @ Latex.modes) (Output.no_warnings_CRITICAL cmd) () end | expand (Antiquote.Open _) = "" | expand (Antiquote.Close _) = ""; @@ -417,31 +445,31 @@ (* options *) -val _ = add_options - [("show_types", setmp_CRITICAL Syntax.show_types o boolean), - ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean), - ("show_structs", setmp_CRITICAL show_structs o boolean), - ("show_question_marks", setmp_CRITICAL show_question_marks o boolean), - ("long_names", setmp_CRITICAL Name_Space.long_names o boolean), - ("short_names", setmp_CRITICAL Name_Space.short_names o boolean), - ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean), - ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean), - ("display", setmp_CRITICAL display o boolean), - ("break", setmp_CRITICAL break o boolean), - ("quotes", setmp_CRITICAL quotes o boolean), - ("mode", fn s => fn f => Print_Mode.with_modes [s] f), - ("margin", setmp_CRITICAL Pretty.margin_default o integer), - ("indent", setmp_CRITICAL indent o integer), - ("source", setmp_CRITICAL source o boolean), - ("goals_limit", setmp_CRITICAL goals_limit o integer)]; +val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean); +val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean); +val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean); +val _ = add_option "show_question_marks" (add_wrapper o setmp_CRITICAL show_question_marks o boolean); +val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean); +val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean); +val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean); +val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean); +val _ = add_option "display" (Config.put display o boolean); +val _ = add_option "break" (Config.put break o boolean); +val _ = add_option "quotes" (Config.put quotes o boolean); +val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single); +val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer); +val _ = add_option "indent" (Config.put indent o integer); +val _ = add_option "source" (Config.put source o boolean); +val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer); (* basic pretty printing *) -fun tweak_line s = - if ! display then s else Symbol.strip_blanks s; +fun tweak_line ctxt s = + if Config.get ctxt display then s else Symbol.strip_blanks s; -val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; +fun pretty_text ctxt = + Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o Library.split_lines; fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; @@ -490,19 +518,19 @@ val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src; -fun maybe_pretty_source pretty src xs = - map pretty xs (*always pretty in order to exhibit errors!*) - |> (if ! source then K [pretty_text (str_of_source src)] else I); +fun maybe_pretty_source pretty ctxt src xs = + map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) + |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I); -fun output prts = +fun output ctxt prts = prts - |> (if ! quotes then map Pretty.quote else I) - |> (if ! display then - map (Output.output o Pretty.string_of o Pretty.indent (! indent)) + |> (if Config.get ctxt quotes then map Pretty.quote else I) + |> (if Config.get ctxt display then + map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent)) #> space_implode "\\isasep\\isanewline%\n" #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" else - map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of)) + map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of)) #> space_implode "\\isasep\\isanewline%\n" #> enclose "\\isa{" "}"); @@ -515,11 +543,12 @@ local fun basic_entities name scan pretty = antiquotation name scan - (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source); + (fn {source, context, ...} => output context o maybe_pretty_source pretty context source); fun basic_entities_style name scan pretty = antiquotation name scan (fn {source, context, ...} => fn (style, xs) => - output (maybe_pretty_source (fn x => pretty context (style, x)) source xs)); + output context + (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs)); fun basic_entity name scan = basic_entities name (scan >> single); @@ -533,7 +562,7 @@ val _ = basic_entity "const" (Args.const_proper false) pretty_const; val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev; val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ; -val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text); +val _ = basic_entity "text" (Scan.lift Args.name) pretty_text; val _ = basic_entities "prf" Attrib.thms (pretty_prf false); val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true); val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory; @@ -554,7 +583,7 @@ | _ => error "No proof state"); fun goal_state name main_goal = antiquotation name (Scan.succeed ()) - (fn {state, ...} => fn () => output + (fn {state, context, ...} => fn () => output context [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]); in @@ -578,7 +607,7 @@ val _ = context |> Proof.theorem NONE (K I) [[(prop, [])]] |> Proof.global_terminal_proof methods; - in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end); + in output context (maybe_pretty_source pretty_term context prop_src [prop]) end); (* ML text *) @@ -589,8 +618,8 @@ (fn {context, ...} => fn (txt, pos) => (ML_Context.eval_in (SOME context) false pos (ml pos txt); Symbol_Pos.content (Symbol_Pos.explode (txt, pos)) - |> (if ! quotes then quote else I) - |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" + |> (if Config.get context quotes then quote else I) + |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" else split_lines #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") diff -r c421cfe2eada -r abe92b33ac9f src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Tools/Code/code_simp.ML Fri Aug 27 12:57:55 2010 +0200 @@ -37,7 +37,8 @@ (* dedicated simpset *) -structure Simpset = Theory_Data ( +structure Simpset = Theory_Data +( type T = simpset; val empty = empty_ss; fun extend ss = MetaSimplifier.inherit_context empty_ss ss; diff -r c421cfe2eada -r abe92b33ac9f src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/Tools/quickcheck.ML Fri Aug 27 12:57:55 2010 +0200 @@ -78,27 +78,32 @@ datatype test_params = Test_Params of { size: int, iterations: int, default_type: typ list, no_assms: bool, - expect : expectation, report: bool, quiet : bool}; + expect : expectation, report: bool, quiet : bool}; fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))); + fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) = Test_Params { size = size, iterations = iterations, default_type = default_type, - no_assms = no_assms, expect = expect, report = report, quiet = quiet }; + no_assms = no_assms, expect = expect, report = report, quiet = quiet }; + fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet)))); -fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1, - no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 }, + +fun merge_test_params + (Test_Params { size = size1, iterations = iterations1, default_type = default_type1, + no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 }, Test_Params { size = size2, iterations = iterations2, default_type = default_type2, - no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) = + no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) = make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2), ((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2))); structure Data = Theory_Data ( - type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list - * test_params; + type T = + (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list + * test_params; val empty = ([], Test_Params { size = 10, iterations = 100, default_type = [], no_assms = false, expect = No_Expectation, report = false, quiet = false});