# HG changeset patch # User wenzelm # Date 1459879404 -7200 # Node ID 507c90523113bff25a6a7d30d89e8e0b498e82f4 # Parent 5a0c0649197436b961fe75ed608a818423ef58ac clarified modules -- simplified bootstrap; diff -r 5a0c06491974 -r 507c90523113 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Doc/Implementation/ML.thy Tue Apr 05 20:03:24 2016 +0200 @@ -616,15 +616,15 @@ text %mlref \ \begin{mldecls} - @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\ + @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\ @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\ @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\ @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\ \end{mldecls} - \<^descr> @{ML "ML_Context.the_generic_context ()"} refers to the theory context of + \<^descr> @{ML "Context.the_generic_context ()"} refers to the theory context of the ML toplevel --- at compile time. ML code needs to take care to refer to - @{ML "ML_Context.the_generic_context ()"} correctly. Recall that evaluation + @{ML "Context.the_generic_context ()"} correctly. Recall that evaluation of a function body is delayed until actual run-time. \<^descr> @{ML "Context.>>"}~\f\ applies context transformation \f\ to the implicit diff -r 5a0c06491974 -r 507c90523113 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Apr 05 20:03:24 2016 +0200 @@ -280,7 +280,7 @@ val output_value = the_default "NONE" (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response) val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml - ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))"; + ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))"; val ctxt' = ctxt |> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) |> Context.proof_map (exec false ml_code); diff -r 5a0c06491974 -r 507c90523113 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Tue Apr 05 20:03:24 2016 +0200 @@ -120,7 +120,7 @@ NONE => () | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']); val _ = - Context_Position.report_generic (ML_Context.the_generic_context ()) + Context_Position.report_generic (Context.the_generic_context ()) (command_pos cmd) (command_markup true (name, cmd)); in Data.map (Symtab.update (name, cmd)) thy end; diff -r 5a0c06491974 -r 507c90523113 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/ML/ml_context.ML Tue Apr 05 20:03:24 2016 +0200 @@ -6,9 +6,6 @@ signature ML_CONTEXT = sig - val the_generic_context: unit -> Context.generic - val the_global_context: unit -> theory - val the_local_context: unit -> Proof.context val thm: xstring -> thm val thms: xstring -> thm list val exec: (unit -> unit) -> Context.generic -> Context.generic @@ -35,12 +32,8 @@ (** implicit ML context **) -val the_generic_context = Context.the_thread_data; -val the_global_context = Context.theory_of o the_generic_context; -val the_local_context = Context.proof_of o the_generic_context; - -fun thm name = Proof_Context.get_thm (the_local_context ()) name; -fun thms name = Proof_Context.get_thms (the_local_context ()) name; +fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name; +fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name; fun exec (e: unit -> unit) context = (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of @@ -123,7 +116,7 @@ (ML_Lex.tokenize ("structure " ^ name ^ " =\nstruct\n\ \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^ - " (ML_Context.the_local_context ());\n\ + " (Context.the_local_context ());\n\ \val ML_print_depth =\n\ \ let val default = ML_Options.get_print_depth ()\n\ \ in fn () => ML_Options.get_print_depth_default default end;\n"), @@ -233,7 +226,7 @@ eval ML_Compiler.flags (#1 range) (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @ ML_Lex.read (": " ^ constraint ^ " =") @ ants @ - ML_Lex.read ("in " ^ body ^ " end (ML_Context.the_generic_context ())));"))); + ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));"))); end; diff -r 5a0c06491974 -r 507c90523113 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/ML/ml_env.ML Tue Apr 05 20:03:24 2016 +0200 @@ -130,7 +130,7 @@ let fun lookup sel1 sel2 name = if SML then - Context.the_thread_data () + Context.the_generic_context () |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name) else Context.thread_data () @@ -139,7 +139,7 @@ fun all sel1 sel2 () = (if SML then - Context.the_thread_data () + Context.the_generic_context () |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context)))) else Context.thread_data () diff -r 5a0c06491974 -r 507c90523113 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/ML/ml_thms.ML Tue Apr 05 20:03:24 2016 +0200 @@ -113,7 +113,7 @@ fun merge _ = []; ); -fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ()); +fun get_stored_thms () = Stored_Thms.get (Context.the_global_context ()); val get_stored_thm = hd o get_stored_thms; fun ml_store get (name, ths) = diff -r 5a0c06491974 -r 507c90523113 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue Apr 05 20:03:24 2016 +0200 @@ -260,7 +260,7 @@ val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = Resources.load_thy document symbols last_timing update_time dir header text_pos text - (if name = Context.PureN then [ML_Context.the_global_context ()] else parents); + (if name = Context.PureN then [Context.the_global_context ()] else parents); fun commit () = update_thy deps theory; in Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} diff -r 5a0c06491974 -r 507c90523113 src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/Tools/debugger.ML Tue Apr 05 20:03:24 2016 +0200 @@ -155,7 +155,7 @@ fun eval_context thread_name index SML toks = let - val context = ML_Context.the_generic_context (); + val context = Context.the_generic_context (); val context1 = if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks then context diff -r 5a0c06491974 -r 507c90523113 src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/conjunction.ML Tue Apr 05 20:03:24 2016 +0200 @@ -30,7 +30,7 @@ (** abstract syntax **) -fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t; +fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t; val read_prop = certify o Simple_Syntax.read_prop; val true_prop = certify Logic.true_prop; @@ -76,7 +76,7 @@ val A_B = read_prop "A &&& B"; val conjunction_def = - Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def"; + Thm.unvarify_axiom (Context.the_global_context ()) "Pure.conjunction_def"; fun conjunctionD which = Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP @@ -137,7 +137,7 @@ local -val bootstrap_thy = Context.theory_of (Context.the_thread_data ()); +val bootstrap_thy = Context.the_global_context (); fun conjs n = let diff -r 5a0c06491974 -r 507c90523113 src/Pure/context.ML --- a/src/Pure/context.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/context.ML Tue Apr 05 20:03:24 2016 +0200 @@ -74,9 +74,11 @@ val proof_of: generic -> Proof.context (*total*) (*thread data*) val thread_data: unit -> generic option - val the_thread_data: unit -> generic val set_thread_data: generic option -> unit val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b + val the_generic_context: unit -> generic + val the_global_context: unit -> theory + val the_local_context: unit -> Proof.context val >> : (generic -> generic) -> unit val >>> : (generic -> 'a * generic) -> 'a end; @@ -496,19 +498,22 @@ SOME (SOME context) => SOME context | _ => NONE); -fun the_thread_data () = +fun set_thread_data context = Thread.setLocal (tag, context); +fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context; + +fun the_generic_context () = (case thread_data () of SOME context => context | _ => error "Unknown context"); -fun set_thread_data context = Thread.setLocal (tag, context); -fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context; +val the_global_context = theory_of o the_generic_context; +val the_local_context = proof_of o the_generic_context; end; fun >>> f = let - val (res, context') = f (the_thread_data ()); + val (res, context') = f (the_generic_context ()); val _ = set_thread_data (SOME context'); in res end; diff -r 5a0c06491974 -r 507c90523113 src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/drule.ML Tue Apr 05 20:03:24 2016 +0200 @@ -134,7 +134,7 @@ (*The premises of a theorem, as a cterm list*) val cprems_of = strip_imp_prems o Thm.cprop_of; -fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t; +fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t; val implies = certify Logic.implies; fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B; @@ -570,7 +570,7 @@ local val A = certify (Free ("A", propT)); - val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())); + val axiom = Thm.unvarify_axiom (Context.the_global_context ()); val prop_def = axiom "Pure.prop_def"; val term_def = axiom "Pure.term_def"; val sort_constraint_def = axiom "Pure.sort_constraint_def"; @@ -645,7 +645,7 @@ store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here}))) (Thm.equal_intr (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) - (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI))) + (Thm.unvarify_global (Context.the_global_context ()) sort_constraintI))) (implies_intr_list [A, C] (Thm.assume A))); end; diff -r 5a0c06491974 -r 507c90523113 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/pure_syn.ML Tue Apr 05 20:03:24 2016 +0200 @@ -55,7 +55,7 @@ (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); -val bootstrap_thy = ML_Context.the_global_context (); +val bootstrap_thy = Context.the_global_context (); val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false); diff -r 5a0c06491974 -r 507c90523113 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Pure/raw_simplifier.ML Tue Apr 05 20:03:24 2016 +0200 @@ -1392,11 +1392,10 @@ Variable.gen_all ctxt; val hhf_ss = - simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ())) - addsimps Drule.norm_hhf_eqs); + simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs); val hhf_protect_ss = - simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ())) + simpset_of (empty_simpset (Context.the_local_context ()) addsimps Drule.norm_hhf_eqs |> add_eqcong Drule.protect_cong); in diff -r 5a0c06491974 -r 507c90523113 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Tools/Code/code_runtime.ML Tue Apr 05 20:03:24 2016 +0200 @@ -88,7 +88,7 @@ let val code = (prelude ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml - ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))"); + ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))"); val ctxt' = ctxt |> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) |> Context.proof_map (exec ctxt false code); @@ -539,7 +539,7 @@ ML_Compiler0.use_text notifying_context {line = 0, file = Path.implode filepath, verbose = false, debug = false} (File.read filepath); - val thy'' = Context.the_theory (Context.the_thread_data ()); + val thy'' = Context.the_global_context (); val names = Loaded_Values.get thy''; in (names, thy'') end; diff -r 5a0c06491974 -r 507c90523113 src/Tools/Spec_Check/gen_construction.ML --- a/src/Tools/Spec_Check/gen_construction.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Tools/Spec_Check/gen_construction.ML Tue Apr 05 20:03:24 2016 +0200 @@ -155,7 +155,7 @@ (*produce compilable string*) fun build_check ctxt name (ty, spec) = - "Spec_Check.checkGen (ML_Context.the_local_context ()) (" + "Spec_Check.checkGen (Context.the_local_context ()) (" ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\"" ^ name ^ "\", Property.pred (" ^ spec ^ "));"; diff -r 5a0c06491974 -r 507c90523113 src/Tools/Spec_Check/spec_check.ML --- a/src/Tools/Spec_Check/spec_check.ML Tue Apr 05 19:41:58 2016 +0200 +++ b/src/Tools/Spec_Check/spec_check.ML Tue Apr 05 20:03:24 2016 +0200 @@ -192,5 +192,5 @@ end; -fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s; +fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s;