--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Sep 05 16:42:23 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Sep 05 16:42:32 2006 +0200
@@ -357,7 +357,7 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Context data%
+\isamarkupsubsection{Context data \label{sec:context-data}%
}
\isamarkuptrue%
%
@@ -473,124 +473,78 @@
%
\endisadelimmlref
%
-\isamarkupsection{Name spaces%
+\isamarkupsection{Names%
}
\isamarkuptrue%
%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
\begin{isamarkuptext}%
-FIXME tune
+In principle, a name is just a string, but there are various
+ convention for encoding additional structure.
- By general convention, each kind of formal entities (logical
- constant, type, type class, theorem, method etc.) lives in a
- separate name space. It is usually clear from the syntactic context
- of a name, which kind of entity it refers to. For example, proof
- method \isa{foo} vs.\ theorem \isa{foo} vs.\ logical
- constant \isa{foo} are easily distinguished thanks to the design
- of the concrete outer syntax. A notable exception are logical
- identifiers within a term (\secref{sec:terms}): constants, fixed
- variables, and bound variables all share the same identifier syntax,
- but are distinguished by their scope.
-
- Name spaces are organized uniformly, as a collection of qualified
- names consisting of a sequence of basic name components separated by
- dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
- are examples for qualified names.
-
- Despite the independence of names of different kinds, certain naming
- conventions may relate them to each other. For example, a constant
- \isa{foo} could be accompanied with theorems \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. The same
- could happen for a type \isa{foo}, but this is apt to cause
- clashes in the theorem name space! To avoid this, there is an
- additional convention to add a suffix that determines the original
- kind. For example, constant \isa{foo} could associated with
- theorem \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.
-
- \medskip Name components are subdivided into \emph{symbols}, which
- constitute the smallest textual unit in Isabelle --- raw characters
- are normally not encountered.%
+ For example, the string ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a
+ qualified name. The most basic constituents of names may have their
+ own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
+ considered as a single symbol (printed as ``\isa{{\isasymalpha}}'').%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
\isamarkupsubsection{Strings of symbols%
}
\isamarkuptrue%
%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
\begin{isamarkuptext}%
-FIXME tune
+\glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
+ plain ASCII characters as well as an infinite collection of named
+ symbols (for greek, math etc.).}
- Isabelle strings consist of a sequence of
- symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
- subsumes plain ASCII characters as well as an infinite collection of
- named symbols (for greek, math etc.).}, which are either packed as
- an actual \isa{string}, or represented as a list. Each symbol
- is in itself a small string of the following form:
+ A \emph{symbol} constitutes the smallest textual unit in Isabelle
+ --- raw characters are normally not encountered. Isabelle strings
+ consist of a sequence of symbols, represented as a packed string or
+ a list of symbols. Each symbol is in itself a small string, which
+ is of one of the following forms:
\begin{enumerate}
- \item either a singleton ASCII character ``\isa{c}'' (with
- character code 0--127), for example ``\verb,a,'',
+ \item singleton ASCII character ``\isa{c}'' (character code
+ 0--127), for example ``\verb,a,'',
- \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
+ \item regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
+ for example ``\verb,\,\verb,<alpha>,'',
- \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
+ \item control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
+ for example ``\verb,\,\verb,<^bold>,'',
- \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
- character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
- character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
+ \item raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' where
+ \isa{text} is constists of printable characters excluding
+ ``\verb,.,'' and ``\verb,>,'', for example
+ ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
- \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
+ \item numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
``\verb,\,\verb,<^raw42>,''.
\end{enumerate}
- The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and
- \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many regular symbols
- and control symbols available, but a certain collection of standard
- symbols is treated specifically. For example,
+ \noindent The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many
+ regular symbols and control symbols, but a fixed collection of
+ standard symbols is treated specifically. For example,
``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
which means it may occur within regular Isabelle identifier syntax.
- Output of symbols depends on the print mode
- (\secref{sec:print-mode}). For example, the standard {\LaTeX} setup
- of the Isabelle document preparation system would present
- ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
- ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
+ Note that the character set underlying Isabelle symbols is plain
+ 7-bit ASCII. Since 8-bit characters are passed through
+ transparently, Isabelle may process Unicode/UCS data (in UTF-8
+ encoding) as well. Unicode provides its own collection of
+ mathematical symbols, but there is no built-in link to the ones of
+ Isabelle.
- \medskip It is important to note that the character set underlying
- Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
- passed through transparently, Isabelle may easily process
- Unicode/UCS data as well (using UTF-8 encoding). Unicode provides
- its own collection of mathematical symbols, but there is no built-in
- link to the ones of Isabelle.%
+ \medskip Output of Isabelle symbols depends on the print mode
+ (\secref{FIXME}). For example, the standard {\LaTeX} setup of the
+ Isabelle document preparation system would present
+ ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
+ ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
\isadelimmlref
%
\endisadelimmlref
@@ -615,15 +569,13 @@
type is an alias for \verb|string|, but emphasizes the
specific format encountered here.
- \item \verb|Symbol.explode|~\isa{s} produces a symbol list from
- the packed form that is encountered in most practical situations.
- This function supercedes \verb|String.explode| for virtually all
- purposes of manipulating text in Isabelle! Plain \verb|implode|
- may still be used for the reverse operation.
+ \item \verb|Symbol.explode|~\isa{str} produces a symbol list
+ from the packed form that. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
+ Isabelle!
- \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
- (both ASCII and several named ones) according to fixed syntactic
- conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
+ \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
+ symbols according to fixed syntactic conventions of Isabelle, cf.\
+ \cite{isabelle-isar-ref}.
\item \verb|Symbol.sym| is a concrete datatype that represents
the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
@@ -642,45 +594,43 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Qualified names%
+\isamarkupsubsection{Basic names \label{sec:basic-names}%
}
\isamarkuptrue%
%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
\begin{isamarkuptext}%
-FIXME tune
+A \emph{basic name} essentially consists of a single Isabelle
+ identifier. There are conventions to mark separate classes of basic
+ names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
+ underscore means \emph{internal name}, two underscores means
+ \emph{Skolem name}, three underscores means \emph{internal Skolem
+ name}.
+
+ For example, the basic name \isa{foo} has the internal version
+ \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
- A \emph{qualified name} essentially consists of a non-empty list of
- basic name components. The packad notation uses a dot as separator,
- as in \isa{A{\isachardot}b}, for example. The very last component is called
- \emph{base} name, the remaining prefix \emph{qualifier} (which may
- be empty).
+ Such special versions are required for bookkeeping of names that are
+ apart from anything that may appear in the text given by the user.
+ In particular, system generated variables in high-level Isar proof
+ contexts are usually marked as internal, which prevents mysterious
+ name references such as \isa{xaa} in the text.
+
+ \medskip Basic manipulations of binding scopes requires names to be
+ modified. A \emph{name context} contains a collection of already
+ used names, which is maintained by the \isa{declare} operation.
- A \isa{naming} policy tells how to produce fully qualified names
- from a given specification. The \isa{full} operation applies
- performs naming of a name; the policy is usually taken from the
- context. For example, a common policy is to attach an implicit
- prefix.
+ The \isa{invents} operation derives a number of fresh names
+ derived from a given starting point. For example, three names
+ derived from \isa{a} are \isa{a}, \isa{b}, \isa{c},
+ provided there are no clashes with already used names.
- A \isa{name\ space} manages declarations of fully qualified
- names. There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.
-
- FIXME%
+ The \isa{variants} operation produces fresh names by
+ incrementing given names as to base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}). For example, name \isa{foo} results in variants
+ \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab}, \dots; each renaming step picks the next
+ unused variant from this list.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
\isadelimmlref
%
\endisadelimmlref
@@ -688,7 +638,99 @@
\isatagmlref
%
\begin{isamarkuptext}%
-FIXME%
+\begin{mldecls}
+ \indexml{Name.internal}\verb|Name.internal: string -> string| \\
+ \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
+ \indexmltype{Name.context}\verb|type Name.context| \\
+ \indexml{Name.context}\verb|Name.context: Name.context| \\
+ \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
+ \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
+ \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Name.internal|~\isa{name} produces an internal name
+ by adding one underscore.
+
+ \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
+ adding two underscores.
+
+ \item \verb|Name.context| represents the context of already used
+ names; the initial value is \verb|Name.context|.
+
+ \item \verb|Name.declare|~\isa{name} declares \isa{name} as
+ being used.
+
+ \item \verb|Name.invents|~\isa{context\ base\ n} produces \isa{n} fresh names derived from \isa{base}.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Indexed names%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
+ name with a natural number. This representation allows efficient
+ renaming by incrementing the second component only. To rename two
+ collections of indexnames apart from each other, first determine the
+ maximum index \isa{maxidx} of the first collection, then
+ increment all indexes of the second collection by \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}. Note that the maximum index of an empty collection is \isa{{\isacharminus}{\isadigit{1}}}.
+
+ Isabelle syntax observes the following rules for representing an
+ indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
+
+ \begin{itemize}
+
+ \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
+
+ \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
+
+ \item \isa{{\isacharquery}x{\isachardot}i} else.
+
+ \end{itemize}
+
+ Occasionally, basic names and indexed names are injected into the
+ same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
+ to encode basic names.
+
+ \medskip Indexnames may acquire arbitrary large index numbers over
+ time. Results are usually normalized towards \isa{{\isadigit{0}}} at certain
+ checkpoints, such that the very end of a proof. This works by
+ producing variants of the corresponding basic names
+ (\secref{sec:basic-names}). For example, the collection \isa{{\isacharquery}x{\isachardot}{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{4}}{\isadigit{2}}} then becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexmltype{indexname}\verb|type indexname| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|indexname| represents indexed names. This is an
+ abbreviation for \verb|string * int|. The second component is
+ usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
+ is used to embed plain names.
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -699,36 +741,153 @@
%
\endisadelimmlref
%
-\isamarkupsection{Structured output%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Pretty printing%
+\isamarkupsubsection{Qualified names and name spaces%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+A \emph{qualified name} consists of a non-empty sequence of basic
+ name components. The packed representation a dot as separator, for
+ example in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called
+ \emph{base} name, the remaining prefix \emph{qualifier} (which may
+ be empty).
+
+ The empty name is commonly used as an indication of unnamed
+ entities, if this makes any sense. The operations on qualified
+ names are smart enough to pass through such improper names
+ unchanged.
+
+ The basic idea of qualified names is to encode a hierarchically
+ structured name spaces by recording the access path as part of the
+ name. For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
+ entity \isa{c} within a local structure \isa{b} of the
+ enclosing structure \isa{A}. Typically, name space hierarchies
+ consist of 1--3 levels, but this need not be always so.
+
+ \medskip A \isa{naming} policy tells how to turn a name
+ specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
+ externally.
+
+ For example, the default naming prefixes an implicit path from the
+ context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
+ standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
+ partial \isa{path} specifications.
+
+ Normally, the naming is implicit in the theory or proof context.
+ There are separate versions of the corresponding operations for these
+ context types.
+
+ \medskip A \isa{name\ space} manages a collection of fully
+ internalized names, together with a mapping between external names
+ and internal names (in both directions). The corresponding \isa{intern} and \isa{extern} operations are mostly used for
+ parsing and printing only! The \isa{declare} operation augments
+ a name space according to a given naming policy.
+
+ By general convention, there are separate name spaces for each kind
+ of formal entity, such as logical constant, type, type class,
+ theorem etc. It is usually clear from the occurrence in concrete
+ syntax (or from the scope) which kind of entity a name refers to.
+
+ For example, the very same name \isa{c} may be used uniformly
+ for a constant, type, type class, which are from separate syntactic
+ categories. There is a common convention to name theorems
+ systematically, according to the name of the main logical entity
+ being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
+ theorems related to constant \isa{c}.
+
+ This technique of mapping names from one space into another requires
+ some care in order to avoid conflicts. In particular, theorem names
+ derived from type or class names are better suffixed in addition to
+ the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c} and class
+ \isa{c}, respectively.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Output channels%
-}
-\isamarkuptrue%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
%
\begin{isamarkuptext}%
-FIXME%
+\begin{mldecls}
+ \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
+ \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\
+ \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
+ \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
+ \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
+ \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
+ \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
+ \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
+ \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
+ \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
+ \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
+ \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
+ \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
+ \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
+ \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|NameSpace.base|~\isa{name} returns the base name of a
+ qualified name.
+
+ \item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
+ of a qualified name.
+
+ \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
+ appends two qualified names.
+
+ \item \verb|NameSpace.pack|~\isa{name} and \isa{NameSpace{\isachardot}unpack}~\isa{names} convert between the packed
+ string representation and explicit list form of qualified names.
+
+ \item \verb|NameSpace.naming| represents the abstract concept of
+ a naming policy.
+
+ \item \verb|NameSpace.default_naming| is the default naming policy.
+ In a theory context, this is usually augmented by a path prefix
+ consisting of the theory name.
+
+ \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
+ naming policy by extending its path.
+
+ \item \verb|NameSpace.full|\isa{naming\ name} turns a name
+ specification (usually a basic name) into the fully qualified
+ internal version, according to the given naming policy.
+
+ \item \verb|NameSpace.T| represents name spaces.
+
+ \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} provide basic operations for
+ building name spaces in accordance to the usual theory data
+ management (\secref{sec:context-data}).
+
+ \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
+ fully qualified name into the name space, with partial accesses
+ being derived from the given policy.
+
+ \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
+ (partially qualified) external name.
+
+ This operation is mostly for parsing. Note that fully qualified
+ names stemming from declarations are produced via \verb|NameSpace.full| (or derivatives for \verb|theory| or \verb|Proof.context|).
+
+ \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
+ (fully qualified) internal name.
+
+ This operation is mostly for printing. Note unqualified names are
+ produced via \verb|NameSpace.base|.
+
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Print modes \label{sec:print-mode}%
-}
-\isamarkuptrue%
+\endisatagmlref
+{\isafoldmlref}%
%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimmlref
+%
+\endisadelimmlref
%
\isadelimtheory
%