doc-src/LaTeXsugar/Sugar/document/Sugar.tex
 changeset 15960 9bd6550dc004 parent 15953 902b556e4bc0 child 15984 bc6ead9d6628
     1.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri May 13 20:21:41 2005 +0200
1.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sat May 14 21:31:13 2005 +0200
1.3 @@ -371,29 +371,41 @@
1.4    \end{quote}
1.5
1.6    If you are not afraid of ML, you may also define your own styles.
1.7 -  A style is simply implemented by an ML function of type \verb!term -> term!.
1.8 -  Have a look at the following example (which indeed shows just the way the
1.9 -  \verb!lhs! style is implemented):
1.10 +  A style is implemented by an ML function of type
1.11 +  \verb!Proof.context -> term -> term!.
1.12 +  Have a look at the following example:
1.13 +
1.14    \begin{quote}
1.15      \verb!setup {!\verb!*!\\
1.16      \verb!let!\\
1.17 -    \verb!  fun my_lhs (Const ("==", _) $t$ _) = t!\\
1.18 -    \verb!    | my_lhs (Const ("Trueprop", _) $t) = my_lhs t!\\ 1.19 - \verb! | my_lhs (Const ("==>", _)$ _ $t) = my_lhs t!\\ 1.20 - \verb! | my_lhs (_$ t $_) = t!\\ 1.21 - \verb! | my_lhs _ = error ("Binary operator expected")!\\ 1.22 - \verb! in [Style.put_style "new_lhs" my_lhs]!\\ 1.23 + \verb! fun my_lhs ctxt (Const ("==", _)$ t $_) = t!\\ 1.24 + \verb! | my_lhs ctxt (Const ("Trueprop", _)$ t) = my_lhs t!\\
1.25 +    \verb!    | my_lhs ctxt (Const ("==>", _) $_$ t) = my_lhs t!\\
1.26 +    \verb!    | my_lhs ctxt (_ $t$ _) = t!\\
1.27 +    \verb!    | my_lhs ctxt _ = error ("Binary operator expected")!\\
1.28 +    \verb!  in [TermStyle.update_style "new_lhs" my_lhs]!\\
1.29      \verb!end;!\\
1.30      \verb!*!\verb!}!\\
1.31    \end{quote}
1.32 +
1.33 +  This example indeed shows a way the \verb!lhs! style could be implemented;
1.34 +  note that the real implementation is more sophisticated.
1.35 +
1.36    This code must go into your theory file, not as part of your
1.37    \LaTeX\ text but as a separate command in front of it.
1.38    Like in this example, it is recommended to put the definition of the style
1.39    function into a \verb!let! expression, in order not to pollute the
1.40 -  ML global namespace. The mapping from identifier name to the style function
1.41 -  is done by the \verb!Style.put_style! expression which expects the desired
1.42 -  style name and the style function as arguments. After this \verb!setup!,
1.43 -  there will be a new style available named \verb!new_lhs! allowing
1.44 +  ML global namespace. Each style receives the current proof context
1.45 +  as first argument; this is necessary in situations where the current proof
1.46 +  context has an impact on the style (which is the case e.~g.~when the
1.47 +  style has some object-logic specific behaviour).
1.48 +
1.49 +  The mapping from identifier name to the style function
1.50 +  is done by the \verb!Style.update_style! expression which expects the desired
1.51 +  style name and the style function as arguments.
1.52 +
1.53 +  After this \verb!setup!,
1.54 +  there will be a new style available named \verb!new_lhs!, thus allowing
1.55    antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}!
1.56    yielding \isa{rev\ {\isacharparenleft}map\ f\ xs{\isacharparenright}}.
1.57