# HG changeset patch
# User wenzelm
# Date 1460225230 -7200
# Node ID 6e3fb0aa857a11177a73f812382ccf05d4d17998
# Parent  f14569a9ab9324194f6ec9ed3ebc7815f257297b
tuned signature;
proper signature for structure;

diff -r f14569a9ab93 -r 6e3fb0aa857a src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Sat Apr 09 19:38:25 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Sat Apr 09 20:07:10 2016 +0200
@@ -64,7 +64,7 @@
         is_reported pos ?
           let
             val xml =
-              ML_Name_Space.displayTypeExpression (types, depth, space)
+              PolyML.NameSpace.Values.printType (types, depth, SOME space)
               |> Pretty.from_polyml |> Pretty.string_of
               |> Output.output |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
@@ -211,17 +211,20 @@
           else ();
 
         fun apply_fix (a, b) =
-          (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
+          (#enterFix space (a, b); display PolyML.NameSpace.Infixes.print b);
         fun apply_type (a, b) =
-          (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
+          (#enterType space (a, b);
+            display PolyML.NameSpace.TypeConstrs.print (b, depth, SOME space));
         fun apply_sig (a, b) =
-          (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
+          (#enterSig space (a, b); display PolyML.NameSpace.Signatures.print (b, depth, SOME space));
         fun apply_struct (a, b) =
-          (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
+          (#enterStruct space (a, b);
+            display PolyML.NameSpace.Structures.print (b, depth, SOME space));
         fun apply_funct (a, b) =
-          (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
+          (#enterFunct space (a, b); display PolyML.NameSpace.Functors.print (b, depth, SOME space));
         fun apply_val (a, b) =
-          (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
+          (#enterVal space (a, b);
+            display PolyML.NameSpace.Values.printWithType (b, depth, SOME space));
       in
         List.app apply_fix fixes;
         List.app apply_type types;
diff -r f14569a9ab93 -r 6e3fb0aa857a src/Pure/ML/ml_debugger.ML
--- a/src/Pure/ML/ml_debugger.ML	Sat Apr 09 19:38:25 2016 +0200
+++ b/src/Pure/ML/ml_debugger.ML	Sat Apr 09 20:07:10 2016 +0200
@@ -17,8 +17,8 @@
   type state
   val state: Thread.thread -> state list
   val debug_function: state -> string
-  val debug_function_arg: state -> ML_Name_Space.valueVal
-  val debug_function_result: state -> ML_Name_Space.valueVal
+  val debug_function_arg: state -> PolyML.NameSpace.Values.value
+  val debug_function_result: state -> PolyML.NameSpace.Values.value
   val debug_location: state -> ML_Compiler0.polyml_location
   val debug_name_space: state -> ML_Name_Space.T
   val debug_local_name_space: state -> ML_Name_Space.T
diff -r f14569a9ab93 -r 6e3fb0aa857a src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Sat Apr 09 19:38:25 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Sat Apr 09 20:07:10 2016 +0200
@@ -27,12 +27,12 @@
 (* context data *)
 
 type tables =
-  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;
+  PolyML.NameSpace.Values.value Symtab.table *
+  PolyML.NameSpace.TypeConstrs.typeConstr Symtab.table *
+  PolyML.NameSpace.Infixes.fixity Symtab.table *
+  PolyML.NameSpace.Structures.structureVal Symtab.table *
+  PolyML.NameSpace.Signatures.signatureVal Symtab.table *
+  PolyML.NameSpace.Functors.functorVal Symtab.table;
 
 fun merge_tables
   ((val1, type1, fixity1, structure1, signature1, functor1),
diff -r f14569a9ab93 -r 6e3fb0aa857a src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Sat Apr 09 19:38:25 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Sat Apr 09 20:07:10 2016 +0200
@@ -4,83 +4,91 @@
 ML name space, with initial entries for strict Standard ML.
 *)
 
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-
-  type T = PolyML.NameSpace.nameSpace;
+signature ML_NAME_SPACE =
+sig
+  type T
+  val global: T
+  val global_values: (string * string) list -> T
+  val forget_val: string -> unit
+  val forget_type: string -> unit
+  val forget_structure: string -> unit
+  val bootstrap_values: string list
+  val hidden_structures: string list
+  val bootstrap_structures: string list
+  val bootstrap_signatures: string list
+  val sml_val: (string * PolyML.NameSpace.Values.value) list
+  val sml_type: (string * PolyML.NameSpace.TypeConstrs.typeConstr) list
+  val sml_fixity: (string * PolyML.NameSpace.Infixes.fixity) list
+  val sml_structure: (string * PolyML.NameSpace.Structures.structureVal) list
+  val sml_signature: (string * PolyML.NameSpace.Signatures.signatureVal) list
+  val sml_functor: (string * PolyML.NameSpace.Functors.functorVal) list
+end;
 
-  val global = PolyML.globalNameSpace;
-  fun global_values values : T =
-   {lookupVal = #lookupVal global,
-    lookupType = #lookupType global,
-    lookupStruct = #lookupStruct global,
-    lookupFix = #lookupFix global,
-    lookupSig = #lookupSig global,
-    lookupFunct = #lookupFunct global,
-    enterVal =
-      fn (x, value) =>
-        (case List.find (fn (y, _) => x = y) values of
-          SOME (_, x') => #enterVal global (x', value)
-        | NONE => ()),
-    enterType = fn _ => (),
-    enterFix = fn _ => (),
-    enterStruct = fn _ => (),
-    enterSig = fn _ => (),
-    enterFunct = fn _ => (),
-    allVal = #allVal global,
-    allType = #allType global,
-    allFix = #allFix global,
-    allStruct = #allStruct global,
-    allSig = #allSig global,
-    allFunct = #allFunct global};
+structure ML_Name_Space: ML_NAME_SPACE =
+struct
 
-  type valueVal = Values.value;
-  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
-  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
-  val forget_val = PolyML.Compiler.forgetValue;
-
-  type typeVal = TypeConstrs.typeConstr;
-  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
-  val forget_type = PolyML.Compiler.forgetType;
-
-  type fixityVal = Infixes.fixity;
-  fun displayFix (_: string, x) = Infixes.print x;
-
-  type structureVal = Structures.structureVal;
-  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-  val forget_structure = PolyML.Compiler.forgetStructure;
-
-  type signatureVal = Signatures.signatureVal;
-  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
-
-  type functorVal = Functors.functorVal;
-  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+type T = PolyML.NameSpace.nameSpace;
 
 
-  (* bootstrap environment *)
+(* global *)
 
-  val bootstrap_values =
-    ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
-      "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
-  val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
-  val bootstrap_structures =
-    ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
-      "Private_Output", "PolyML"] @ hidden_structures;
-  val bootstrap_signatures =
-    ["EXN", "OUTPUT_PRIMITIVES", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE",
-      "PRIVATE_OUTPUT"];
+val global = PolyML.globalNameSpace;
+fun global_values values : T =
+ {lookupVal = #lookupVal global,
+  lookupType = #lookupType global,
+  lookupStruct = #lookupStruct global,
+  lookupFix = #lookupFix global,
+  lookupSig = #lookupSig global,
+  lookupFunct = #lookupFunct global,
+  enterVal =
+    fn (x, value) =>
+      (case List.find (fn (y, _) => x = y) values of
+        SOME (_, x') => #enterVal global (x', value)
+      | NONE => ()),
+  enterType = fn _ => (),
+  enterFix = fn _ => (),
+  enterStruct = fn _ => (),
+  enterSig = fn _ => (),
+  enterFunct = fn _ => (),
+  allVal = #allVal global,
+  allType = #allType global,
+  allFix = #allFix global,
+  allStruct = #allStruct global,
+  allSig = #allSig global,
+  allFunct = #allFunct global};
 
 
-  (* Standard ML environment *)
+(* forget entries *)
+
+val forget_val = PolyML.Compiler.forgetValue;
+val forget_type = PolyML.Compiler.forgetType;
+val forget_structure = PolyML.Compiler.forgetStructure;
+
+
+(* bootstrap environment *)
 
-  val sml_val =
-    List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
-  val sml_type = #allType global ();
-  val sml_fixity = #allFix global ();
-  val sml_structure =
-    List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
-  val sml_signature =
-    List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_signatures) (#allSig global ());
-  val sml_functor = #allFunct global ();
+val bootstrap_values =
+  ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
+    "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
+val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+val bootstrap_structures =
+  ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
+    "Private_Output", "PolyML"] @ hidden_structures;
+val bootstrap_signatures =
+  ["EXN", "OUTPUT_PRIMITIVES", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE",
+    "PRIVATE_OUTPUT", "ML_NAME_SPACE"];
+
+
+(* Standard ML environment *)
+
+val sml_val =
+  List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
+val sml_type = #allType global ();
+val sml_fixity = #allFix global ();
+val sml_structure =
+  List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
+val sml_signature =
+  List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_signatures) (#allSig global ());
+val sml_functor = #allFunct global ();
+
 end;
diff -r f14569a9ab93 -r 6e3fb0aa857a src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sat Apr 09 19:38:25 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Sat Apr 09 20:07:10 2016 +0200
@@ -182,7 +182,8 @@
 
     fun print x =
       Pretty.from_polyml
-        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), space));
+        (PolyML.NameSpace.Values.printWithType
+          (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space));
     fun print_all () =
       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)