preliminary material on "Concrete syntax and type-checking";

--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Oct 20 21:22:56 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Thu Oct 21 20:00:46 2010 +0100
@@ -565,7 +565,7 @@
 
   For example, the predefined configuration option @{attribute
   show_types} controls output of explicit type constraints for
-  variables in printed terms (cf.\ \secref{sec:parse-print}).  Its
+  variables in printed terms (cf.\ \secref{sec:read-print}).  Its
   value can be modified within Isar text like this:
 *}
 

--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Wed Oct 20 21:22:56 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Thu Oct 21 20:00:46 2010 +0100
@@ -6,14 +6,91 @@
 
 text FIXME
 
-
-section {* Parsing and printing \label{sec:parse-print} *}
+section {* Reading and pretty printing \label{sec:read-print} *}
 
 text FIXME
 
+text %mlref {*
+  \begin{mldecls}
+  @{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.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\
+  @{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item FIXME
+
+  \end{description}
+*}
+
+
+section {* Parsing and unparsing \label{sec:parse-unparse} *}
+
+text FIXME
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\
+  @{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\
+  @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\
+  @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\
+  @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item FIXME
+
+  \end{description}
+*}
+
 
 section {* Checking and unchecking \label{sec:term-check} *}
 
 text FIXME
 
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\
+  @{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\
+  @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\
+  @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\
+  @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item FIXME
+
+  \end{description}
+*}
+
+
+section {* Syntax translations *}
+
+text FIXME
+
+text %mlantiq {*
+  \begin{matharray}{rcl}
+  @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\
+  @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
+  @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
+  @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
+  \end{matharray}
+
+  \begin{rail}
+  ('class_syntax' | 'type_syntax' | 'const_syntax' | 'syntax_const') name
+  ;
+  \end{rail}
+
+  \begin{description}
+
+  \item FIXME
+
+  \end{description}
+*}
+
 end