doc-src/LaTeXsugar/Sugar/document/Sugar.tex

 %
 \begin{isabellebody}%
 \def\isabellecontext{Sugar}%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isamarkuptrue%
 %
 \isamarkupsection{Introduction%
 }
 \isamarkuptrue%
 %

 marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still
 printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their
 internal index. This can be avoided by turning the last digit into a
 subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isamarkuptrue%
 %
 \isamarkupsubsection{Variable names%
 }
 \isamarkuptrue%
 %

 
   It is usually easiest to put them in figures like the one in Fig.\
   \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
   command:%
 \end{isamarkuptext}%
-\isamarkuptrue%
 %
 \begin{figure}
   \begin{center}\begin{minipage}{0.6\textwidth}  
   \isastyle\isamarkuptrue
+\isamarkupfalse%
 \isacommand{lemma}\ True\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
 \isamarkupfalse%
 \isacommand{proof}\ {\isacharminus}\isanewline
 \ \ %
 \isamarkupcmt{pretty trivial%
 }
 \isanewline
 \ \ \isamarkupfalse%
 \isacommand{show}\ True\ \isamarkupfalse%
 \isacommand{by}\ force\isanewline
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
 %
 \end{minipage}\end{center}
   \caption{Example proof in a figure.}\label{fig:proof}
   \end{figure}
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \begin{quote}
 \small
 \verb!text_raw {!\verb!*!\\

   (e.~g.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}).
 
   Likewise, \verb!concl! may be used as a style to show just the
   conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
   \begin{center}
-    \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+    \isa{{\isacharparenleft}xs{\isasymColon}{\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   \end{center}
   To print just the conclusion,
   \begin{center}
-    \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+    \isa{hd\ {\isacharparenleft}xs{\isasymColon}{\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   \end{center}
   type
   \begin{quote}
     \verb!\begin{center}!\\
-    \verb!@!\verb!{thm_style concl hd_Cons_tl}!\\
+    \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\
     \verb!\end{center}!
   \end{quote}
+
+  Be aware that any options must be placed \emph{before}
+  the name of the style, as in this example.
 
   Further use cases can be found in \S\ref{sec:yourself}.
 
   If you are not afraid of ML, you may also define your own styles.
   A style is implemented by an ML function of type
   \verb!Proof.context -> term -> term!.
   Have a look at the following example:%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \begin{quote}
     \verb!setup {!\verb!*!\\
     \verb!let!\\

   ML global namespace. Each style receives the current proof context
   as first argument; this is helpful in situations where the
   style has some object-logic specific behaviour for example.
 
   The mapping from identifier name to the style function
-  is done by the \isa{TermStyle{\isachardot}add{\isacharunderscore}style} expression which expects the desired
+  is done by the \verb|TermStyle.add_style| expression which expects the desired
   style name and the style function as arguments.
   
   After this \verb!setup!,
   there will be a new style available named \verb!my_concl!, thus allowing
   antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
   yielding \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
 %%% End: