equal
deleted
inserted
replaced
692 *} |
692 *} |
693 |
693 |
694 text %mlref {* |
694 text %mlref {* |
695 \begin{mldecls} |
695 \begin{mldecls} |
696 @{index_ML NameSpace.base: "string -> string"} \\ |
696 @{index_ML NameSpace.base: "string -> string"} \\ |
697 @{index_ML NameSpace.drop_base: "string -> string"} \\ %FIXME qualifier |
697 @{index_ML NameSpace.qualifier: "string -> string"} \\ |
698 @{index_ML NameSpace.append: "string -> string -> string"} \\ |
698 @{index_ML NameSpace.append: "string -> string -> string"} \\ |
699 @{index_ML NameSpace.pack: "string list -> string"} \\ |
699 @{index_ML NameSpace.pack: "string list -> string"} \\ |
700 @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex] |
700 @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex] |
701 @{index_ML_type NameSpace.naming} \\ |
701 @{index_ML_type NameSpace.naming} \\ |
702 @{index_ML NameSpace.default_naming: NameSpace.naming} \\ |
702 @{index_ML NameSpace.default_naming: NameSpace.naming} \\ |
713 \begin{description} |
713 \begin{description} |
714 |
714 |
715 \item @{ML NameSpace.base}~@{text "name"} returns the base name of a |
715 \item @{ML NameSpace.base}~@{text "name"} returns the base name of a |
716 qualified name. |
716 qualified name. |
717 |
717 |
718 \item @{ML NameSpace.drop_base}~@{text "name"} returns the qualifier |
718 \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier |
719 of a qualified name. |
719 of a qualified name. |
720 |
720 |
721 \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"} |
721 \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"} |
722 appends two qualified names. |
722 appends two qualified names. |
723 |
723 |