src/Doc/Implementation/Syntax.thy

+(*:wrap=hard:maxLineLen=78:*)
+
 theory Syntax
 imports Base
 begin
 
 chapter {* Concrete syntax and type-checking *}

   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 here! *}
+  changed between these phases! *}
 
 
 section {* Reading and pretty printing \label{sec:read-print} *}
 
 text {* Read and print operations are roughly dual to each other, such
   that for the user @{text "s' = pretty (read s)"} looks similar to
   the original source text @{text "s"}, but the details depend on many
   side-conditions.  There are also explicit options to control
   suppressing of type information in the output.  The default
   configuration routinely looses information, so @{text "t' = read
-  (pretty t)"} might fail, produce a differently typed term, or a
+  (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_typ: "Proof.context -> string -> typ"} \\

 
 text {* Parsing and unparsing converts between actual source text and
   a certain \emph{pre-term} format, where all bindings and scopes are
   resolved faithfully.  Thus the names of free variables or constants
   are already determined in the sense of the logical context, but type
-  information might is still missing.  Pre-terms support an explicit
+  information might be still missing.  Pre-terms support an explicit
   language of \emph{type constraints} that may be augmented by user
-  code to guide the later \emph{check} phase, for example.
+  code to guide the later \emph{check} phase.
 
   Actual parsing is based on traditional lexical analysis and Earley
   parsing for arbitrary context-free grammars.  The user can specify
-  this via mixfix annotations.  Moreover, there are \emph{syntax
+  the grammar via mixfix annotations.  Moreover, there are \emph{syntax
   translations} that can be augmented by the user, either
   declaratively via @{command translations} or programmatically via
   @{command parse_translation}, @{command print_translation} etc.  The
   final scope resolution is performed by the system, according to name
-  spaces for types, constants etc.\ determined by the context.
+  spaces for types, term variables and constants etc.\ determined by
+  the context.
 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\

   "let"} bindings.  These are expanded during the @{text "check"}
   phase, and contracted during the @{text "uncheck"} phase, without
   affecting the type-assignment of the given terms.
 
   \medskip The precise meaning of type checking depends on the context
-  --- additional check/uncheck plugins might be defined in user space!
+  --- additional check/uncheck plugins might be defined in user space.
 
   For example, the @{command class} command defines a context where
   @{text "check"} treats certain type instances of overloaded
   constants according to the ``dictionary construction'' of its
   logical foundation.  This involves ``type improvement''