--- a/doc-src/IsarImplementation/Thy/Prelim.thy Sun Mar 08 17:26:14 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sun Mar 08 17:37:18 2009 +0100
@@ -682,11 +682,11 @@
text %mlref {*
\begin{mldecls}
- @{index_ML NameSpace.base_name: "string -> string"} \\
- @{index_ML NameSpace.qualifier: "string -> string"} \\
- @{index_ML NameSpace.append: "string -> string -> string"} \\
- @{index_ML NameSpace.implode: "string list -> string"} \\
- @{index_ML NameSpace.explode: "string -> string list"} \\
+ @{index_ML Long_Name.base_name: "string -> string"} \\
+ @{index_ML Long_Name.qualifier: "string -> string"} \\
+ @{index_ML Long_Name.append: "string -> string -> string"} \\
+ @{index_ML Long_Name.implode: "string list -> string"} \\
+ @{index_ML Long_Name.explode: "string -> string list"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML_type NameSpace.naming} \\
@@ -706,17 +706,17 @@
\begin{description}
- \item @{ML NameSpace.base_name}~@{text "name"} returns the base name of a
+ \item @{ML Long_Name.base_name}~@{text "name"} returns the base name of a
qualified name.
- \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier
+ \item @{ML Long_Name.qualifier}~@{text "name"} returns the qualifier
of a qualified name.
- \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
+ \item @{ML Long_Name.append}~@{text "name\<^isub>1 name\<^isub>2"}
appends two qualified names.
- \item @{ML NameSpace.implode}~@{text "name"} and @{ML
- NameSpace.explode}~@{text "names"} convert between the packed string
+ \item @{ML Long_Name.implode}~@{text "names"} and @{ML
+ Long_Name.explode}~@{text "name"} convert between the packed string
representation and the explicit list form of qualified names.
\item @{ML_type NameSpace.naming} represents the abstract concept of
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Sun Mar 08 17:26:14 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Sun Mar 08 17:37:18 2009 +0100
@@ -791,11 +791,11 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{NameSpace.base\_name}\verb|NameSpace.base_name: string -> string| \\
- \indexdef{}{ML}{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
- \indexdef{}{ML}{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
- \indexdef{}{ML}{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\
- \indexdef{}{ML}{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\
+ \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\
+ \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\
+ \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\
+ \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\
+ \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
@@ -815,16 +815,16 @@
\begin{description}
- \item \verb|NameSpace.base_name|~\isa{name} returns the base name of a
+ \item \verb|Long_Name.base_name|~\isa{name} returns the base name of a
qualified name.
- \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier
+ \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
of a qualified name.
- \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
+ \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
appends two qualified names.
- \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string
+ \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
representation and the explicit list form of qualified names.
\item \verb|NameSpace.naming| represents the abstract concept of
--- a/doc-src/antiquote_setup.ML Sun Mar 08 17:26:14 2009 +0100
+++ b/doc-src/antiquote_setup.ML Sun Mar 08 17:37:18 2009 +0100
@@ -153,7 +153,7 @@
fun output_entity check markup index kind ctxt (logic, name) =
let
- val hyper_name = "{" ^ NameSpace.append kind (NameSpace.append logic (clean_name name)) ^ "}";
+ val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
val hyper =
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";