--- 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
--- 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.
+
*}
(*<*)
--- 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}}.
--- 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);
--- 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;