# HG changeset patch # User haftmann # Date 1116099073 -7200 # Node ID 9bd6550dc004da99a05c5837f34681383b697747 # Parent 366d39e95d3c1b71d4b442316a6647b01586a3ee added Proof.context to antiquotation diff -r 366d39e95d3c -r 9bd6550dc004 doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Fri May 13 20:21:41 2005 +0200 +++ b/doc-src/IsarRef/syntax.tex Sat May 14 21:31:13 2005 +0200 @@ -412,11 +412,13 @@ \begin{matharray}{rcl@{\hspace*{2cm}}rcl} thm & : & \isarantiq & text & : & \isarantiq \\ - lhs & : & \isarantiq & goals & : & \isarantiq \\ - rhs & : & \isarantiq & subgoals & : & \isarantiq \\ - prop & : & \isarantiq & prf & : & \isarantiq \\ - term & : & \isarantiq & full_prf & : & \isarantiq \\ + prop & : & \isarantiq & goals & : & \isarantiq \\ + term & : & \isarantiq & subgoals & : & \isarantiq \\ + const & : & \isarantiq & prf & : & \isarantiq \\ + typeof & : & \isarantiq & full_prf & : & \isarantiq \\ typ & : & \isarantiq \\ + thm_style & : & \isarantiq \\ + term_style & : & \isarantiq \\ \end{matharray} The text body of formal comments (see also \S\ref{sec:comments}) may contain @@ -442,11 +444,13 @@ antiquotation: 'thm' options thmrefs | - 'lhs' options thmrefs | - 'rhs' options thmrefs | 'prop' options prop | 'term' options term | + 'const' options term | + 'typeof' options term | 'typ' options type | + 'thm\_style' options style thmref | + 'term\_style' options style term | 'text' options name | 'goals' options | 'subgoals' options | @@ -469,21 +473,23 @@ $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly useful to suppress printing of schematic variables. -\item [$\at\{lhs~\vec a\}$] prints the left hand sides of theorems $\vec a$. - The antiquotation only works for $\vec a$ that are definitions, - equations or other binary operators. It understands the same - options and attributes as $\at\{thm~\vec a\}$. - -\item [$\at\{rhs~\vec a\}$] prints the right hand sides of theorems $\vec a$. - As for $\at\{lhs~\vec a\}$, $\vec a$ must be definitions, equations or - other binary operators. - \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$. \item [$\at\{term~t\}$] prints a well-typed term $t$. +\item [$\at\{const~c\}$] prints a well-defined constant $c$. + +\item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$. + \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$. +\item [$\at\{thm_style~s~a\}$] prints theorem $a$, previously + applying a style $s$ to it; otherwise behaves the same as $\at\{thm~a\}$ + with just one theorem. + +\item [$\at\{term_style~s~t\}$] prints a well-typed term $t$, previously + applying a style $s$ to it; otherwise behaves the same as $\at\{term~t\}$. + \item [$\at\{text~s\}$] prints uninterpreted source text $s$. This is particularly useful to print portions of text according to the Isabelle {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces @@ -510,6 +516,24 @@ \end{descr} +Per default, each theory contains three default styles for use with +$\at\{thm_style~s~a\}$ and $\at\{term_style~s~t\}$: + +\begin{descr} + +\item [$lhs$] extracts the left hand sides of terms; this style only works + for terms that are definitions, equations or other binary operators. + +\item [$rhs$] extracts the right hand sides of terms; likewise, + this style only works + for terms that are definitions, equations or other binary operators. + +\item [$conlusion$] extracts the conclusion from propositions. + +\end{descr} + +Further styles may be defined at ML level. + \medskip The following options are available to tune the output. Note that most of diff -r 366d39e95d3c -r 9bd6550dc004 doc-src/LaTeXsugar/Sugar/Sugar.thy --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri May 13 20:21:41 2005 +0200 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Sat May 14 21:31:13 2005 +0200 @@ -327,29 +327,41 @@ \end{quote} If you are not afraid of ML, you may also define your own styles. - A style is simply implemented by an ML function of type \verb!term -> term!. - Have a look at the following example (which indeed shows just the way the - \verb!lhs! style is implemented): + A style is implemented by an ML function of type + \verb!Proof.context -> term -> term!. + Have a look at the following example: + \begin{quote} \verb!setup {!\verb!*!\\ \verb!let!\\ - \verb! fun my_lhs (Const ("==", _) $ t $ _) = t!\\ - \verb! | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\ - \verb! | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\ - \verb! | my_lhs (_ $ t $ _) = t!\\ - \verb! | my_lhs _ = error ("Binary operator expected")!\\ - \verb! in [Style.put_style "new_lhs" my_lhs]!\\ + \verb! fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\ + \verb! | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs ctxt t!\\ + \verb! | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\ + \verb! | my_lhs ctxt (_ $ t $ _) = t!\\ + \verb! | my_lhs ctxt _ = error ("Binary operator expected")!\\ + \verb! in [TermStyle.update_style "new_lhs" my_lhs]!\\ \verb!end;!\\ \verb!*!\verb!}!\\ \end{quote} + + This example indeed shows a way the \verb!lhs! style could be implemented; + note that the real implementation is more sophisticated. + This code must go into your theory file, not as part of your \LaTeX\ text but as a separate command in front of it. Like in this example, it is recommended to put the definition of the style function into a \verb!let! expression, in order not to pollute the - ML global namespace. The mapping from identifier name to the style function - is done by the \verb!Style.put_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!new_lhs! allowing + ML global namespace. Each style receives the current proof context + as first argument; this is necessary in situations where the current proof + context has an impact on the style (which is the case e.~g.~when the + style has some object-logic specific behaviour). + + The mapping from identifier name to the style function + is done by the \verb!Style.update_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!new_lhs!, thus allowing antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}! yielding @{thm_style lhs rev_map}. @@ -357,6 +369,7 @@ your own styles; for a description of the constructs used, please refer to the Isabelle reference manual. + *} (*<*) diff -r 366d39e95d3c -r 9bd6550dc004 doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri May 13 20:21:41 2005 +0200 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Sat May 14 21:31:13 2005 +0200 @@ -371,29 +371,41 @@ \end{quote} If you are not afraid of ML, you may also define your own styles. - A style is simply implemented by an ML function of type \verb!term -> term!. - Have a look at the following example (which indeed shows just the way the - \verb!lhs! style is implemented): + A style is implemented by an ML function of type + \verb!Proof.context -> term -> term!. + Have a look at the following example: + \begin{quote} \verb!setup {!\verb!*!\\ \verb!let!\\ - \verb! fun my_lhs (Const ("==", _) $ t $ _) = t!\\ - \verb! | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\ - \verb! | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\ - \verb! | my_lhs (_ $ t $ _) = t!\\ - \verb! | my_lhs _ = error ("Binary operator expected")!\\ - \verb! in [Style.put_style "new_lhs" my_lhs]!\\ + \verb! fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\ + \verb! | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs t!\\ + \verb! | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs t!\\ + \verb! | my_lhs ctxt (_ $ t $ _) = t!\\ + \verb! | my_lhs ctxt _ = error ("Binary operator expected")!\\ + \verb! in [TermStyle.update_style "new_lhs" my_lhs]!\\ \verb!end;!\\ \verb!*!\verb!}!\\ \end{quote} + + This example indeed shows a way the \verb!lhs! style could be implemented; + note that the real implementation is more sophisticated. + This code must go into your theory file, not as part of your \LaTeX\ text but as a separate command in front of it. Like in this example, it is recommended to put the definition of the style function into a \verb!let! expression, in order not to pollute the - ML global namespace. The mapping from identifier name to the style function - is done by the \verb!Style.put_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!new_lhs! allowing + ML global namespace. Each style receives the current proof context + as first argument; this is necessary in situations where the current proof + context has an impact on the style (which is the case e.~g.~when the + style has some object-logic specific behaviour). + + The mapping from identifier name to the style function + is done by the \verb!Style.update_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!new_lhs!, thus allowing antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}! yielding \isa{rev\ {\isacharparenleft}map\ f\ xs{\isacharparenright}}. diff -r 366d39e95d3c -r 9bd6550dc004 src/Pure/Isar/isar_output.ML --- a/src/Pure/Isar/isar_output.ML Fri May 13 20:21:41 2005 +0200 +++ b/src/Pure/Isar/isar_output.ML Sat May 14 21:31:13 2005 +0200 @@ -360,11 +360,15 @@ fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of o ProofContext.extern_skolem ctxt; fun pretty_term_const ctxt (Const c) = pretty_term ctxt (Const c) - | pretty_term_const ctxt term = raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term))) + | pretty_term_const ctxt term = + raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term))) fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of; -fun pretty_term_style ctxt (name, term) = pretty_term ctxt ((Style.get_style (ProofContext.theory_of ctxt) name) term); +fun pretty_term_style ctxt (name, term) = + let + val thy = ProofContext.theory_of ctxt + in pretty_term ctxt (TermStyle.lookup_style thy name ctxt term) end; fun pretty_thm_style ctxt (name, thm) = pretty_term_style ctxt (name, Thm.prop_of thm); diff -r 366d39e95d3c -r 9bd6550dc004 src/Pure/Isar/term_style.ML --- a/src/Pure/Isar/term_style.ML Fri May 13 20:21:41 2005 +0200 +++ b/src/Pure/Isar/term_style.ML Sat May 14 21:31:13 2005 +0200 @@ -5,60 +5,53 @@ Styles for terms, to use with the "term_style" and "thm_style" antiquotations *) -signature STYLE = +(* style data *) +signature TERM_STYLE = sig - val get_style: theory -> string -> (Term.term -> Term.term) - val put_style: string -> (Term.term -> Term.term) -> theory -> theory + val lookup_style: theory -> string -> (Proof.context -> term -> term) + val update_style: string -> (Proof.context -> term -> term) -> theory -> theory end; -structure Style: STYLE = +structure TermStyle: TERM_STYLE = struct -(* exception *) -exception STYLE of string; - -(* style data *) structure StyleArgs = struct val name = "Isar/style"; - type T = (string * (Term.term -> Term.term)) list; - val empty = []; + type T = (Proof.context -> term -> term) Symtab.table; + val empty = Symtab.empty; val copy = I; val prep_ext = I; - fun merge (a1, a2) = Library.foldl Library.overwrite (a1, a2); - (* piecewise update of a1 by a2 *) - fun print _ _ = raise (STYLE "cannot print style (not implemented)"); + val merge = Symtab.merge (K true); + fun print _ table = + Pretty.strs ("defined styles:" :: (Symtab.keys table)) + |> Pretty.writeln; end; structure StyleData = TheoryDataFun(StyleArgs); (* accessors *) -fun get_style thy name = - case Library.assoc_string ((StyleData.get thy), name) - of NONE => raise (STYLE ("no style named " ^ name)) +fun lookup_style thy name = + case Symtab.lookup ((StyleData.get thy), name) + of NONE => raise (ERROR_MESSAGE ("no style named " ^ name)) | SOME style => style -fun put_style name style thy = - StyleData.put (Library.overwrite ((StyleData.get thy), (name, style))) thy; +fun update_style name style thy = + thy + |> StyleData.put (Symtab.update ((name, style), StyleData.get thy)); (* predefined styles *) -fun style_lhs (Const ("==", _) $ t $ _) = t - | style_lhs (Const ("Trueprop", _) $ t) = style_lhs t - | style_lhs (Const ("==>", _) $ _ $ t) = style_lhs t - | style_lhs (_ $ t $ _) = t - | style_lhs _ = error ("Binary operator expected") - -fun style_rhs (Const ("==", _) $ _ $ t) = t - | style_rhs (Const ("Trueprop", _) $ t) = style_rhs t - | style_rhs (Const ("==>", _) $ _ $ t) = style_rhs t - | style_rhs (_ $ _ $ t) = t - | style_rhs _ = error ("Binary operator expected") +fun style_binargs ctxt t = + let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in + case concl of (_ $ l $ r) => (l, r) + | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl) + end; (* initialization *) val _ = Context.add_setup [StyleData.init, - put_style "lhs" style_lhs, - put_style "rhs" style_rhs, - put_style "conclusion" Logic.strip_imp_concl + update_style "lhs" (fst oo style_binargs), + update_style "rhs" (snd oo style_binargs), + update_style "conclusion" (K Logic.strip_imp_concl) ]; end;