src/Pure/ML/ml_env.ML
changeset 56618 874bdedb2313
parent 56275 600f432ab556
child 59058 a78612c67ec0
     1.1 --- a/src/Pure/ML/ml_env.ML	Thu Apr 17 14:52:23 2014 +0200
     1.2 +++ b/src/Pure/ML/ml_env.ML	Sat Apr 19 17:23:05 2014 +0200
     1.3 @@ -8,9 +8,9 @@
     1.4  signature ML_ENV =
     1.5  sig
     1.6    val inherit: Context.generic -> Context.generic -> Context.generic
     1.7 -  val SML_name_space: ML_Name_Space.T
     1.8 -  val name_space: ML_Name_Space.T
     1.9 +  val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    1.10    val local_context: use_context
    1.11 +  val local_name_space: ML_Name_Space.T
    1.12    val check_functor: string -> unit
    1.13  end
    1.14  
    1.15 @@ -64,62 +64,35 @@
    1.16  val inherit = Env.put o Env.get;
    1.17  
    1.18  
    1.19 -(* SML name space *)
    1.20 -
    1.21 -val SML_name_space: ML_Name_Space.T =
    1.22 -  let
    1.23 -    fun lookup which name =
    1.24 -      Context.the_thread_data ()
    1.25 -      |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
    1.26 -
    1.27 -    fun all which () =
    1.28 -      Context.the_thread_data ()
    1.29 -      |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
    1.30 -      |> sort_distinct (string_ord o pairself #1);
    1.31 +(* name space *)
    1.32  
    1.33 -    fun enter which entry =
    1.34 -      Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    1.35 -        let val sml_tables' = which (Symtab.update entry) sml_tables
    1.36 -        in make_data (bootstrap, tables, sml_tables') end));
    1.37 -  in
    1.38 -   {lookupVal    = lookup #1,
    1.39 -    lookupType   = lookup #2,
    1.40 -    lookupFix    = lookup #3,
    1.41 -    lookupStruct = lookup #4,
    1.42 -    lookupSig    = lookup #5,
    1.43 -    lookupFunct  = lookup #6,
    1.44 -    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
    1.45 -    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
    1.46 -    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
    1.47 -    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
    1.48 -    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
    1.49 -    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
    1.50 -    allVal       = all #1,
    1.51 -    allType      = all #2,
    1.52 -    allFix       = all #3,
    1.53 -    allStruct    = all #4,
    1.54 -    allSig       = all #5,
    1.55 -    allFunct     = all #6}
    1.56 -  end;
    1.57 -
    1.58 -
    1.59 -(* Isabelle/ML name space *)
    1.60 -
    1.61 -val name_space: ML_Name_Space.T =
    1.62 +fun name_space {SML, exchange} : ML_Name_Space.T =
    1.63    let
    1.64      fun lookup sel1 sel2 name =
    1.65 -      Context.thread_data ()
    1.66 -      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
    1.67 -      |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
    1.68 +      if SML then
    1.69 +        Context.the_thread_data ()
    1.70 +        |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
    1.71 +      else
    1.72 +        Context.thread_data ()
    1.73 +        |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
    1.74 +        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
    1.75  
    1.76      fun all sel1 sel2 () =
    1.77 -      Context.thread_data ()
    1.78 -      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
    1.79 -      |> append (sel2 ML_Name_Space.global ())
    1.80 +      (if SML then
    1.81 +        Context.the_thread_data ()
    1.82 +        |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
    1.83 +      else
    1.84 +        Context.thread_data ()
    1.85 +        |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
    1.86 +        |> append (sel2 ML_Name_Space.global ()))
    1.87        |> sort_distinct (string_ord o pairself #1);
    1.88  
    1.89      fun enter ap1 sel2 entry =
    1.90 -      if is_some (Context.thread_data ()) then
    1.91 +      if SML <> exchange then
    1.92 +        Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    1.93 +          let val sml_tables' = ap1 (Symtab.update entry) sml_tables
    1.94 +          in make_data (bootstrap, tables, sml_tables') end))
    1.95 +      else if is_some (Context.thread_data ()) then
    1.96          Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
    1.97            let
    1.98              val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
    1.99 @@ -149,12 +122,14 @@
   1.100  
   1.101  val local_context: use_context =
   1.102   {tune_source = ML_Parse.fix_ints,
   1.103 -  name_space = name_space,
   1.104 +  name_space = name_space {SML = false, exchange = false},
   1.105    str_of_pos = Position.here oo Position.line_file,
   1.106    print = writeln,
   1.107    error = error};
   1.108  
   1.109 -val is_functor = is_some o #lookupFunct name_space;
   1.110 +val local_name_space = #name_space local_context;
   1.111 +
   1.112 +val is_functor = is_some o #lookupFunct local_name_space;
   1.113  
   1.114  fun check_functor name =
   1.115    if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()