(* Title: Pure/ML/ml_env.ML
Author: Makarius
Local environment of ML sources and results.
*)
signature ML_ENV =
sig
val inherit: Context.generic -> Context.generic -> Context.generic
val register_tokens: ML_Lex.token list -> Context.generic ->
(serial * ML_Lex.token) list * Context.generic
val token_position: Context.generic -> serial -> Position.T option
val name_space: ML_Name_Space.T
val local_context: use_context
end
structure ML_Env: ML_ENV =
struct
(* context data *)
structure Env = GenericDataFun
(
type T =
Position.T Inttab.table *
(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 =
(Inttab.empty,
(Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
val extend = I;
fun merge _
((toks1, (val1, type1, fixity1, structure1, signature1, functor1)),
(toks2, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
(Inttab.merge (K true) (toks1, toks2),
(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;
(* source tokens *)
fun register_tokens toks context =
let
val regs = map (fn tok => (serial (), tok)) toks;
val context' = context
|> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs));
in (regs, context') end;
val token_position = Inttab.lookup o #1 o Env.get;
(* results *)
val name_space: ML_Name_Space.T =
let
fun lookup sel1 sel2 name =
Context.thread_data ()
|> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (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 (#2 (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 (apsnd (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;