--- a/src/Pure/IsaMakefile Mon Jun 01 15:25:59 2009 +0200
+++ b/src/Pure/IsaMakefile Mon Jun 01 15:26:00 2009 +0200
@@ -55,19 +55,19 @@
General/table.ML General/url.ML General/xml.ML General/yxml.ML \
Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
- Isar/constdefs.ML Isar/context_rules.ML \
- Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \
- Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \
- Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
- Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
- Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
- Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
- Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
- Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \
- Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
- Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
- ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
+ Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
+ Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
+ Isar/local_theory.ML Isar/locale.ML Isar/method.ML \
+ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
+ Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
+ Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
+ Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
+ Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \
+ Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
+ Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_context.ML ML/ml_env.ML \
+ ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_test.ML \
+ ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
ML-Systems/install_pp_polyml-experimental.ML \
ML-Systems/use_context.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
--- a/src/Pure/ML/ml_context.ML Mon Jun 01 15:25:59 2009 +0200
+++ b/src/Pure/ML/ml_context.ML Mon Jun 01 15:26:00 2009 +0200
@@ -19,9 +19,6 @@
val the_global_context: unit -> theory
val the_local_context: unit -> Proof.context
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val inherit_env: Context.generic -> Context.generic -> Context.generic
- val name_space: ML_Name_Space.T
- val local_context: use_context
val stored_thms: thm list ref
val ml_store_thm: string * thm -> unit
val ml_store_thms: string * thm list -> unit
@@ -54,78 +51,6 @@
| NONE => error "Missing context after execution");
-(* ML name space *)
-
-structure ML_Env = GenericDataFun
-(
- type T =
- ML_Name_Space.valueVal Symtab.table *
- ML_Name_Space.typeVal Symtab.table *
- ML_Name_Space.fixityVal Symtab.table *
- ML_Name_Space.structureVal Symtab.table *
- ML_Name_Space.signatureVal Symtab.table *
- ML_Name_Space.functorVal Symtab.table;
- val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
- val extend = I;
- fun merge _
- ((val1, type1, fixity1, structure1, signature1, functor1),
- (val2, type2, fixity2, structure2, signature2, functor2)) : T =
- (Symtab.merge (K true) (val1, val2),
- Symtab.merge (K true) (type1, type2),
- Symtab.merge (K true) (fixity1, fixity2),
- Symtab.merge (K true) (structure1, structure2),
- Symtab.merge (K true) (signature1, signature2),
- Symtab.merge (K true) (functor1, functor2));
-);
-
-val inherit_env = ML_Env.put o ML_Env.get;
-
-val name_space: ML_Name_Space.T =
- let
- fun lookup sel1 sel2 name =
- Context.thread_data ()
- |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name)
- |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
-
- fun all sel1 sel2 () =
- Context.thread_data ()
- |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context)))
- |> append (sel2 ML_Name_Space.global ())
- |> sort_distinct (string_ord o pairself #1);
-
- fun enter ap1 sel2 entry =
- if is_some (Context.thread_data ()) then
- Context.>> (ML_Env.map (ap1 (Symtab.update entry)))
- else sel2 ML_Name_Space.global entry;
- in
- {lookupVal = lookup #1 #lookupVal,
- lookupType = lookup #2 #lookupType,
- lookupFix = lookup #3 #lookupFix,
- lookupStruct = lookup #4 #lookupStruct,
- lookupSig = lookup #5 #lookupSig,
- lookupFunct = lookup #6 #lookupFunct,
- enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
- enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
- enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
- enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
- enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
- enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
- allVal = all #1 #allVal,
- allType = all #2 #allType,
- allFix = all #3 #allFix,
- allStruct = all #4 #allStruct,
- allSig = all #5 #allSig,
- allFunct = all #6 #allFunct}
- end;
-
-val local_context: use_context =
- {tune_source = ML_Parse.fix_ints,
- name_space = name_space,
- str_of_pos = Position.str_of oo Position.line_file,
- print = writeln,
- error = error};
-
-
(* theorem bindings *)
val stored_thms: thm list ref = ref [];
@@ -139,7 +64,7 @@
else if not (ML_Syntax.is_identifier name) then
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
else setmp stored_thms ths' (fn () =>
- use_text local_context (0, "") true
+ use_text ML_Env.local_context (0, "") true
("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
in () end;
@@ -240,7 +165,7 @@
fun eval verbose pos txt =
let
- fun eval_raw p = use_text local_context
+ fun eval_raw p = use_text ML_Env.local_context
(the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p));
(*prepare source text*)
@@ -253,7 +178,7 @@
(*prepare static ML environment*)
val _ = Context.setmp_thread_data env_ctxt
(fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
- |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
+ |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
(*eval ML*)
val _ = eval_raw pos verbose body;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_env.ML Mon Jun 01 15:26:00 2009 +0200
@@ -0,0 +1,87 @@
+(* Title: Pure/ML/ml_env.ML
+ Author: Makarius
+
+Local environment of ML results.
+*)
+
+signature ML_ENV =
+sig
+ val inherit: Context.generic -> Context.generic -> Context.generic
+ val name_space: ML_Name_Space.T
+ val local_context: use_context
+end
+
+structure ML_Env: ML_ENV =
+struct
+
+structure Env = GenericDataFun
+(
+ type T =
+ ML_Name_Space.valueVal Symtab.table *
+ ML_Name_Space.typeVal Symtab.table *
+ ML_Name_Space.fixityVal Symtab.table *
+ ML_Name_Space.structureVal Symtab.table *
+ ML_Name_Space.signatureVal Symtab.table *
+ ML_Name_Space.functorVal Symtab.table;
+ val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
+ val extend = I;
+ fun merge _
+ ((val1, type1, fixity1, structure1, signature1, functor1),
+ (val2, type2, fixity2, structure2, signature2, functor2)) : T =
+ (Symtab.merge (K true) (val1, val2),
+ Symtab.merge (K true) (type1, type2),
+ Symtab.merge (K true) (fixity1, fixity2),
+ Symtab.merge (K true) (structure1, structure2),
+ Symtab.merge (K true) (signature1, signature2),
+ Symtab.merge (K true) (functor1, functor2));
+);
+
+val inherit = Env.put o Env.get;
+
+val name_space: ML_Name_Space.T =
+ let
+ fun lookup sel1 sel2 name =
+ Context.thread_data ()
+ |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name)
+ |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
+
+ fun all sel1 sel2 () =
+ Context.thread_data ()
+ |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (Env.get context)))
+ |> append (sel2 ML_Name_Space.global ())
+ |> sort_distinct (string_ord o pairself #1);
+
+ fun enter ap1 sel2 entry =
+ if is_some (Context.thread_data ()) then
+ Context.>> (Env.map (ap1 (Symtab.update entry)))
+ else sel2 ML_Name_Space.global entry;
+ in
+ {lookupVal = lookup #1 #lookupVal,
+ lookupType = lookup #2 #lookupType,
+ lookupFix = lookup #3 #lookupFix,
+ lookupStruct = lookup #4 #lookupStruct,
+ lookupSig = lookup #5 #lookupSig,
+ lookupFunct = lookup #6 #lookupFunct,
+ enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
+ enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
+ enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
+ enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
+ enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
+ enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
+ allVal = all #1 #allVal,
+ allType = all #2 #allType,
+ allFix = all #3 #allFix,
+ allStruct = all #4 #allStruct,
+ allSig = all #5 #allSig,
+ allFunct = all #6 #allFunct}
+ end;
+
+val local_context: use_context =
+ {tune_source = ML_Parse.fix_ints,
+ name_space = name_space,
+ str_of_pos = Position.str_of oo Position.line_file,
+ print = writeln,
+ error = error};
+
+end;
+