more on names;
authorwenzelm
Tue Sep 05 16:42:23 2006 +0200 (2006-09-05 ago)
changeset 204766d3f144cc1bd
parent 20475 a04bf731ceb6
child 20477 e623b0e30541
more on names;
doc-src/IsarImplementation/Thy/prelim.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Mon Sep 04 20:07:55 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Tue Sep 05 16:42:23 2006 +0200
     1.3 @@ -301,7 +301,8 @@
     1.4    \end{description}
     1.5  *}
     1.6  
     1.7 -subsection {* Context data *}
     1.8 +
     1.9 +subsection {* Context data \label{sec:context-data} *}
    1.10  
    1.11  text {*
    1.12    The main purpose of theory and proof contexts is to manage arbitrary
    1.13 @@ -403,100 +404,75 @@
    1.14  *}
    1.15  
    1.16  
    1.17 -section {* Name spaces *}
    1.18 -
    1.19 -text %FIXME {*
    1.20 -  FIXME tune
    1.21 -
    1.22 -  By general convention, each kind of formal entities (logical
    1.23 -  constant, type, type class, theorem, method etc.) lives in a
    1.24 -  separate name space.  It is usually clear from the syntactic context
    1.25 -  of a name, which kind of entity it refers to.  For example, proof
    1.26 -  method @{text "foo"} vs.\ theorem @{text "foo"} vs.\ logical
    1.27 -  constant @{text "foo"} are easily distinguished thanks to the design
    1.28 -  of the concrete outer syntax.  A notable exception are logical
    1.29 -  identifiers within a term (\secref{sec:terms}): constants, fixed
    1.30 -  variables, and bound variables all share the same identifier syntax,
    1.31 -  but are distinguished by their scope.
    1.32 +section {* Names *}
    1.33  
    1.34 -  Name spaces are organized uniformly, as a collection of qualified
    1.35 -  names consisting of a sequence of basic name components separated by
    1.36 -  dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
    1.37 -  are examples for qualified names.
    1.38 +text {*
    1.39 +  In principle, a name is just a string, but there are various
    1.40 +  convention for encoding additional structure.
    1.41  
    1.42 -  Despite the independence of names of different kinds, certain naming
    1.43 -  conventions may relate them to each other.  For example, a constant
    1.44 -  @{text "foo"} could be accompanied with theorems @{text
    1.45 -  "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The same
    1.46 -  could happen for a type @{text "foo"}, but this is apt to cause
    1.47 -  clashes in the theorem name space!  To avoid this, there is an
    1.48 -  additional convention to add a suffix that determines the original
    1.49 -  kind.  For example, constant @{text "foo"} could associated with
    1.50 -  theorem @{text "foo.intro"}, type @{text "foo"} with theorem @{text
    1.51 -  "foo_type.intro"}, and type class @{text "foo"} with @{text
    1.52 -  "foo_class.intro"}.
    1.53 -
    1.54 -  \medskip Name components are subdivided into \emph{symbols}, which
    1.55 -  constitute the smallest textual unit in Isabelle --- raw characters
    1.56 -  are normally not encountered.
    1.57 +  For example, the string ``@{text "Foo.bar.baz"}'' is considered as a
    1.58 +  qualified name.  The most basic constituents of names may have their
    1.59 +  own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
    1.60 +  considered as a single symbol (printed as ``@{text "\<alpha>"}'').
    1.61  *}
    1.62  
    1.63  
    1.64  subsection {* Strings of symbols *}
    1.65  
    1.66 -text %FIXME {*
    1.67 -  FIXME tune
    1.68 +text {*
    1.69 +  \glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
    1.70 +  plain ASCII characters as well as an infinite collection of named
    1.71 +  symbols (for greek, math etc.).}
    1.72  
    1.73 -  Isabelle strings consist of a sequence of
    1.74 -  symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
    1.75 -  subsumes plain ASCII characters as well as an infinite collection of
    1.76 -  named symbols (for greek, math etc.).}, which are either packed as
    1.77 -  an actual @{text "string"}, or represented as a list.  Each symbol
    1.78 -  is in itself a small string of the following form:
    1.79 +  A \emph{symbol} constitutes the smallest textual unit in Isabelle
    1.80 +  --- raw characters are normally not encountered.  Isabelle strings
    1.81 +  consist of a sequence of symbols, represented as a packed string or
    1.82 +  a list of symbols.  Each symbol is in itself a small string, which
    1.83 +  is of one of the following forms:
    1.84  
    1.85    \begin{enumerate}
    1.86  
    1.87 -  \item either a singleton ASCII character ``@{text "c"}'' (with
    1.88 -  character code 0--127), for example ``\verb,a,'',
    1.89 +  \item singleton ASCII character ``@{text "c"}'' (character code
    1.90 +  0--127), for example ``\verb,a,'',
    1.91  
    1.92 -  \item or a regular symbol ``\verb,\,\verb,<,@{text
    1.93 -  "ident"}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
    1.94 +  \item regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
    1.95 +  for example ``\verb,\,\verb,<alpha>,'',
    1.96  
    1.97 -  \item or a control symbol ``\verb,\,\verb,<^,@{text
    1.98 -  "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
    1.99 +  \item control symbol ``\verb,\,\verb,<^,@{text "ident"}\verb,>,'',
   1.100 +  for example ``\verb,\,\verb,<^bold>,'',
   1.101  
   1.102 -  \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
   1.103 -  "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any printable ASCII
   1.104 -  character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
   1.105 -  character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   1.106 +  \item raw symbol ``\verb,\,\verb,<^raw:,@{text text}\verb,>,'' where
   1.107 +  @{text text} is constists of printable characters excluding
   1.108 +  ``\verb,.,'' and ``\verb,>,'', for example
   1.109 +  ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   1.110  
   1.111 -  \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
   1.112 -  "nnn"}\verb,>, where @{text "nnn"} are digits, for example
   1.113 +  \item numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
   1.114 +  n}\verb,>, where @{text n} consists of digits, for example
   1.115    ``\verb,\,\verb,<^raw42>,''.
   1.116  
   1.117    \end{enumerate}
   1.118  
   1.119 -  The @{text "ident"} syntax for symbol names is @{text "letter
   1.120 -  (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and
   1.121 -  @{text "digit = 0..9"}.  There are infinitely many regular symbols
   1.122 -  and control symbols available, but a certain collection of standard
   1.123 -  symbols is treated specifically.  For example,
   1.124 +  \noindent The @{text "ident"} syntax for symbol names is @{text
   1.125 +  "letter (letter | digit)\<^sup>*"}, where @{text "letter =
   1.126 +  A..Za..z"} and @{text "digit = 0..9"}.  There are infinitely many
   1.127 +  regular symbols and control symbols, but a fixed collection of
   1.128 +  standard symbols is treated specifically.  For example,
   1.129    ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   1.130    which means it may occur within regular Isabelle identifier syntax.
   1.131  
   1.132 -  Output of symbols depends on the print mode
   1.133 -  (\secref{sec:print-mode}).  For example, the standard {\LaTeX} setup
   1.134 -  of the Isabelle document preparation system would present
   1.135 +  Note that the character set underlying Isabelle symbols is plain
   1.136 +  7-bit ASCII.  Since 8-bit characters are passed through
   1.137 +  transparently, Isabelle may process Unicode/UCS data (in UTF-8
   1.138 +  encoding) as well.  Unicode provides its own collection of
   1.139 +  mathematical symbols, but there is no built-in link to the ones of
   1.140 +  Isabelle.
   1.141 +
   1.142 +  \medskip Output of Isabelle symbols depends on the print mode
   1.143 +  (\secref{FIXME}).  For example, the standard {\LaTeX} setup of the
   1.144 +  Isabelle document preparation system would present
   1.145    ``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and
   1.146    ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
   1.147    "\<^bold>\<alpha>"}.
   1.148 -
   1.149 -  \medskip It is important to note that the character set underlying
   1.150 -  Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
   1.151 -  passed through transparently, Isabelle may easily process
   1.152 -  Unicode/UCS data as well (using UTF-8 encoding).  Unicode provides
   1.153 -  its own collection of mathematical symbols, but there is no built-in
   1.154 -  link to the ones of Isabelle.
   1.155  *}
   1.156  
   1.157  text %mlref {*
   1.158 @@ -517,16 +493,15 @@
   1.159    type is an alias for @{ML_type "string"}, but emphasizes the
   1.160    specific format encountered here.
   1.161  
   1.162 -  \item @{ML "Symbol.explode"}~@{text "s"} produces a symbol list from
   1.163 -  the packed form that is encountered in most practical situations.
   1.164 -  This function supercedes @{ML "String.explode"} for virtually all
   1.165 -  purposes of manipulating text in Isabelle!  Plain @{ML "implode"}
   1.166 -  may still be used for the reverse operation.
   1.167 +  \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
   1.168 +  from the packed form that.  This function supercedes @{ML
   1.169 +  "String.explode"} for virtually all purposes of manipulating text in
   1.170 +  Isabelle!
   1.171  
   1.172    \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
   1.173 -  "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
   1.174 -  (both ASCII and several named ones) according to fixed syntactic
   1.175 -  conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
   1.176 +  "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard
   1.177 +  symbols according to fixed syntactic conventions of Isabelle, cf.\
   1.178 +  \cite{isabelle-isar-ref}.
   1.179  
   1.180    \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
   1.181    the different kinds of symbols explicitly with constructors @{ML
   1.182 @@ -540,46 +515,264 @@
   1.183  *}
   1.184  
   1.185  
   1.186 -subsection {* Qualified names *}
   1.187 +subsection {* Basic names \label{sec:basic-names} *}
   1.188 +
   1.189 +text {*
   1.190 +  A \emph{basic name} essentially consists of a single Isabelle
   1.191 +  identifier.  There are conventions to mark separate classes of basic
   1.192 +  names, by attaching a suffix of underscores (@{text "_"}): one
   1.193 +  underscore means \emph{internal name}, two underscores means
   1.194 +  \emph{Skolem name}, three underscores means \emph{internal Skolem
   1.195 +  name}.
   1.196 +
   1.197 +  For example, the basic name @{text "foo"} has the internal version
   1.198 +  @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text
   1.199 +  "foo___"}, respectively.
   1.200 +
   1.201 +  Such special versions are required for bookkeeping of names that are
   1.202 +  apart from anything that may appear in the text given by the user.
   1.203 +  In particular, system generated variables in high-level Isar proof
   1.204 +  contexts are usually marked as internal, which prevents mysterious
   1.205 +  name references such as @{text "xaa"} in the text.
   1.206 +
   1.207 +  \medskip Basic manipulations of binding scopes requires names to be
   1.208 +  modified.  A \emph{name context} contains a collection of already
   1.209 +  used names, which is maintained by the @{text "declare"} operation.
   1.210 +
   1.211 +  The @{text "invents"} operation derives a number of fresh names
   1.212 +  derived from a given starting point.  For example, three names
   1.213 +  derived from @{text "a"} are @{text "a"}, @{text "b"}, @{text "c"},
   1.214 +  provided there are no clashes with already used names.
   1.215 +
   1.216 +  The @{text "variants"} operation produces fresh names by
   1.217 +  incrementing given names as to base-26 numbers (with digits @{text
   1.218 +  "a..z"}).  For example, name @{text "foo"} results in variants
   1.219 +  @{text "fooa"}, @{text "foob"}, @{text "fooc"}, \dots, @{text
   1.220 +  "fooaa"}, @{text "fooab"}, \dots; each renaming step picks the next
   1.221 +  unused variant from this list.
   1.222 +*}
   1.223 +
   1.224 +text %mlref {*
   1.225 +  \begin{mldecls}
   1.226 +  @{index_ML Name.internal: "string -> string"} \\
   1.227 +  @{index_ML Name.skolem: "string -> string"} \\[1ex]
   1.228 +  @{index_ML_type Name.context} \\
   1.229 +  @{index_ML Name.context: Name.context} \\
   1.230 +  @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
   1.231 +  @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
   1.232 +  @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\
   1.233 +  \end{mldecls}
   1.234 +
   1.235 +  \begin{description}
   1.236 +
   1.237 +  \item @{ML Name.internal}~@{text "name"} produces an internal name
   1.238 +  by adding one underscore.
   1.239 +
   1.240 +  \item @{ML Name.skolem}~@{text "name"} produces a Skolem name by
   1.241 +  adding two underscores.
   1.242 +
   1.243 +  \item @{ML_type Name.context} represents the context of already used
   1.244 +  names; the initial value is @{ML "Name.context"}.
   1.245 +
   1.246 +  \item @{ML Name.declare}~@{text "name"} declares @{text "name"} as
   1.247 +  being used.
   1.248  
   1.249 -text %FIXME {*
   1.250 -  FIXME tune
   1.251 +  \item @{ML Name.invents}~@{text "context base n"} produces @{text
   1.252 +  "n"} fresh names derived from @{text "base"}.
   1.253 +
   1.254 +  \end{description}
   1.255 +*}
   1.256 +
   1.257 +
   1.258 +subsection {* Indexed names *}
   1.259 +
   1.260 +text {*
   1.261 +  An \emph{indexed name} (or @{text "indexname"}) is a pair of a basic
   1.262 +  name with a natural number.  This representation allows efficient
   1.263 +  renaming by incrementing the second component only.  To rename two
   1.264 +  collections of indexnames apart from each other, first determine the
   1.265 +  maximum index @{text "maxidx"} of the first collection, then
   1.266 +  increment all indexes of the second collection by @{text "maxidx +
   1.267 +  1"}.  Note that the maximum index of an empty collection is @{text
   1.268 +  "-1"}.
   1.269 +
   1.270 +  Isabelle syntax observes the following rules for representing an
   1.271 +  indexname @{text "(x, i)"} as a packed string:
   1.272 +
   1.273 +  \begin{itemize}
   1.274 +
   1.275 +  \item @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"}.
   1.276 +
   1.277 +  \item @{text "?xi"} if @{text "x"} does not end with a digit,
   1.278 +
   1.279 +  \item @{text "?x.i"} else.
   1.280 +
   1.281 +  \end{itemize}
   1.282  
   1.283 -  A \emph{qualified name} essentially consists of a non-empty list of
   1.284 -  basic name components.  The packad notation uses a dot as separator,
   1.285 -  as in @{text "A.b"}, for example.  The very last component is called
   1.286 +  Occasionally, basic names and indexed names are injected into the
   1.287 +  same pair type: the (improper) indexname @{text "(x, -1)"} is used
   1.288 +  to encode basic names.
   1.289 +
   1.290 +  \medskip Indexnames may acquire arbitrary large index numbers over
   1.291 +  time.  Results are usually normalized towards @{text "0"} at certain
   1.292 +  checkpoints, such that the very end of a proof.  This works by
   1.293 +  producing variants of the corresponding basic names
   1.294 +  (\secref{sec:basic-names}).  For example, the collection @{text
   1.295 +  "?x.1, ?x.7, ?x.42"} then becomes @{text "?x, ?xa, ?xb"}.
   1.296 +*}
   1.297 +
   1.298 +text %mlref {*
   1.299 +  \begin{mldecls}
   1.300 +  @{index_ML_type indexname} \\
   1.301 +  \end{mldecls}
   1.302 +
   1.303 +  \begin{description}
   1.304 +
   1.305 +  \item @{ML_type indexname} represents indexed names.  This is an
   1.306 +  abbreviation for @{ML_type "string * int"}.  The second component is
   1.307 +  usually non-negative, except for situations where @{text "(x, -1)"}
   1.308 +  is used to embed plain names.
   1.309 +
   1.310 +  \end{description}
   1.311 +*}
   1.312 +
   1.313 +
   1.314 +subsection {* Qualified names and name spaces *}
   1.315 +
   1.316 +text {*
   1.317 +  A \emph{qualified name} consists of a non-empty sequence of basic
   1.318 +  name components.  The packed representation a dot as separator, for
   1.319 +  example in ``@{text "A.b.c"}''.  The last component is called
   1.320    \emph{base} name, the remaining prefix \emph{qualifier} (which may
   1.321    be empty).
   1.322  
   1.323 -  A @{text "naming"} policy tells how to produce fully qualified names
   1.324 -  from a given specification.  The @{text "full"} operation applies
   1.325 -  performs naming of a name; the policy is usually taken from the
   1.326 -  context.  For example, a common policy is to attach an implicit
   1.327 -  prefix.
   1.328 +  The empty name is commonly used as an indication of unnamed
   1.329 +  entities, if this makes any sense.  The operations on qualified
   1.330 +  names are smart enough to pass through such improper names
   1.331 +  unchanged.
   1.332 +
   1.333 +  The basic idea of qualified names is to encode a hierarchically
   1.334 +  structured name spaces by recording the access path as part of the
   1.335 +  name.  For example, @{text "A.b.c"} may be understood as a local
   1.336 +  entity @{text "c"} within a local structure @{text "b"} of the
   1.337 +  enclosing structure @{text "A"}.  Typically, name space hierarchies
   1.338 +  consist of 1--3 levels, but this need not be always so.
   1.339 +
   1.340 +  \medskip A @{text "naming"} policy tells how to turn a name
   1.341 +  specification into a fully qualified internal name (by the @{text
   1.342 +  "full"} operation), and how to fully qualified names may be accessed
   1.343 +  externally.
   1.344 +
   1.345 +  For example, the default naming prefixes an implicit path from the
   1.346 +  context: @{text "x"} is becomes @{text "path.x"} internally; the
   1.347 +  standard accesses include @{text "x"}, @{text "path.x"}, and further
   1.348 +  partial @{text "path"} specifications.
   1.349 +
   1.350 +  Normally, the naming is implicit in the theory or proof context.
   1.351 +  There are separate versions of the corresponding operations for these
   1.352 +  context types.
   1.353  
   1.354 -  A @{text "name space"} manages declarations of fully qualified
   1.355 -  names.  There are separate operations to @{text "declare"}, @{text
   1.356 -  "intern"}, and @{text "extern"} names.
   1.357 +  \medskip A @{text "name space"} manages a collection of fully
   1.358 +  internalized names, together with a mapping between external names
   1.359 +  and internal names (in both directions).  The corresponding @{text
   1.360 +  "intern"} and @{text "extern"} operations are mostly used for
   1.361 +  parsing and printing only!  The @{text "declare"} operation augments
   1.362 +  a name space according to a given naming policy.
   1.363 +
   1.364 +  By general convention, there are separate name spaces for each kind
   1.365 +  of formal entity, such as logical constant, type, type class,
   1.366 +  theorem etc.  It is usually clear from the occurrence in concrete
   1.367 +  syntax (or from the scope) which kind of entity a name refers to.
   1.368  
   1.369 -  FIXME
   1.370 +  For example, the very same name @{text "c"} may be used uniformly
   1.371 +  for a constant, type, type class, which are from separate syntactic
   1.372 +  categories.  There is a common convention to name theorems
   1.373 +  systematically, according to the name of the main logical entity
   1.374 +  being involved, such as @{text "c.intro"} and @{text "c.elim"} for
   1.375 +  theorems related to constant @{text "c"}.
   1.376 +
   1.377 +  This technique of mapping names from one space into another requires
   1.378 +  some care in order to avoid conflicts.  In particular, theorem names
   1.379 +  derived from type or class names are better suffixed in addition to
   1.380 +  the usual qualification, e.g.\ @{text "c_type.intro"} and @{text
   1.381 +  "c_class.intro"} for theorems related to type @{text "c"} and class
   1.382 +  @{text "c"}, respectively.
   1.383  *}
   1.384  
   1.385 -text %mlref FIXME
   1.386 -
   1.387 +text %mlref {*
   1.388 +  \begin{mldecls}
   1.389 +  @{index_ML NameSpace.base: "string -> string"} \\
   1.390 +  @{index_ML NameSpace.drop_base: "string -> string"} \\
   1.391 +  @{index_ML NameSpace.append: "string -> string -> string"} \\
   1.392 +  @{index_ML NameSpace.pack: "string list -> string"} \\
   1.393 +  @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
   1.394 +  @{index_ML_type NameSpace.naming} \\
   1.395 +  @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   1.396 +  @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
   1.397 +  @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\[1ex]
   1.398 +  @{index_ML_type NameSpace.T} \\
   1.399 +  @{index_ML NameSpace.empty: NameSpace.T} \\
   1.400 +  @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
   1.401 +  @{index_ML NameSpace.declare: "NameSpace.naming -> string -> NameSpace.T -> NameSpace.T"} \\
   1.402 +  @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
   1.403 +  @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
   1.404 +  \end{mldecls}
   1.405  
   1.406 -section {* Structured output *}
   1.407 +  \begin{description}
   1.408 +
   1.409 +  \item @{ML NameSpace.base}~@{text "name"} returns the base name of a
   1.410 +  qualified name.
   1.411 +
   1.412 +  \item @{ML NameSpace.drop_base}~@{text "name"} returns the qualifier
   1.413 +  of a qualified name.
   1.414  
   1.415 -subsection {* Pretty printing *}
   1.416 +  \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
   1.417 +  appends two qualified names.
   1.418  
   1.419 -text FIXME
   1.420 +  \item @{ML NameSpace.pack}~@{text "name"} and @{text
   1.421 +  "NameSpace.unpack"}~@{text "names"} convert between the packed
   1.422 +  string representation and explicit list form of qualified names.
   1.423 +
   1.424 +  \item @{ML_type NameSpace.naming} represents the abstract concept of
   1.425 +  a naming policy.
   1.426  
   1.427 -subsection {* Output channels *}
   1.428 +  \item @{ML NameSpace.default_naming} is the default naming policy.
   1.429 +  In a theory context, this is usually augmented by a path prefix
   1.430 +  consisting of the theory name.
   1.431 +
   1.432 +  \item @{ML NameSpace.add_path}~@{text "path naming"} augments the
   1.433 +  naming policy by extending its path.
   1.434  
   1.435 -text FIXME
   1.436 +  \item @{ML NameSpace.full}@{text "naming name"} turns a name
   1.437 +  specification (usually a basic name) into the fully qualified
   1.438 +  internal version, according to the given naming policy.
   1.439 +
   1.440 +  \item @{ML_type NameSpace.T} represents name spaces.
   1.441 +
   1.442 +  \item @{ML NameSpace.empty} and @{ML NameSpace.merge}~@{text
   1.443 +  "(space\<^isub>1, space\<^isub>2)"} provide basic operations for
   1.444 +  building name spaces in accordance to the usual theory data
   1.445 +  management (\secref{sec:context-data}).
   1.446  
   1.447 -subsection {* Print modes \label{sec:print-mode} *}
   1.448 +  \item @{ML NameSpace.declare}~@{text "naming name space"} enters a
   1.449 +  fully qualified name into the name space, with partial accesses
   1.450 +  being derived from the given policy.
   1.451 +
   1.452 +  \item @{ML NameSpace.intern}~@{text "space name"} internalizes a
   1.453 +  (partially qualified) external name.
   1.454  
   1.455 -text FIXME
   1.456 +  This operation is mostly for parsing.  Note that fully qualified
   1.457 +  names stemming from declarations are produced via @{ML
   1.458 +  "NameSpace.full"} (or derivatives for @{ML_type theory} or @{ML_type
   1.459 +  Proof.context}).
   1.460  
   1.461 +  \item @{ML NameSpace.extern}~@{text "space name"} externalizes a
   1.462 +  (fully qualified) internal name.
   1.463 +
   1.464 +  This operation is mostly for printing.  Note unqualified names are
   1.465 +  produced via @{ML NameSpace.base}.
   1.466 +
   1.467 +  \end{description}
   1.468 +*}
   1.469  
   1.470  end