equal
deleted
inserted
replaced
789 % |
789 % |
790 \isatagmlref |
790 \isatagmlref |
791 % |
791 % |
792 \begin{isamarkuptext}% |
792 \begin{isamarkuptext}% |
793 \begin{mldecls} |
793 \begin{mldecls} |
794 \indexdef{}{ML}{NameSpace.base\_name}\verb|NameSpace.base_name: string -> string| \\ |
794 \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\ |
795 \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\ |
795 \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\ |
796 \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\ |
796 \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\ |
797 \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\ |
797 \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\ |
798 \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\ |
798 \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\ |
799 \end{mldecls} |
799 \end{mldecls} |
800 \begin{mldecls} |
800 \begin{mldecls} |
801 \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\ |
801 \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\ |
802 \indexdef{}{ML}{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\ |
802 \indexdef{}{ML}{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\ |
803 \indexdef{}{ML}{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\ |
803 \indexdef{}{ML}{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\ |
813 \indexdef{}{ML}{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\ |
813 \indexdef{}{ML}{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\ |
814 \end{mldecls} |
814 \end{mldecls} |
815 |
815 |
816 \begin{description} |
816 \begin{description} |
817 |
817 |
818 \item \verb|NameSpace.base_name|~\isa{name} returns the base name of a |
818 \item \verb|Long_Name.base_name|~\isa{name} returns the base name of a |
819 qualified name. |
819 qualified name. |
820 |
820 |
821 \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier |
821 \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier |
822 of a qualified name. |
822 of a qualified name. |
823 |
823 |
824 \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}} |
824 \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}} |
825 appends two qualified names. |
825 appends two qualified names. |
826 |
826 |
827 \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string |
827 \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string |
828 representation and the explicit list form of qualified names. |
828 representation and the explicit list form of qualified names. |
829 |
829 |
830 \item \verb|NameSpace.naming| represents the abstract concept of |
830 \item \verb|NameSpace.naming| represents the abstract concept of |
831 a naming policy. |
831 a naming policy. |
832 |
832 |