src/Pure/ML/ml_env.ML

tuned signature;

(*  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;