src/Pure/ML/ml_env.ML
changeset 56275 600f432ab556
parent 56203 76c72f4d0667
child 56618 874bdedb2313
     1.1 --- a/src/Pure/ML/ml_env.ML	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_env.ML	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -1,12 +1,14 @@
     1.4  (*  Title:      Pure/ML/ml_env.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Local environment of ML results.
     1.8 +Toplevel environment for Standard ML and Isabelle/ML within the
     1.9 +implicit context.
    1.10  *)
    1.11  
    1.12  signature ML_ENV =
    1.13  sig
    1.14    val inherit: Context.generic -> Context.generic -> Context.generic
    1.15 +  val SML_name_space: ML_Name_Space.T
    1.16    val name_space: ML_Name_Space.T
    1.17    val local_context: use_context
    1.18    val check_functor: string -> unit
    1.19 @@ -17,56 +19,112 @@
    1.20  
    1.21  (* context data *)
    1.22  
    1.23 +type tables =
    1.24 +  ML_Name_Space.valueVal Symtab.table *
    1.25 +  ML_Name_Space.typeVal Symtab.table *
    1.26 +  ML_Name_Space.fixityVal Symtab.table *
    1.27 +  ML_Name_Space.structureVal Symtab.table *
    1.28 +  ML_Name_Space.signatureVal Symtab.table *
    1.29 +  ML_Name_Space.functorVal Symtab.table;
    1.30 +
    1.31 +fun merge_tables
    1.32 +  ((val1, type1, fixity1, structure1, signature1, functor1),
    1.33 +   (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
    1.34 +  (Symtab.merge (K true) (val1, val2),
    1.35 +   Symtab.merge (K true) (type1, type2),
    1.36 +   Symtab.merge (K true) (fixity1, fixity2),
    1.37 +   Symtab.merge (K true) (structure1, structure2),
    1.38 +   Symtab.merge (K true) (signature1, signature2),
    1.39 +   Symtab.merge (K true) (functor1, functor2));
    1.40 +
    1.41 +type data = {bootstrap: bool, tables: tables, sml_tables: tables};
    1.42 +
    1.43 +fun make_data (bootstrap, tables, sml_tables) : data =
    1.44 +  {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables};
    1.45 +
    1.46  structure Env = Generic_Data
    1.47  (
    1.48 -  type T =
    1.49 -    bool * (*global bootstrap environment*)
    1.50 -     (ML_Name_Space.valueVal Symtab.table *
    1.51 -      ML_Name_Space.typeVal Symtab.table *
    1.52 -      ML_Name_Space.fixityVal Symtab.table *
    1.53 -      ML_Name_Space.structureVal Symtab.table *
    1.54 -      ML_Name_Space.signatureVal Symtab.table *
    1.55 -      ML_Name_Space.functorVal Symtab.table);
    1.56 -  val empty : T =
    1.57 -    (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
    1.58 -  fun extend (_, tabs) : T = (false, tabs);
    1.59 -  fun merge
    1.60 -   ((_, (val1, type1, fixity1, structure1, signature1, functor1)),
    1.61 -    (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
    1.62 -    (false,
    1.63 -     (Symtab.merge (K true) (val1, val2),
    1.64 -      Symtab.merge (K true) (type1, type2),
    1.65 -      Symtab.merge (K true) (fixity1, fixity2),
    1.66 -      Symtab.merge (K true) (structure1, structure2),
    1.67 -      Symtab.merge (K true) (signature1, signature2),
    1.68 -      Symtab.merge (K true) (functor1, functor2)));
    1.69 +  type T = data
    1.70 +  val empty =
    1.71 +    make_data (true,
    1.72 +      (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
    1.73 +      (Symtab.make ML_Name_Space.initial_val,
    1.74 +       Symtab.make ML_Name_Space.initial_type,
    1.75 +       Symtab.make ML_Name_Space.initial_fixity,
    1.76 +       Symtab.make ML_Name_Space.initial_structure,
    1.77 +       Symtab.make ML_Name_Space.initial_signature,
    1.78 +       Symtab.make ML_Name_Space.initial_functor));
    1.79 +  fun extend (data : T) = make_data (false, #tables data, #sml_tables data);
    1.80 +  fun merge (data : T * T) =
    1.81 +    make_data (false,
    1.82 +      merge_tables (pairself #tables data),
    1.83 +      merge_tables (pairself #sml_tables data));
    1.84  );
    1.85  
    1.86  val inherit = Env.put o Env.get;
    1.87  
    1.88  
    1.89 -(* results *)
    1.90 +(* SML name space *)
    1.91 +
    1.92 +val SML_name_space: ML_Name_Space.T =
    1.93 +  let
    1.94 +    fun lookup which name =
    1.95 +      Context.the_thread_data ()
    1.96 +      |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
    1.97 +
    1.98 +    fun all which () =
    1.99 +      Context.the_thread_data ()
   1.100 +      |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
   1.101 +      |> sort_distinct (string_ord o pairself #1);
   1.102 +
   1.103 +    fun enter which entry =
   1.104 +      Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
   1.105 +        let val sml_tables' = which (Symtab.update entry) sml_tables
   1.106 +        in make_data (bootstrap, tables, sml_tables') end));
   1.107 +  in
   1.108 +   {lookupVal    = lookup #1,
   1.109 +    lookupType   = lookup #2,
   1.110 +    lookupFix    = lookup #3,
   1.111 +    lookupStruct = lookup #4,
   1.112 +    lookupSig    = lookup #5,
   1.113 +    lookupFunct  = lookup #6,
   1.114 +    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
   1.115 +    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
   1.116 +    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
   1.117 +    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
   1.118 +    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
   1.119 +    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
   1.120 +    allVal       = all #1,
   1.121 +    allType      = all #2,
   1.122 +    allFix       = all #3,
   1.123 +    allStruct    = all #4,
   1.124 +    allSig       = all #5,
   1.125 +    allFunct     = all #6}
   1.126 +  end;
   1.127 +
   1.128 +
   1.129 +(* Isabelle/ML name space *)
   1.130  
   1.131  val name_space: ML_Name_Space.T =
   1.132    let
   1.133      fun lookup sel1 sel2 name =
   1.134        Context.thread_data ()
   1.135 -      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
   1.136 +      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
   1.137        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
   1.138  
   1.139      fun all sel1 sel2 () =
   1.140        Context.thread_data ()
   1.141 -      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
   1.142 +      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
   1.143        |> append (sel2 ML_Name_Space.global ())
   1.144        |> sort_distinct (string_ord o pairself #1);
   1.145  
   1.146      fun enter ap1 sel2 entry =
   1.147        if is_some (Context.thread_data ()) then
   1.148 -        Context.>> (Env.map (fn (global, tabs) =>
   1.149 +        Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
   1.150            let
   1.151 -            val _ = if global then sel2 ML_Name_Space.global entry else ();
   1.152 -            val tabs' = ap1 (Symtab.update entry) tabs;
   1.153 -          in (global, tabs') end))
   1.154 +            val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
   1.155 +            val tables' = ap1 (Symtab.update entry) tables;
   1.156 +          in make_data (bootstrap, tables', sml_tables) end))
   1.157        else sel2 ML_Name_Space.global entry;
   1.158    in
   1.159     {lookupVal    = lookup #1 #lookupVal,