equal
deleted
inserted
replaced
680 and class @{text "c"}, respectively. |
680 and class @{text "c"}, respectively. |
681 *} |
681 *} |
682 |
682 |
683 text %mlref {* |
683 text %mlref {* |
684 \begin{mldecls} |
684 \begin{mldecls} |
685 @{index_ML NameSpace.base_name: "string -> string"} \\ |
685 @{index_ML Long_Name.base_name: "string -> string"} \\ |
686 @{index_ML NameSpace.qualifier: "string -> string"} \\ |
686 @{index_ML Long_Name.qualifier: "string -> string"} \\ |
687 @{index_ML NameSpace.append: "string -> string -> string"} \\ |
687 @{index_ML Long_Name.append: "string -> string -> string"} \\ |
688 @{index_ML NameSpace.implode: "string list -> string"} \\ |
688 @{index_ML Long_Name.implode: "string list -> string"} \\ |
689 @{index_ML NameSpace.explode: "string -> string list"} \\ |
689 @{index_ML Long_Name.explode: "string -> string list"} \\ |
690 \end{mldecls} |
690 \end{mldecls} |
691 \begin{mldecls} |
691 \begin{mldecls} |
692 @{index_ML_type NameSpace.naming} \\ |
692 @{index_ML_type NameSpace.naming} \\ |
693 @{index_ML NameSpace.default_naming: NameSpace.naming} \\ |
693 @{index_ML NameSpace.default_naming: NameSpace.naming} \\ |
694 @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\ |
694 @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\ |
704 @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\ |
704 @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\ |
705 \end{mldecls} |
705 \end{mldecls} |
706 |
706 |
707 \begin{description} |
707 \begin{description} |
708 |
708 |
709 \item @{ML NameSpace.base_name}~@{text "name"} returns the base name of a |
709 \item @{ML Long_Name.base_name}~@{text "name"} returns the base name of a |
710 qualified name. |
710 qualified name. |
711 |
711 |
712 \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier |
712 \item @{ML Long_Name.qualifier}~@{text "name"} returns the qualifier |
713 of a qualified name. |
713 of a qualified name. |
714 |
714 |
715 \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"} |
715 \item @{ML Long_Name.append}~@{text "name\<^isub>1 name\<^isub>2"} |
716 appends two qualified names. |
716 appends two qualified names. |
717 |
717 |
718 \item @{ML NameSpace.implode}~@{text "name"} and @{ML |
718 \item @{ML Long_Name.implode}~@{text "names"} and @{ML |
719 NameSpace.explode}~@{text "names"} convert between the packed string |
719 Long_Name.explode}~@{text "name"} convert between the packed string |
720 representation and the explicit list form of qualified names. |
720 representation and the explicit list form of qualified names. |
721 |
721 |
722 \item @{ML_type NameSpace.naming} represents the abstract concept of |
722 \item @{ML_type NameSpace.naming} represents the abstract concept of |
723 a naming policy. |
723 a naming policy. |
724 |
724 |