wenzelm@28267: (*  Title:      Pure/ML-Systems/ml_name_space.ML
wenzelm@28267:     Author:     Makarius
wenzelm@28267: 
wenzelm@28267: ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm@28267: *)
wenzelm@28267: 
wenzelm@28267: structure ML_NameSpace =
wenzelm@28267: struct
wenzelm@28267: 
wenzelm@28267: type valueVal = unit;
wenzelm@28267: type typeVal = unit;
wenzelm@28267: type fixityVal = unit;
wenzelm@28267: type structureVal = unit;
wenzelm@28267: type signatureVal = unit;
wenzelm@28267: type functorVal = unit;
wenzelm@28267: 
wenzelm@28267: type nameSpace =
wenzelm@28267:  {lookupVal:    string -> valueVal option,
wenzelm@28267:   lookupType:   string -> typeVal option,
wenzelm@28267:   lookupFix:    string -> fixityVal option,
wenzelm@28267:   lookupStruct: string -> structureVal option,
wenzelm@28267:   lookupSig:    string -> signatureVal option,
wenzelm@28267:   lookupFunct:  string -> functorVal option,
wenzelm@28267:   enterVal:     string * valueVal -> unit,
wenzelm@28267:   enterType:    string * typeVal -> unit,
wenzelm@28267:   enterFix:     string * fixityVal -> unit,
wenzelm@28267:   enterStruct:  string * structureVal -> unit,
wenzelm@28267:   enterSig:     string * signatureVal -> unit,
wenzelm@28267:   enterFunct:   string * functorVal -> unit,
wenzelm@28267:   allVal:       unit -> (string * valueVal) list,
wenzelm@28267:   allType:      unit -> (string * typeVal) list,
wenzelm@28267:   allFix:       unit -> (string * fixityVal) list,
wenzelm@28267:   allStruct:    unit -> (string * structureVal) list,
wenzelm@28267:   allSig:       unit -> (string * signatureVal) list,
wenzelm@28267:   allFunct:     unit -> (string * functorVal) list};
wenzelm@28267: 
wenzelm@28267: val global: nameSpace =
wenzelm@28267:  {lookupVal = fn _ => NONE,
wenzelm@28267:   lookupType = fn _ => NONE,
wenzelm@28267:   lookupFix = fn _ => NONE,
wenzelm@28267:   lookupStruct = fn _ => NONE,
wenzelm@28267:   lookupSig = fn _ => NONE,
wenzelm@28267:   lookupFunct = fn _ => NONE,
wenzelm@28267:   enterVal = fn _ => (),
wenzelm@28267:   enterType = fn _ => (),
wenzelm@28267:   enterFix = fn _ => (),
wenzelm@28267:   enterStruct = fn _ => (),
wenzelm@28267:   enterSig = fn _ => (),
wenzelm@28267:   enterFunct = fn _ => (),
wenzelm@28267:   allVal = fn _ => [],
wenzelm@28267:   allType = fn _ => [],
wenzelm@28267:   allFix = fn _ => [],
wenzelm@28267:   allStruct = fn _ => [],
wenzelm@28267:   allSig = fn _ => [],
wenzelm@28267:   allFunct = fn _ => []};
wenzelm@28267: 
wenzelm@28267: end;