--- 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}*}
--- 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%
%