src/Pure/ML/ml_env.ML

--- /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;
+