--- a/src/Doc/Implementation/Syntax.thy Thu Jun 19 21:19:30 2014 +0200
+++ b/src/Doc/Implementation/Syntax.thy Thu Jun 19 22:07:44 2014 +0200
@@ -48,7 +48,17 @@
resulting pre-term before full type-reconstruction is performed by
@{text "check"}, for example. Note that the formal status of bound
variables, versus free variables, versus constants must not be
- changed between these phases! *}
+ changed between these phases!
+
+ \medskip In general, @{text check} and @{text uncheck} operate
+ simultaneously on a list of terms. This is particular important for
+ type-checking, to reconstruct types for several terms of the same context
+ and scope. In contrast, @{text parse} and @{text unparse} operate separately
+ in single terms.
+
+ There are analogous operations to read and print types, with the same
+ sub-division into phases.
+*}
section {* Reading and pretty printing \label{sec:read-print} *}
@@ -64,14 +74,72 @@
text %mlref {*
\begin{mldecls}
+ @{index_ML Syntax.read_typs: "Proof.context -> string list -> typ list"} \\
+ @{index_ML Syntax.read_terms: "Proof.context -> string list -> term list"} \\
+ @{index_ML Syntax.read_props: "Proof.context -> string list -> term list"} \\[0.5ex]
@{index_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\
@{index_ML Syntax.read_term: "Proof.context -> string -> term"} \\
- @{index_ML Syntax.read_prop: "Proof.context -> string -> term"} \\
+ @{index_ML Syntax.read_prop: "Proof.context -> string -> term"} \\[0.5ex]
@{index_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\
@{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\
+ @{index_ML Syntax.string_of_typ: "Proof.context -> typ -> string"} \\
+ @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\
\end{mldecls}
- %FIXME description
+ \begin{description}
+
+ \item @{ML Syntax.read_typs}~@{text "ctxt strs"} reads and checks a
+ simultaneous list of source strings as types of the logic.
+
+ \item @{ML Syntax.read_terms}~@{text "ctxt strs"} reads and checks a
+ simultaneous list of source strings as terms of the logic.
+ Type-reconstruction puts all parsed terms into the same scope.
+
+ If particular type-constraints are required for some of the arguments, the
+ read operations needs to be split into its parse and check phases, using
+ @{ML Type.constraint} on the intermediate pre-terms.
+
+ \item @{ML Syntax.read_props} ~@{text "ctxt strs"} reads and checks a
+ simultaneous list of source strings as propositions of the logic, with an
+ implicit type-constraint for each argument to make it of type @{typ prop};
+ this also affects the inner syntax for parsing. The remaining
+ type-reconstructions works as for @{ML Syntax.read_terms} above.
+
+ \item @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop}
+ are like the simultaneous versions above, but operate on a single argument
+ only. This convenient shorthand is adequate in situations where a single
+ item in its own scope is processed. Never use @{ML "map o Syntax.read_term"}
+ where @{ML Syntax.read_terms} is actually intended!
+
+ \item @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML
+ Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type
+ or term, respectively. Although the uncheck phase acts on a simultaneous
+ list as well, this is rarely relevant in practice, so only the singleton
+ case is provided as combined pretty operation. Moreover, the distinction of
+ term vs.\ proposition is ignored here.
+
+ \item @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are
+ convenient compositions of @{ML Syntax.pretty_typ} and @{ML
+ Syntax.pretty_term} with @{ML Pretty.string_of} for output. The result may
+ be concatenated with other strings, as long as there is no further
+ formatting and line-breaking involved.
+
+ \end{description}
+
+ The most important operations in practice are @{ML Syntax.read_term}, @{ML
+ Syntax.read_prop}, and @{ML Syntax.string_of_term}.
+
+ \medskip Note that the string values that are passed in and out here are
+ actually annotated by the system, to carry further markup that is relevant
+ for the Prover IDE \cite{isabelle-jedit}. User code should neither compose
+ its own strings for input, nor try to analyze the string for output.
+
+ The standard way to provide the required position markup for input works via
+ the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already
+ part of @{ML Parse.typ}, @{ML Parse.term}, @{ML Parse.prop}. So a string
+ obtained from one of the latter may be directly passed to the corresponding
+ read operation, in order to get PIDE markup of the input and precise
+ positions for warnings and errors.
*}