src/Doc/Implementation/Syntax.thy

   Some specification package might thus intercept syntax processing at
   a well-defined stage after @{text "parse"}, to a augment the
   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} *}
 
 text {* Read and print operations are roughly dual to each other, such

   (pretty t)"} might fail, or produce a differently typed term, or a
   completely different term in the face of syntactic overloading!  *}
 
 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.
 *}
 
 
 section {* Parsing and unparsing \label{sec:parse-unparse} *}