src/Pure/RAW/ml_name_space.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_name_space.ML	Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,68 @@
+(*  Title:      Pure/RAW/ml_name_space.ML
+    Author:     Makarius
+
+ML name space -- dummy version of Poly/ML 5.2 facility.
+*)
+
+structure ML_Name_Space =
+struct
+
+type valueVal = unit;
+type typeVal = unit;
+type fixityVal = unit;
+type structureVal = unit;
+type signatureVal = unit;
+type functorVal = unit;
+
+type T =
+ {lookupVal:    string -> valueVal option,
+  lookupType:   string -> typeVal option,
+  lookupFix:    string -> fixityVal option,
+  lookupStruct: string -> structureVal option,
+  lookupSig:    string -> signatureVal option,
+  lookupFunct:  string -> functorVal option,
+  enterVal:     string * valueVal -> unit,
+  enterType:    string * typeVal -> unit,
+  enterFix:     string * fixityVal -> unit,
+  enterStruct:  string * structureVal -> unit,
+  enterSig:     string * signatureVal -> unit,
+  enterFunct:   string * functorVal -> unit,
+  allVal:       unit -> (string * valueVal) list,
+  allType:      unit -> (string * typeVal) list,
+  allFix:       unit -> (string * fixityVal) list,
+  allStruct:    unit -> (string * structureVal) list,
+  allSig:       unit -> (string * signatureVal) list,
+  allFunct:     unit -> (string * functorVal) list};
+
+val global: T =
+ {lookupVal = fn _ => NONE,
+  lookupType = fn _ => NONE,
+  lookupFix = fn _ => NONE,
+  lookupStruct = fn _ => NONE,
+  lookupSig = fn _ => NONE,
+  lookupFunct = fn _ => NONE,
+  enterVal = fn _ => (),
+  enterType = fn _ => (),
+  enterFix = fn _ => (),
+  enterStruct = fn _ => (),
+  enterSig = fn _ => (),
+  enterFunct = fn _ => (),
+  allVal = fn _ => [],
+  allType = fn _ => [],
+  allFix = fn _ => [],
+  allStruct = fn _ => [],
+  allSig = fn _ => [],
+  allFunct = fn _ => []};
+
+val initial_val : (string * valueVal) list = [];
+val initial_type : (string * typeVal) list = [];
+val initial_fixity : (string * fixityVal) list = [];
+val initial_structure : (string * structureVal) list = [];
+val initial_signature : (string * signatureVal) list = [];
+val initial_functor : (string * functorVal) list = [];
+
+fun forget_global_structure (_: string) = ();
+
+fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
+
+end;