# HG changeset patch
# User wenzelm
# Date 1286567941 -3600
# Node ID d829ce302ca4bfd687b2b344c60e27051047338b
# Parent  855104e1047c12c238420d210b47ebdae5a6c772
basic setup for ML antiquotations -- with rail diagrams;
tuned;

diff -r 855104e1047c -r d829ce302ca4 doc-src/IsarImplementation/Makefile
--- a/doc-src/IsarImplementation/Makefile	Fri Oct 08 18:05:35 2010 +0100
+++ b/doc-src/IsarImplementation/Makefile	Fri Oct 08 20:59:01 2010 +0100
@@ -11,8 +11,8 @@
 NAME = implementation
 
 FILES = ../extra.sty ../iman.sty ../isabelle.sty ../isabellesym.sty	\
-  ../isar.sty ../manual.bib ../pdfsetup.sty ../proof.sty		\
-  Thy/document/Integration.tex Thy/document/Isar.tex			\
+  ../isar.sty ../manual.bib ../pdfsetup.sty ../proof.sty ../rail.sty	\
+  ../railsetup.sty Thy/document/Integration.tex Thy/document/Isar.tex	\
   Thy/document/Local_Theory.tex Thy/document/Logic.tex			\
   Thy/document/Prelim.tex Thy/document/Proof.tex			\
   Thy/document/Syntax.tex Thy/document/Tactic.tex implementation.tex	\
@@ -22,6 +22,7 @@
 
 $(NAME).dvi: $(FILES) isabelle_isar.eps
 	$(LATEX) $(NAME)
+	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
 	$(LATEX) $(NAME)
@@ -33,6 +34,7 @@
 
 $(NAME).pdf: $(FILES) isabelle_isar.pdf
 	$(PDFLATEX) $(NAME)
+	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(PDFLATEX) $(NAME)
 	$(PDFLATEX) $(NAME)
diff -r 855104e1047c -r d829ce302ca4 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Fri Oct 08 18:05:35 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Fri Oct 08 20:59:01 2010 +0100
@@ -53,7 +53,7 @@
 *}
 
 
-section {* Isar ML commands *}
+subsection {* Isar ML commands *}
 
 text {* The primary Isar source language provides various facilities
   to open a ``window'' to the underlying ML compiler.  Especially see
@@ -131,7 +131,7 @@
 qed
 
 
-section {* Compile-time context *}
+subsection {* Compile-time context *}
 
 text {* Whenever the ML compiler is invoked within Isabelle/Isar, the
   formal context is passed as a thread-local reference variable.  Thus
@@ -153,7 +153,7 @@
   context of the ML toplevel --- at compile time.  ML code needs to
   take care to refer to @{ML "ML_Context.the_generic_context ()"}
   correctly.  Recall that evaluation of a function body is delayed
-  until actual runtime.
+  until actual run-time.
 
   \item @{ML "Context.>>"}~@{text f} applies context transformation
   @{text f} to the implicit context of the ML toplevel.
@@ -162,15 +162,41 @@
 
   It is very important to note that the above functions are really
   restricted to the compile time, even though the ML compiler is
-  invoked at runtime.  The majority of ML code either uses static
+  invoked at run-time.  The majority of ML code either uses static
   antiquotations (\secref{sec:ML-antiq}) or refers to the theory or
   proof context at run-time, by explicit functional abstraction.
 *}
 
 
-section {* Antiquotations \label{sec:ML-antiq} *}
+subsection {* Antiquotations \label{sec:ML-antiq} *}
+
+text {* A very important consequence of embedding SML into Isar is the
+  concept of \emph{ML antiquotation}: the standard token language of
+  ML is augmented by special syntactic entities of the following form:
+
+  \begin{rail}
+  antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym
+  ;
+  \end{rail}
+
+  \noindent Here the syntax categories @{syntax nameref} and @{syntax
+  args} are defined in \cite{isabelle-isar-ref}; attributes and proof
+  methods use similar syntax.
 
-text FIXME
+  \medskip A regular antiquotation @{text "@{name args}"} processes
+  its arguments by the usual means of the Isar source language, and
+  produces corresponding ML source text, either as literal
+  \emph{inline} text (e.g. @{text "@{term t}"}) or abstract
+  \emph{value} (e.g. @{text "@{thm th}"}).  This pre-compilation
+  scheme allows to refer to formal entities in a robust manner, with
+  proper static scoping and with some degree of logical checking of
+  small portions of the code.
 
+  Special antiquotations like @{text "@{let \<dots>}"} or @{text "@{note
+  \<dots>}"} augment the compilation context without generating code.  The
+  non-ASCII braces @{text "\<lbrace>"} and @{text "\<rbrace>"} allow to delimit the
+  effect by introducing local blocks within the pre-compilation
+  environment.
+*}
 
 end
\ No newline at end of file
diff -r 855104e1047c -r d829ce302ca4 doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Fri Oct 08 18:05:35 2010 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Fri Oct 08 20:59:01 2010 +0100
@@ -4,6 +4,7 @@
 \usepackage{../iman,../extra,../isar,../proof}
 \usepackage[nohyphen,strings]{../underscore}
 \usepackage{../isabelle,../isabellesym}
+\usepackage{../ttbox,../rail,../railsetup}
 \usepackage{style}
 \usepackage{../pdfsetup}
 
@@ -22,6 +23,11 @@
 
 \makeindex
 
+\railterm{lbrace,rbrace,atsign}
+\railalias{lbracesym}{\isasymlbrace}\railterm{lbracesym}
+\railalias{rbracesym}{\isasymrbrace}\railterm{rbracesym}
+\railalias{dots}{\isasymdots}\railterm{dots}
+
 
 \begin{document}