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