# HG changeset patch
# User haftmann
# Date 1263286785 -3600
# Node ID ded5b770ec1cfb6a527572b8a28185dff7da78ab
# Parent  b52e03f68cc316b28730f6bb1a425085417e78de
formal antiquotations for ML snippets; no "open" unsynchronized references

diff -r b52e03f68cc3 -r ded5b770ec1c doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Mon Jan 11 23:41:06 2010 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue Jan 12 09:59:45 2010 +0100
@@ -1,6 +1,7 @@
 (*<*)
 theory Sugar
 imports LaTeXsugar OptionalSugar
+uses "~~/doc-src/antiquote_setup"
 begin
 (*>*)
 
@@ -101,7 +102,7 @@
 line. To avoid this, \texttt{OptionalSugar} contains syntax to group
 @{text"@"}-terms to the left before printing, which leads to better
 line breaking behaviour:
-@{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
+@{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>10"}
 
 \end{itemize}
 *}
@@ -131,9 +132,9 @@
 
 This \verb!no_vars! business can become a bit tedious.
 If you would rather never see question marks, simply put
-\begin{verbatim}
-show_question_marks := false;
-\end{verbatim}
+\begin{quote}
+@{ML "Unsynchronized.reset show_question_marks"}\verb!;!
+\end{quote}
 at the beginning of your file \texttt{ROOT.ML}.
 The rest of this document is produced with this flag set to \texttt{false}.
 
@@ -144,7 +145,7 @@
 turning the last digit into a subscript: write \verb!x\<^isub>1! and
 obtain the much nicer @{text"x\<^isub>1"}. *}
 
-(*<*)ML"show_question_marks := false"(*>*)
+(*<*)ML "Unsynchronized.reset show_question_marks"(*>*)
 
 subsection {*Qualified names*}
 
@@ -154,9 +155,9 @@
 "List.length"}. In case there is no danger of confusion, you can insist on
 short names (no qualifiers) by setting \verb!short_names!, typically
 in \texttt{ROOT.ML}:
-\begin{verbatim}
-set short_names;
-\end{verbatim}
+\begin{quote}
+@{ML "Unsynchronized.set short_names"}\verb!;!
+\end{quote}
 *}
 
 subsection {*Variable names\label{sec:varnames}*}
diff -r b52e03f68cc3 -r ded5b770ec1c doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Mon Jan 11 23:41:06 2010 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue Jan 12 09:59:45 2010 +0100
@@ -130,7 +130,7 @@
 \isa{{\isacharat}}-terms to the left before printing, which leads to better
 line breaking behaviour:
 \begin{isabelle}%
-term\isactrlisub {\isadigit{0}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\ \isacharat\ term\isactrlisub {\isadigit{2}}\ \isacharat\ term\isactrlisub {\isadigit{3}}\ \isacharat\ term\isactrlisub {\isadigit{4}}\ \isacharat\ term\isactrlisub {\isadigit{5}}\ \isacharat\ term\isactrlisub {\isadigit{6}}\ \isacharat\ term\isactrlisub {\isadigit{7}}\ \isacharat\ term\isactrlisub {\isadigit{8}}\ \isacharat\ term\isactrlisub {\isadigit{9}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\isactrlisub {\isadigit{0}}%
+term\isactrlisub {\isadigit{0}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\ \isacharat\ term\isactrlisub {\isadigit{2}}\ \isacharat\ term\isactrlisub {\isadigit{3}}\ \isacharat\ term\isactrlisub {\isadigit{4}}\ \isacharat\ term\isactrlisub {\isadigit{5}}\ \isacharat\ term\isactrlisub {\isadigit{6}}\ \isacharat\ term\isactrlisub {\isadigit{7}}\ \isacharat\ term\isactrlisub {\isadigit{8}}\ \isacharat\ term\isactrlisub {\isadigit{9}}\ \isacharat\ term\isactrlisub {\isadigit{1}}{\isadigit{0}}%
 \end{isabelle}
 
 \end{itemize}%
@@ -172,9 +172,9 @@
 
 This \verb!no_vars! business can become a bit tedious.
 If you would rather never see question marks, simply put
-\begin{verbatim}
-show_question_marks := false;
-\end{verbatim}
+\begin{quote}
+\verb|Unsynchronized.reset show_question_marks|\verb!;!
+\end{quote}
 at the beginning of your file \texttt{ROOT.ML}.
 The rest of this document is produced with this flag set to \texttt{false}.
 
@@ -210,9 +210,9 @@
 theory it is defined in, to distinguish it from the predefined \isa{{\isachardoublequote}List{\isachardot}length{\isachardoublequote}}. In case there is no danger of confusion, you can insist on
 short names (no qualifiers) by setting \verb!short_names!, typically
 in \texttt{ROOT.ML}:
-\begin{verbatim}
-set short_names;
-\end{verbatim}%
+\begin{quote}
+\verb|Unsynchronized.set short_names|\verb!;!
+\end{quote}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %