# HG changeset patch # User wenzelm # Date 1221679642 -7200 # Node ID 596b0fd784a3f3627f0a2c78af6efa93353b7be0 # Parent a5ac5726a86a79bc6f072cee413b9bebaa026961 ML name space -- dummy version of Poly/ML 5.2 facility. diff -r a5ac5726a86a -r 596b0fd784a3 src/Pure/ML-Systems/ml_name_space.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/ml_name_space.ML Wed Sep 17 21:27:22 2008 +0200 @@ -0,0 +1,58 @@ +(* Title: Pure/ML-Systems/ml_name_space.ML + ID: $Id$ + Author: Makarius + +ML name space -- dummy version of Poly/ML 5.2 facility. +*) + +structure ML_NameSpace = +struct + +type valueVal = unit; +type typeVal = unit; +type fixityVal = unit; +type structureVal = unit; +type signatureVal = unit; +type functorVal = unit; + +type nameSpace = + {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: nameSpace = + {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 _ => []}; + +end;