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