--- a/CONTRIBUTORS Mon Mar 09 23:07:41 2009 +0100
+++ b/CONTRIBUTORS Mon Mar 09 23:07:51 2009 +0100
@@ -7,6 +7,10 @@
Contributions to this Isabelle version
--------------------------------------
+* March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
+ Cambridge
+ Elementary topology in Euclidean space.
+
* February 2009: Filip Maric, Univ. of Belgrade
A Serbian theory.
--- a/NEWS Mon Mar 09 23:07:41 2009 +0100
+++ b/NEWS Mon Mar 09 23:07:51 2009 +0100
@@ -75,18 +75,6 @@
class foo = ... instead of class foo = type + ...
-* Type binding gradually replaces formerly used type bstring for names
-to be bound. Name space interface for declarations has been simplified:
-
- NameSpace.declare: NameSpace.naming
- -> binding -> NameSpace.T -> string * NameSpace.T
- NameSpace.bind: NameSpace.naming
- -> binding * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
- (*exception Symtab.DUP*)
-
-See further modules src/Pure/General/binding.ML and
-src/Pure/General/name_space.ML
-
* Module moves in repository:
src/Pure/Tools/value.ML ~> src/Tools/
src/Pure/Tools/quickcheck.ML ~> src/Tools/
@@ -634,13 +622,22 @@
for theorem dependency output of transactions resulting in a new
theory state.
-* Name bindings in higher specification mechanisms (notably
-LocalTheory.define, LocalTheory.note, and derived packages) are now
-formalized as type Name.binding, replacing old bstring.
-INCOMPATIBILITY, need to wrap strings via Name.binding function, see
-also Name.name_of. Packages should pass name bindings given by the
-user to underlying specification mechanisms; this enables precise
-tracking of source positions, for example.
+* More systematic treatment of long names, abstract name bindings, and
+name space operations. Basic operations on qualified names have been
+move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,
+Long_Name.append. Old type bstring has been mostly replaced by
+abstract type binding (see structure Binding), which supports precise
+qualification (by packages and local theory targets), as well as
+proper tracking of source positions. INCOMPATIBILITY, need to wrap
+old bstring values into Binding.name, or better pass through abstract
+bindings everywhere. See further src/Pure/General/long_name.ML,
+src/Pure/General/binding.ML and src/Pure/General/name_space.ML
+
+* Simplified interface for defining document antiquotations via
+ThyOutput.antiquotation, ThyOutput.output, and optionally
+ThyOutput.maybe_pretty_source. INCOMPATIBILITY, need to simplify user
+antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common
+examples.
* Result facts (from PureThy.note_thms, ProofContext.note_thms,
LocalTheory.note etc.) now refer to the *full* internal name, not the
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Mar 09 23:07:51 2009 +0100
@@ -317,61 +317,63 @@
\begin{description}
- \item @{text "show_types = bool"} and @{text "show_sorts = bool"}
- control printing of explicit type and sort constraints.
+ \item @{antiquotation_option_def show_types}~@{text "= bool"} and
+ @{antiquotation_option_def show_sorts}~@{text "= bool"} control
+ printing of explicit type and sort constraints.
- \item @{text "show_structs = bool"} controls printing of implicit
- structures.
+ \item @{antiquotation_option_def show_structs}~@{text "= bool"}
+ controls printing of implicit structures.
- \item @{text "long_names = bool"} forces names of types and
- constants etc.\ to be printed in their fully qualified internal
- form.
+ \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
+ names of types and constants etc.\ to be printed in their fully
+ qualified internal form.
- \item @{text "short_names = bool"} forces names of types and
- constants etc.\ to be printed unqualified. Note that internalizing
- the output again in the current context may well yield a different
- result.
+ \item @{antiquotation_option_def short_names}~@{text "= bool"}
+ forces names of types and constants etc.\ to be printed unqualified.
+ Note that internalizing the output again in the current context may
+ well yield a different result.
- \item @{text "unique_names = bool"} determines whether the printed
- version of qualified names should be made sufficiently long to avoid
- overlap with names declared further back. Set to @{text false} for
- more concise output.
+ \item @{antiquotation_option_def unique_names}~@{text "= bool"}
+ determines whether the printed version of qualified names should be
+ made sufficiently long to avoid overlap with names declared further
+ back. Set to @{text false} for more concise output.
- \item @{text "eta_contract = bool"} prints terms in @{text
- \<eta>}-contracted form.
+ \item @{antiquotation_option_def eta_contract}~@{text "= bool"}
+ prints terms in @{text \<eta>}-contracted form.
- \item @{text "display = bool"} indicates if the text is to be output
- as multi-line ``display material'', rather than a small piece of
- text without line breaks (which is the default).
+ \item @{antiquotation_option_def display}~@{text "= bool"} indicates
+ if the text is to be output as multi-line ``display material'',
+ rather than a small piece of text without line breaks (which is the
+ default).
In this mode the embedded entities are printed in the same style as
the main theory text.
- \item @{text "break = bool"} controls line breaks in non-display
- material.
+ \item @{antiquotation_option_def break}~@{text "= bool"} controls
+ line breaks in non-display material.
- \item @{text "quotes = bool"} indicates if the output should be
- enclosed in double quotes.
+ \item @{antiquotation_option_def quotes}~@{text "= bool"} indicates
+ if the output should be enclosed in double quotes.
- \item @{text "mode = name"} adds @{text name} to the print mode to
- be used for presentation (see also \cite{isabelle-ref}). Note that
- the standard setup for {\LaTeX} output is already present by
- default, including the modes @{text latex} and @{text xsymbols}.
+ \item @{antiquotation_option_def mode}~@{text "= name"} adds @{text
+ name} to the print mode to be used for presentation. Note that the
+ standard setup for {\LaTeX} output is already present by default,
+ including the modes @{text latex} and @{text xsymbols}.
- \item @{text "margin = nat"} and @{text "indent = nat"} change the
- margin or indentation for pretty printing of display material.
-
- \item @{text "goals_limit = nat"} determines the maximum number of
- goals to be printed (for goal-based antiquotation).
+ \item @{antiquotation_option_def margin}~@{text "= nat"} and
+ @{antiquotation_option_def indent}~@{text "= nat"} change the margin
+ or indentation for pretty printing of display material.
- \item @{text "locale = name"} specifies an alternative locale
- context used for evaluating and printing the subsequent argument.
+ \item @{antiquotation_option_def goals_limit}~@{text "= nat"}
+ determines the maximum number of goals to be printed (for goal-based
+ antiquotation).
- \item @{text "source = bool"} prints the original source text of the
- antiquotation arguments, rather than its internal representation.
- Note that formal checking of @{antiquotation "thm"}, @{antiquotation
- "term"}, etc. is still enabled; use the @{antiquotation "text"}
- antiquotation for unchecked output.
+ \item @{antiquotation_option_def source}~@{text "= bool"} prints the
+ original source text of the antiquotation arguments, rather than its
+ internal representation. Note that formal checking of
+ @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still
+ enabled; use the @{antiquotation "text"} antiquotation for unchecked
+ output.
Regular @{text "term"} and @{text "typ"} antiquotations with @{text
"source = false"} involve a full round-trip from the original source
@@ -380,9 +382,10 @@
not under direct control of the author, it may even fluctuate a bit
as the underlying theory is changed later on.
- In contrast, @{text "source = true"} admits direct printing of the
- given source text, with the desirable well-formedness check in the
- background, but without modification of the printed text.
+ In contrast, @{antiquotation_option_def source}~@{text "= true"}
+ admits direct printing of the given source text, with the desirable
+ well-formedness check in the background, but without modification of
+ the printed text.
\end{description}
--- a/doc-src/IsarRef/Thy/Generic.thy Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Mon Mar 09 23:07:51 2009 +0100
@@ -78,13 +78,14 @@
into all goals of the proof state. Note that current facts
indicated for forward chaining are ignored.
- \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method drule}~@{text "a\<^sub>1
- \<dots> a\<^sub>n"}, and @{method frule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the
- basic @{method rule} method (see \secref{sec:pure-meth-att}), but
- apply rules by elim-resolution, destruct-resolution, and
- forward-resolution, respectively \cite{isabelle-ref}. The optional
- natural number argument (default 0) specifies additional assumption
- steps to be performed here.
+ \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
+ drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
+ "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
+ method (see \secref{sec:pure-meth-att}), but apply rules by
+ elim-resolution, destruct-resolution, and forward-resolution,
+ respectively \cite{isabelle-implementation}. The optional natural
+ number argument (default 0) specifies additional assumption steps to
+ be performed here.
Note that these methods are improper ones, mainly serving for
experimentation and tactic script emulation. Different modes of
@@ -143,7 +144,7 @@
specified); the @{attribute COMP} version skips the automatic
lifting process that is normally intended (cf.\ @{ML [source=false]
"op RS"} and @{ML [source=false] "op COMP"} in
- \cite[\S5]{isabelle-ref}).
+ \cite{isabelle-implementation}).
\item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
@@ -304,26 +305,26 @@
\item @{method rule_tac} etc. do resolution of rules with explicit
instantiation. This works the same way as the ML tactics @{ML
- res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
+ res_inst_tac} etc. (see \cite{isabelle-implementation})
Multiple rules may be only given if there is no instantiation; then
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see
- \cite[\S3]{isabelle-ref}).
+ \cite{isabelle-implementation}).
\item @{method cut_tac} inserts facts into the proof state as
assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
- \cite[\S3]{isabelle-ref}. Note that the scope of schematic
+ \cite{isabelle-implementation}. Note that the scope of schematic
variables is spread over the main goal statement. Instantiations
may be given as well, see also ML tactic @{ML cut_inst_tac} in
- \cite[\S3]{isabelle-ref}.
+ \cite{isabelle-implementation}.
\item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
from a subgoal; note that @{text \<phi>} may contain schematic variables.
- See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}.
+ See also @{ML thin_tac} in \cite{isabelle-implementation}.
\item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
- subgoals_tac} in \cite[\S3]{isabelle-ref}.
+ subgoals_tac} in \cite{isabelle-implementation}.
\item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
@@ -333,7 +334,7 @@
goal by @{text n} positions: from right to left if @{text n} is
positive, and from left to right if @{text n} is negative; the
default value is 1. See also @{ML rotate_tac} in
- \cite[\S3]{isabelle-ref}.
+ \cite{isabelle-implementation}.
\item @{method tactic}~@{text "text"} produces a proof method from
any ML text of type @{ML_type tactic}. Apart from the usual ML
@@ -400,13 +401,13 @@
By default the Simplifier methods take local assumptions fully into
account, using equational assumptions in the subsequent
normalization process, or simplifying assumptions themselves (cf.\
- @{ML asm_full_simp_tac} in \cite[\S10]{isabelle-ref}). In
- structured proofs this is usually quite well behaved in practice:
- just the local premises of the actual goal are involved, additional
- facts may be inserted via explicit forward-chaining (via @{command
- "then"}, @{command "from"}, @{command "using"} etc.). The full
- context of premises is only included if the ``@{text "!"}'' (bang)
- argument is given, which should be used with some care, though.
+ @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured
+ proofs this is usually quite well behaved in practice: just the
+ local premises of the actual goal are involved, additional facts may
+ be inserted via explicit forward-chaining (via @{command "then"},
+ @{command "from"}, @{command "using"} etc.). The full context of
+ premises is only included if the ``@{text "!"}'' (bang) argument is
+ given, which should be used with some care, though.
Additional Simplifier options may be specified to tune the behavior
further (mostly for unstructured scripts with many accidental local
@@ -615,14 +616,14 @@
\begin{description}
\item @{method blast} refers to the classical tableau prover (see
- @{ML blast_tac} in \cite[\S11]{isabelle-ref}). The optional
- argument specifies a user-supplied search bound (default 20).
+ @{ML blast_tac} in \cite{isabelle-ref}). The optional argument
+ specifies a user-supplied search bound (default 20).
\item @{method fast}, @{method slow}, @{method best}, @{method
safe}, and @{method clarify} refer to the generic classical
reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
- safe_tac}, and @{ML clarify_tac} in \cite[\S11]{isabelle-ref} for
- more information.
+ safe_tac}, and @{ML clarify_tac} in \cite{isabelle-ref} for more
+ information.
\end{description}
@@ -667,8 +668,8 @@
to Isabelle's combined simplification and classical reasoning
tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
- added as wrapper, see \cite[\S11]{isabelle-ref} for more
- information. The modifier arguments correspond to those given in
+ added as wrapper, see \cite{isabelle-ref} for more information. The
+ modifier arguments correspond to those given in
\secref{sec:simplifier} and \secref{sec:classical}. Just note that
the ones related to the Simplifier are prefixed by \railtterm{simp}
here.
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Mar 09 23:07:51 2009 +0100
@@ -799,8 +799,8 @@
translations functions may refer to specific theory declarations or
auxiliary proof data.
- See also \cite[\S8]{isabelle-ref} for more information on the
- general concept of syntax transformations in Isabelle.
+ See also \cite{isabelle-ref} for more information on the general
+ concept of syntax transformations in Isabelle.
%FIXME proper antiquotations
\begin{ttbox}
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Mar 09 23:07:51 2009 +0100
@@ -335,59 +335,62 @@
\begin{description}
- \item \isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}
- control printing of explicit type and sort constraints.
+ \item \indexdef{}{antiquotation option}{show\_types}\hypertarget{antiquotation option.show-types}{\hyperlink{antiquotation option.show-types}{\mbox{\isa{show{\isacharunderscore}types}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} and
+ \indexdef{}{antiquotation option}{show\_sorts}\hypertarget{antiquotation option.show-sorts}{\hyperlink{antiquotation option.show-sorts}{\mbox{\isa{show{\isacharunderscore}sorts}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} control
+ printing of explicit type and sort constraints.
- \item \isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}} controls printing of implicit
- structures.
+ \item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isacharunderscore}structs}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
+ controls printing of implicit structures.
- \item \isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
- constants etc.\ to be printed in their fully qualified internal
- form.
+ \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} forces
+ names of types and constants etc.\ to be printed in their fully
+ qualified internal form.
- \item \isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
- constants etc.\ to be printed unqualified. Note that internalizing
- the output again in the current context may well yield a different
- result.
+ \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
+ forces names of types and constants etc.\ to be printed unqualified.
+ Note that internalizing the output again in the current context may
+ well yield a different result.
- \item \isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} determines whether the printed
- version of qualified names should be made sufficiently long to avoid
- overlap with names declared further back. Set to \isa{false} for
- more concise output.
+ \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
+ determines whether the printed version of qualified names should be
+ made sufficiently long to avoid overlap with names declared further
+ back. Set to \isa{false} for more concise output.
- \item \isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}} prints terms in \isa{{\isasymeta}}-contracted form.
+ \item \indexdef{}{antiquotation option}{eta\_contract}\hypertarget{antiquotation option.eta-contract}{\hyperlink{antiquotation option.eta-contract}{\mbox{\isa{eta{\isacharunderscore}contract}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
+ prints terms in \isa{{\isasymeta}}-contracted form.
- \item \isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the text is to be output
- as multi-line ``display material'', rather than a small piece of
- text without line breaks (which is the default).
+ \item \indexdef{}{antiquotation option}{display}\hypertarget{antiquotation option.display}{\hyperlink{antiquotation option.display}{\mbox{\isa{display}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
+ if the text is to be output as multi-line ``display material'',
+ rather than a small piece of text without line breaks (which is the
+ default).
In this mode the embedded entities are printed in the same style as
the main theory text.
- \item \isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}} controls line breaks in non-display
- material.
+ \item \indexdef{}{antiquotation option}{break}\hypertarget{antiquotation option.break}{\hyperlink{antiquotation option.break}{\mbox{\isa{break}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} controls
+ line breaks in non-display material.
- \item \isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the output should be
- enclosed in double quotes.
+ \item \indexdef{}{antiquotation option}{quotes}\hypertarget{antiquotation option.quotes}{\hyperlink{antiquotation option.quotes}{\mbox{\isa{quotes}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
+ if the output should be enclosed in double quotes.
- \item \isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to
- be used for presentation (see also \cite{isabelle-ref}). Note that
- the standard setup for {\LaTeX} output is already present by
- default, including the modes \isa{latex} and \isa{xsymbols}.
+ \item \indexdef{}{antiquotation option}{mode}\hypertarget{antiquotation option.mode}{\hyperlink{antiquotation option.mode}{\mbox{\isa{mode}}}}~\isa{{\isachardoublequote}{\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to be used for presentation. Note that the
+ standard setup for {\LaTeX} output is already present by default,
+ including the modes \isa{latex} and \isa{xsymbols}.
- \item \isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}} change the
- margin or indentation for pretty printing of display material.
-
- \item \isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}} determines the maximum number of
- goals to be printed (for goal-based antiquotation).
+ \item \indexdef{}{antiquotation option}{margin}\hypertarget{antiquotation option.margin}{\hyperlink{antiquotation option.margin}{\mbox{\isa{margin}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} and
+ \indexdef{}{antiquotation option}{indent}\hypertarget{antiquotation option.indent}{\hyperlink{antiquotation option.indent}{\mbox{\isa{indent}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} change the margin
+ or indentation for pretty printing of display material.
- \item \isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}} specifies an alternative locale
- context used for evaluating and printing the subsequent argument.
+ \item \indexdef{}{antiquotation option}{goals\_limit}\hypertarget{antiquotation option.goals-limit}{\hyperlink{antiquotation option.goals-limit}{\mbox{\isa{goals{\isacharunderscore}limit}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}}
+ determines the maximum number of goals to be printed (for goal-based
+ antiquotation).
- \item \isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}} prints the original source text of the
- antiquotation arguments, rather than its internal representation.
- Note that formal checking of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}}
- antiquotation for unchecked output.
+ \item \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} prints the
+ original source text of the antiquotation arguments, rather than its
+ internal representation. Note that formal checking of
+ \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still
+ enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation for unchecked
+ output.
Regular \isa{{\isachardoublequote}term{\isachardoublequote}} and \isa{{\isachardoublequote}typ{\isachardoublequote}} antiquotations with \isa{{\isachardoublequote}source\ {\isacharequal}\ false{\isachardoublequote}} involve a full round-trip from the original source
to an internalized logical entity back to a source form, according
@@ -395,9 +398,10 @@
not under direct control of the author, it may even fluctuate a bit
as the underlying theory is changed later on.
- In contrast, \isa{{\isachardoublequote}source\ {\isacharequal}\ true{\isachardoublequote}} admits direct printing of the
- given source text, with the desirable well-formedness check in the
- background, but without modification of the printed text.
+ In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ true{\isachardoublequote}}
+ admits direct printing of the given source text, with the desirable
+ well-formedness check in the background, but without modification of
+ the printed text.
\end{description}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Mon Mar 09 23:07:51 2009 +0100
@@ -99,12 +99,12 @@
into all goals of the proof state. Note that current facts
indicated for forward chaining are ignored.
- \item \hyperlink{method.erule}{\mbox{\isa{erule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \hyperlink{method.frule}{\mbox{\isa{frule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} are similar to the
- basic \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see \secref{sec:pure-meth-att}), but
- apply rules by elim-resolution, destruct-resolution, and
- forward-resolution, respectively \cite{isabelle-ref}. The optional
- natural number argument (default 0) specifies additional assumption
- steps to be performed here.
+ \item \hyperlink{method.erule}{\mbox{\isa{erule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}, and \hyperlink{method.frule}{\mbox{\isa{frule}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} are similar to the basic \hyperlink{method.rule}{\mbox{\isa{rule}}}
+ method (see \secref{sec:pure-meth-att}), but apply rules by
+ elim-resolution, destruct-resolution, and forward-resolution,
+ respectively \cite{isabelle-implementation}. The optional natural
+ number argument (default 0) specifies additional assumption steps to
+ be performed here.
Note that these methods are improper ones, mainly serving for
experimentation and tactic script emulation. Different modes of
@@ -161,7 +161,7 @@
first premise of \isa{a} (an alternative position may be also
specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
lifting process that is normally intended (cf.\ \verb|op RS| and \verb|op COMP| in
- \cite[\S5]{isabelle-ref}).
+ \cite{isabelle-implementation}).
\item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} expand and fold back again the given
definitions throughout a rule.
@@ -321,25 +321,25 @@
\begin{description}
\item \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc. do resolution of rules with explicit
- instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref})
+ instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite{isabelle-implementation})
Multiple rules may be only given if there is no instantiation; then
\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see
- \cite[\S3]{isabelle-ref}).
+ \cite{isabelle-implementation}).
\item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}} inserts facts into the proof state as
assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
- \cite[\S3]{isabelle-ref}. Note that the scope of schematic
+ \cite{isabelle-implementation}. Note that the scope of schematic
variables is spread over the main goal statement. Instantiations
may be given as well, see also ML tactic \verb|cut_inst_tac| in
- \cite[\S3]{isabelle-ref}.
+ \cite{isabelle-implementation}.
\item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}} deletes the specified assumption
from a subgoal; note that \isa{{\isasymphi}} may contain schematic variables.
- See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}.
+ See also \verb|thin_tac| in \cite{isabelle-implementation}.
\item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}} adds \isa{{\isasymphi}} as an
- assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}.
+ assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}.
\item \hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} renames parameters of a
goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the
@@ -349,7 +349,7 @@
goal by \isa{n} positions: from right to left if \isa{n} is
positive, and from left to right if \isa{n} is negative; the
default value is 1. See also \verb|rotate_tac| in
- \cite[\S3]{isabelle-ref}.
+ \cite{isabelle-implementation}.
\item \hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} produces a proof method from
any ML text of type \verb|tactic|. Apart from the usual ML
@@ -420,12 +420,13 @@
By default the Simplifier methods take local assumptions fully into
account, using equational assumptions in the subsequent
normalization process, or simplifying assumptions themselves (cf.\
- \verb|asm_full_simp_tac| in \cite[\S10]{isabelle-ref}). In
- structured proofs this is usually quite well behaved in practice:
- just the local premises of the actual goal are involved, additional
- facts may be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}, \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full
- context of premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang)
- argument is given, which should be used with some care, though.
+ \verb|asm_full_simp_tac| in \cite{isabelle-ref}). In structured
+ proofs this is usually quite well behaved in practice: just the
+ local premises of the actual goal are involved, additional facts may
+ be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
+ \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full context of
+ premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) argument is
+ given, which should be used with some care, though.
Additional Simplifier options may be specified to tune the behavior
further (mostly for unstructured scripts with many accidental local
@@ -637,12 +638,12 @@
\begin{description}
\item \hyperlink{method.blast}{\mbox{\isa{blast}}} refers to the classical tableau prover (see
- \verb|blast_tac| in \cite[\S11]{isabelle-ref}). The optional
- argument specifies a user-supplied search bound (default 20).
+ \verb|blast_tac| in \cite{isabelle-ref}). The optional argument
+ specifies a user-supplied search bound (default 20).
\item \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, \hyperlink{method.safe}{\mbox{\isa{safe}}}, and \hyperlink{method.clarify}{\mbox{\isa{clarify}}} refer to the generic classical
- reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite[\S11]{isabelle-ref} for
- more information.
+ reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite{isabelle-ref} for more
+ information.
\end{description}
@@ -686,8 +687,8 @@
\item \hyperlink{method.auto}{\mbox{\isa{auto}}}, \hyperlink{method.force}{\mbox{\isa{force}}}, \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}, \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, and \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} provide access
to Isabelle's combined simplification and classical reasoning
tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
- added as wrapper, see \cite[\S11]{isabelle-ref} for more
- information. The modifier arguments correspond to those given in
+ added as wrapper, see \cite{isabelle-ref} for more information. The
+ modifier arguments correspond to those given in
\secref{sec:simplifier} and \secref{sec:classical}. Just note that
the ones related to the Simplifier are prefixed by \railtterm{simp}
here.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Mar 09 23:07:51 2009 +0100
@@ -819,8 +819,8 @@
translations functions may refer to specific theory declarations or
auxiliary proof data.
- See also \cite[\S8]{isabelle-ref} for more information on the
- general concept of syntax transformations in Isabelle.
+ See also \cite{isabelle-ref} for more information on the general
+ concept of syntax transformations in Isabelle.
%FIXME proper antiquotations
\begin{ttbox}
--- a/doc-src/Locales/Locales/Examples.thy Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy Mon Mar 09 23:07:51 2009 +0100
@@ -109,9 +109,11 @@
At the same time, the locale is extended by syntax information
hiding this construction in the context of the locale. That is,
@{term "partial_order.less le"} is printed and parsed as infix
- @{text \<sqsubset>}. Finally, the conclusion of the definition is added to
- the locale, @{thm [locale=partial_order, source] less_def}:
- @{thm [locale=partial_order, display, indent=2] less_def}
+ @{text \<sqsubset>}. *}
+
+text (in partial_order) {* Finally, the conclusion of the definition
+ is added to the locale, @{thm [source] less_def}:
+ @{thm [display, indent=2] less_def}
*}
text {* As an example of a theorem statement in the locale, here is the
--- a/doc-src/Locales/Locales/Examples3.thy Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Mon Mar 09 23:07:51 2009 +0100
@@ -314,8 +314,8 @@
abbreviation (in order_preserving)
less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
-text {* Now the theorem is displayed nicely as
- @{thm [locale=order_preserving] le'.less_le_trans}. *}
+text (in order_preserving) {* Now the theorem is displayed nicely as
+ @{thm le'.less_le_trans}. *}
text {* Not only names of theorems are qualified. In fact, all names
are qualified, in particular names introduced by definitions and
@@ -399,12 +399,12 @@
then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
qed
-text {* Theorems and other declarations --- syntax, in particular ---
- from the locale @{text order_preserving} are now active in @{text
+text (in lattice_hom) {*
+ Theorems and other declarations --- syntax, in particular --- from
+ the locale @{text order_preserving} are now active in @{text
lattice_hom}, for example
-
- @{thm [locale=lattice_hom, source] le'.less_le_trans}:
- @{thm [locale=lattice_hom] le'.less_le_trans}
+ @{thm [source] le'.less_le_trans}:
+ @{thm le'.less_le_trans}
*}
--- a/doc-src/Locales/Locales/document/Examples.tex Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex Mon Mar 09 23:07:51 2009 +0100
@@ -142,8 +142,13 @@
At the same time, the locale is extended by syntax information
hiding this construction in the context of the locale. That is,
\isa{partial{\isacharunderscore}order{\isachardot}less\ le} is printed and parsed as infix
- \isa{{\isasymsqsubset}}. Finally, the conclusion of the definition is added to
- the locale, \isa{less{\isacharunderscore}def}:
+ \isa{{\isasymsqsubset}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Finally, the conclusion of the definition
+ is added to the locale, \isa{less{\isacharunderscore}def}:
\begin{isabelle}%
\ \ {\isacharparenleft}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}%
\end{isabelle}%
--- a/doc-src/Locales/Locales/document/Examples3.tex Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Mar 09 23:07:51 2009 +0100
@@ -686,9 +686,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Theorems and other declarations --- syntax, in particular ---
- from the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
-
+Theorems and other declarations --- syntax, in particular --- from
+ the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
\isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
\isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}%
\end{isamarkuptext}%
--- a/doc-src/antiquote_setup.ML Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/antiquote_setup.ML Mon Mar 09 23:07:51 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: Doc/antiquote_setup.ML
+(* Title: doc-src/antiquote_setup.ML
Author: Makarius
Auxiliary antiquotations for the Isabelle manuals.
@@ -35,8 +35,8 @@
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
-val _ = ThyOutput.antiquotation "verbatim" (fn _ => fn _ =>
- Scan.lift Args.name >> (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
+val _ = ThyOutput.antiquotation "verbatim" (Scan.lift Args.name)
+ (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
(* ML text *)
@@ -52,87 +52,70 @@
fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
| ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
-fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
+fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
-fun ml_functor _ = "val _ = ();"; (*no check!*)
+fun ml_functor _ = ""; (*no check!*)
-fun index_ml kind ml src ctxt (txt1, txt2) =
- let
- val txt = if txt2 = "" then txt1 else
- if kind = "type" then txt1 ^ " = " ^ txt2
- else if kind = "exception" then txt1 ^ " of " ^ txt2
- else txt1 ^ ": " ^ txt2;
- val txt' = if kind = "" then txt else kind ^ " " ^ txt;
- val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
- val kind' = if kind = "" then "ML" else "ML " ^ kind;
- in
- "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
- (txt'
- |> (if ! ThyOutput.quotes then quote else I)
- |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
- else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
- end;
-
-fun output_ml ctxt src =
- if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
- else
- split_lines
- #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
- #> space_implode "\\isasep\\isanewline%\n";
-
-fun ml_args x = ThyOutput.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
+fun index_ml name kind ml = ThyOutput.antiquotation name
+ (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
+ (fn {context = ctxt, ...} => fn (txt1, txt2) =>
+ let
+ val txt =
+ if txt2 = "" then txt1
+ else if kind = "type" then txt1 ^ " = " ^ txt2
+ else if kind = "exception" then txt1 ^ " of " ^ txt2
+ else txt1 ^ ": " ^ txt2;
+ val txt' = if kind = "" then txt else kind ^ " " ^ txt;
+ val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
+ val kind' = if kind = "" then "ML" else "ML " ^ kind;
+ in
+ "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
+ (txt'
+ |> (if ! ThyOutput.quotes then quote else I)
+ |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+ else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
+ end);
in
-val _ = ThyOutput.add_commands
- [("index_ML", ml_args (index_ml "" ml_val)),
- ("index_ML_type", ml_args (index_ml "type" ml_type)),
- ("index_ML_exn", ml_args (index_ml "exception" ml_exn)),
- ("index_ML_structure", ml_args (index_ml "structure" ml_structure)),
- ("index_ML_functor", ml_args (index_ml "functor" ml_functor)),
- ("ML_functor", ThyOutput.args (Scan.lift Args.name) output_ml),
- ("ML_text", ThyOutput.args (Scan.lift Args.name) output_ml)];
+val _ = index_ml "index_ML" "" ml_val;
+val _ = index_ml "index_ML_type" "type" ml_type;
+val _ = index_ml "index_ML_exn" "exception" ml_exn;
+val _ = index_ml "index_ML_structure" "structure" ml_structure;
+val _ = index_ml "index_ML_functor" "functor" ml_functor;
end;
-(* theorems with names *)
-
-local
+(* named theorems *)
-fun output_named_thms src ctxt xs =
- map (apfst (ThyOutput.pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*)
- |> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
- |> (if ! ThyOutput.display then
- map (fn (p, name) =>
- Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
- "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
- #> space_implode "\\par\\smallskip%\n"
- #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else
- map (fn (p, name) =>
- Output.output (Pretty.str_of p) ^
- "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
- #> space_implode "\\par\\smallskip%\n"
- #> enclose "\\isa{" "}");
-
-in
-
-val _ = ThyOutput.add_commands
- [("named_thms", ThyOutput.args (Scan.repeat (Attrib.thm --
- Scan.lift (Args.parens Args.name))) output_named_thms)];
-
-end;
+val _ = ThyOutput.antiquotation "named_thms"
+ (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
+ (fn {context = ctxt, ...} =>
+ map (apfst (ThyOutput.pretty_thm ctxt))
+ #> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
+ #> (if ! ThyOutput.display
+ then
+ map (fn (p, name) =>
+ Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
+ "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
+ #> space_implode "\\par\\smallskip%\n"
+ #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ else
+ map (fn (p, name) =>
+ Output.output (Pretty.str_of p) ^
+ "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
+ #> space_implode "\\par\\smallskip%\n"
+ #> enclose "\\isa{" "}"));
-(* theory files *)
+(* theory file *)
-val _ = ThyOutput.add_commands
- [("thy_file", ThyOutput.args (Scan.lift Args.name) (ThyOutput.output (fn _ => fn name =>
- (ThyLoad.check_thy Path.current name; Pretty.str name))))];
+val _ = ThyOutput.antiquotation "thy_file" (Scan.lift Args.name)
+ (fn _ => fn name => (ThyLoad.check_thy Path.current name; ThyOutput.output [Pretty.str name]));
-(* Isabelle entities (with index) *)
+(* Isabelle/Isar entities (with index) *)
local
@@ -147,56 +130,58 @@
val arg = enclose "{" "}" o clean_string;
-fun output_entity check markup index kind ctxt (logic, name) =
- let
- val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
- val hyper =
- enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
- index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
- val idx =
- (case index of
- NONE => ""
- | SOME is_def =>
- "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
- in
- if check ctxt name then
- idx ^
- (Output.output name
- |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> (if ! ThyOutput.quotes then quote else I)
- |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else hyper o enclose "\\mbox{\\isa{" "}}"))
- else error ("Bad " ^ kind ^ " " ^ quote name)
- end;
-
-fun entity check markup index kind =
- ThyOutput.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
- (K (output_entity check markup index kind));
+fun entity check markup kind index =
+ ThyOutput.antiquotation
+ (translate (fn " " => "_" | c => c) kind ^
+ (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
+ (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
+ (fn {context = ctxt, ...} => fn (logic, name) =>
+ let
+ val hyper_name =
+ "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
+ val hyper =
+ enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
+ index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
+ val idx =
+ (case index of
+ NONE => ""
+ | SOME is_def =>
+ "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
+ in
+ if check ctxt name then
+ idx ^
+ (Output.output name
+ |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
+ |> (if ! ThyOutput.quotes then quote else I)
+ |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ else hyper o enclose "\\mbox{\\isa{" "}}"))
+ else error ("Bad " ^ kind ^ " " ^ quote name)
+ end);
fun entity_antiqs check markup kind =
- [(kind, entity check markup NONE kind),
- (kind ^ "_def", entity check markup (SOME true) kind),
- (kind ^ "_ref", entity check markup (SOME false) kind)];
+ [(entity check markup kind NONE),
+ (entity check markup kind (SOME true)),
+ (entity check markup kind (SOME false))];
in
-val _ = ThyOutput.add_commands
- (entity_antiqs no_check "" "syntax" @
- entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command" @
- entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword" @
- entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element" @
- entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
- entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
- entity_antiqs no_check "" "fact" @
- entity_antiqs no_check "" "variable" @
- entity_antiqs no_check "" "case" @
- entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
- entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
- entity_antiqs no_check "" "inference" @
- entity_antiqs no_check "isatt" "executable" @
- entity_antiqs (K check_tool) "isatt" "tool" @
- entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @
- entity_antiqs (K ThyInfo.known_thy) "" "theory");
+val _ = entity_antiqs no_check "" "syntax";
+val _ = entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command";
+val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword";
+val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element";
+val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
+val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
+val _ = entity_antiqs no_check "" "fact";
+val _ = entity_antiqs no_check "" "variable";
+val _ = entity_antiqs no_check "" "case";
+val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
+val _ = entity_antiqs (K ThyOutput.defined_option) "" "antiquotation option";
+val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
+val _ = entity_antiqs no_check "" "inference";
+val _ = entity_antiqs no_check "isatt" "executable";
+val _ = entity_antiqs (K check_tool) "isatt" "tool";
+val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
+val _ = entity_antiqs (K ThyInfo.known_thy) "" "theory";
end;
--- a/doc-src/more_antiquote.ML Mon Mar 09 23:07:41 2009 +0100
+++ b/doc-src/more_antiquote.ML Mon Mar 09 23:07:51 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: Doc/more_antiquote.ML
+(* Title: doc-src/more_antiquote.ML
Author: Florian Haftmann, TU Muenchen
More antiquotations.
@@ -12,15 +12,13 @@
structure More_Antiquote : MORE_ANTIQUOTE =
struct
-structure O = ThyOutput;
-
(* printing typewriter lines *)
fun typewriter s =
let
val parse = Scan.repeat
(Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
- || (Scan.this_string " "
+ || (Scan.this_string " "
|| Scan.this_string "."
|| Scan.this_string ","
|| Scan.this_string ":"
@@ -66,9 +64,8 @@
in
-val _ = O.add_commands
- [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)),
- ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))]
+val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
+val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
end;
@@ -96,12 +93,12 @@
val thms = Code_Wellsorted.eqns funcgr const
|> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
|> map (holize o no_vars ctxt o AxClass.overload thy);
- in ThyOutput.output_list pretty_thm src ctxt thms end;
+ in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
in
-val _ = O.add_commands
- [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
+val _ = ThyOutput.antiquotation "code_thms" Args.term
+ (fn {source, context, ...} => pretty_code_thm source context);
end;
@@ -120,21 +117,20 @@
>> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes);
val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name))
>> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts);
- val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
-
- fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) =
- Code_Target.code_of (ProofContext.theory_of ctxt)
- target "Example" (mk_cs (ProofContext.theory_of ctxt))
- (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
- |> typewriter;
+ val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
in
-val _ = O.add_commands
- [("code_stmts", O.args
- (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
- code_stmts)]
-
-end
+val _ = ThyOutput.antiquotation "code_stmts"
+ (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
+ (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
+ let val thy = ProofContext.theory_of ctxt in
+ Code_Target.code_of thy
+ target "Example" (mk_cs thy)
+ (fn naming => maps (fn f => f thy naming) mk_stmtss)
+ |> typewriter
+ end);
end;
+
+end;
--- a/src/HOL/Docs/Main_Doc.thy Mon Mar 09 23:07:41 2009 +0100
+++ b/src/HOL/Docs/Main_Doc.thy Mon Mar 09 23:07:51 2009 +0100
@@ -9,8 +9,10 @@
else error "term_type_only: type mismatch";
Syntax.pretty_typ ctxt T)
-val _ = ThyOutput.add_commands
- [("term_type_only", ThyOutput.args (Args.term -- Args.typ_abbrev) (ThyOutput.output pretty_term_type_only))];
+val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
+ (fn {source, context, ...} => fn arg =>
+ ThyOutput.output
+ (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg]));
*}
(*>*)
text{*
--- a/src/HOL/IsaMakefile Mon Mar 09 23:07:41 2009 +0100
+++ b/src/HOL/IsaMakefile Mon Mar 09 23:07:51 2009 +0100
@@ -15,6 +15,7 @@
HOL-Auth \
HOL-Bali \
HOL-Decision_Procs \
+ HOL-Docs \
HOL-Extraction \
HOL-HahnBanach \
HOL-Hoare \
@@ -683,6 +684,15 @@
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
+## HOL-Docs
+
+HOL-Docs: HOL $(LOG)/HOL-Docs.gz
+
+$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \
+ Docs/document/root.tex
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Docs
+
+
## HOL-Lambda
HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
--- a/src/HOL/Tools/datatype_package.ML Mon Mar 09 23:07:41 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Mon Mar 09 23:07:51 2009 +0100
@@ -628,38 +628,6 @@
val add_datatype_cmd = gen_add_datatype read_typ true;
-(** a datatype antiquotation **)
-
-fun args_datatype (ctxt, args) =
- let
- val (tyco, (ctxt', args')) = Args.tyname (ctxt, args);
- val thy = Context.theory_of ctxt';
- val spec = the_datatype_spec thy tyco;
- in ((tyco, spec), (ctxt', args')) end;
-
-fun pretty_datatype ctxt (dtco, (vs, cos)) =
- let
- val ty = Type (dtco, map TFree vs);
- fun pretty_typ_br ty =
- let
- val p = Syntax.pretty_typ ctxt ty;
- val s = explode (Pretty.str_of p);
- in if member (op =) s " " then Pretty.enclose "(" ")" [p]
- else p
- end;
- fun pretty_constr (co, tys) =
- (Pretty.block o Pretty.breaks)
- (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- map pretty_typ_br tys);
- in
- Pretty.block
- (Pretty.command "datatype" :: Pretty.brk 1 ::
- Syntax.pretty_typ ctxt ty ::
- Pretty.str " =" :: Pretty.brk 1 ::
- flat (separate [Pretty.brk 1, Pretty.str "| "]
- (map (single o pretty_constr) cos)))
- end
-
(** package setup **)
@@ -698,11 +666,34 @@
>> (fn (alt_names, ts) => Toplevel.print
o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
-val _ =
- ThyOutput.add_commands [("datatype",
- ThyOutput.args args_datatype (ThyOutput.output pretty_datatype))];
+end;
+
+
+(* document antiquotation *)
+
+val _ = ThyOutput.antiquotation "datatype" Args.tyname
+ (fn {source = src, context = ctxt, ...} => fn dtco =>
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (vs, cos) = the_datatype_spec thy dtco;
+ val ty = Type (dtco, map TFree vs);
+ fun pretty_typ_br ty =
+ let
+ val p = Syntax.pretty_typ ctxt ty;
+ val s = explode (Pretty.str_of p); (* FIXME do not inspect pretty output! *)
+ in if member (op =) s " " then Pretty.enclose "(" ")" [p] else p end;
+ fun pretty_constr (co, tys) =
+ (Pretty.block o Pretty.breaks)
+ (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
+ map pretty_typ_br tys);
+ val pretty_datatype =
+ Pretty.block
+ (Pretty.command "datatype" :: Pretty.brk 1 ::
+ Syntax.pretty_typ ctxt ty ::
+ Pretty.str " =" :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, Pretty.str "| "]
+ (map (single o pretty_constr) cos)));
+ in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
end;
-end;
-
--- a/src/HOL/ex/predicate_compile.ML Mon Mar 09 23:07:41 2009 +0100
+++ b/src/HOL/ex/predicate_compile.ML Mon Mar 09 23:07:51 2009 +0100
@@ -639,8 +639,8 @@
in
map_function_intros (Symtab.update_new (mode_id, introthm)) thy
|> map_function_elims (Symtab.update_new (mode_id, elimthm))
- |> PureThy.store_thm (Binding.name (NameSpace.base_name mode_id ^ "I"), introthm) |> snd
- |> PureThy.store_thm (Binding.name (NameSpace.base_name mode_id ^ "E"), elimthm) |> snd
+ |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "I"), introthm) |> snd
+ |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "E"), elimthm) |> snd
end;
fun create_definitions preds nparams (name, modes) thy =
@@ -673,12 +673,12 @@
in mk_split_lambda' xs t end;
val predterm = mk_Enum (mk_split_lambda xouts (list_comb (Const (name, T), xparams' @ xargs)))
val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (mk_tupleT Us2))
- val mode_id = Sign.full_bname thy (NameSpace.base_name mode_id)
+ val mode_id = Sign.full_bname thy (Long_Name.base_name mode_id)
val lhs = list_comb (Const (mode_id, funT), xparams @ xins)
val def = Logic.mk_equals (lhs, predterm)
val ([defthm], thy') = thy |>
- Sign.add_consts_i [(Binding.name (NameSpace.base_name mode_id), funT, NoSyn)] |>
- PureThy.add_defs false [((Binding.name (NameSpace.base_name mode_id ^ "_def"), def), [])]
+ Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_id), funT, NoSyn)] |>
+ PureThy.add_defs false [((Binding.name (Long_Name.base_name mode_id ^ "_def"), def), [])]
in thy' |> map_names (PredModetab.update_new ((name, mode), mode_id))
|> map_function_defs (Symtab.update_new (mode_id, defthm))
|> create_intro_rule nparams mode defthm mode_id funT (Const (name, T))
@@ -1304,7 +1304,7 @@
val _ = tracing "starting proof"
val result_thms = prove_preds thy''' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
val (_, thy'''') = yield_singleton PureThy.add_thmss
- ((Binding.name (NameSpace.base_name ind_name ^ "_codegen" (*FIXME other suffix*)), result_thms),
+ ((Binding.name (Long_Name.base_name ind_name ^ "_codegen" (*FIXME other suffix*)), result_thms),
[Attrib.attribute_i thy''' Code.add_default_eqn_attrib]) thy'''
in
thy''''
--- a/src/Pure/Isar/toplevel.ML Mon Mar 09 23:07:41 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Mar 09 23:07:51 2009 +0100
@@ -22,7 +22,7 @@
val previous_node_of: state -> node option
val node_of: state -> node
val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
- val presentation_context_of: state -> xstring option -> Proof.context
+ val presentation_context_of: state -> Proof.context
val context_of: state -> Proof.context
val generic_theory_of: state -> generic_theory
val theory_of: state -> theory
@@ -180,12 +180,11 @@
fun node_case f g state = cases_node f g (node_of state);
-fun presentation_context_of state opt_loc =
- (case (try node_of state, opt_loc) of
- (SOME (Theory (_, SOME ctxt)), NONE) => ctxt
- | (SOME node, NONE) => context_node node
- | (SOME node, SOME loc) => loc_init loc (cases_node Context.theory_of Proof.theory_of node)
- | (NONE, _) => raise UNDEF);
+fun presentation_context_of state =
+ (case try node_of state of
+ SOME (Theory (_, SOME ctxt)) => ctxt
+ | SOME node => context_node node
+ | NONE => raise UNDEF);
val context_of = node_case Context.proof_of Proof.context_of;
val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
@@ -742,13 +741,13 @@
=> State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
|> fold_map command_result body_trs
||> command (end_tr |> set_print false);
- in (states, presentation_context_of result_state NONE) end))
+ in (states, presentation_context_of result_state) end))
#> (fn (states, ctxt) => States.put (SOME states) ctxt);
val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
val states =
- (case States.get (presentation_context_of st'' NONE) of
+ (case States.get (presentation_context_of st'') of
NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
| SOME states => states);
val result = Lazy.lazy
--- a/src/Pure/Thy/thy_output.ML Mon Mar 09 23:07:41 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Mar 09 23:07:51 2009 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/Thy/thy_output.ML
Author: Markus Wenzel, TU Muenchen
-Theory document output.
+Theory document output with antiquotations.
*)
signature THY_OUTPUT =
@@ -18,24 +18,20 @@
val print_antiquotations: unit -> unit
val boolean: string -> bool
val integer: string -> int
- val raw_antiquotation: string -> (Args.src -> Toplevel.state ->
- Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
- val antiquotation: string -> (Args.src -> Proof.context ->
- Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
- val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
- (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
+ val antiquotation: string ->
+ (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
+ ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
datatype markup = Markup | MarkupEnv | Verbatim
val modes: string list ref
val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
- val str_of_source: Args.src -> string
val pretty_text: string -> Pretty.T
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
- val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
- Proof.context -> 'a list -> string
- val output: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string
+ val str_of_source: Args.src -> string
+ val maybe_pretty_source: ('a -> Pretty.T) -> Args.src -> 'a list -> Pretty.T list
+ val output: Pretty.T list -> string
end;
structure ThyOutput: THY_OUTPUT =
@@ -47,7 +43,6 @@
(** global options **)
-val locale = ref "";
val display = ref false;
val quotes = ref false;
val indent = ref 0;
@@ -56,7 +51,7 @@
-(** maintain global commands **)
+(** maintain global antiquotations **)
local
@@ -108,6 +103,11 @@
end;
+fun antiquotation name scan out = add_commands [(name, fn src => fn state =>
+ let val (x, ctxt) = Args.context_syntax "document antiquotation"
+ scan src (Toplevel.presentation_context_of state)
+ in out {source = src, state = state, context = ctxt} x end)];
+
(** syntax of antiquotations **)
@@ -127,25 +127,6 @@
in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
-(* args syntax *)
-
-fun syntax scan = Args.context_syntax "document antiquotation" scan;
-
-fun raw_antiquotation name scan =
- add_commands [(name, fn src => fn state =>
- #1 (syntax (scan src state) src (Toplevel.presentation_context_of state NONE)))];
-
-fun antiquotation name scan =
- raw_antiquotation name (fn src => fn state =>
- scan src (Toplevel.presentation_context_of state NONE));
-
-fun args scan f src state : string =
- let
- val loc = if ! locale = "" then NONE else SOME (! locale);
- val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state loc);
- in f src ctxt x end;
-
-
(* outer syntax *)
local
@@ -442,7 +423,6 @@
("short_names", Library.setmp NameSpace.short_names o boolean),
("unique_names", Library.setmp NameSpace.unique_names o boolean),
("eta_contract", Library.setmp Syntax.eta_contract o boolean),
- ("locale", Library.setmp locale),
("display", Library.setmp display o boolean),
("break", Library.setmp break o boolean),
("quotes", Library.setmp quotes o boolean),
@@ -455,8 +435,6 @@
(* basic pretty printing *)
-val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
-
fun tweak_line s =
if ! display then s else Symbol.strip_blanks s;
@@ -497,18 +475,22 @@
fun pretty_thm_style ctxt (name, th) =
pretty_term_style ctxt (name, Thm.full_prop_of th);
-fun pretty_prf full ctxt thms =
- Pretty.chunks (map (ProofSyntax.pretty_proof_of ctxt full) thms);
+fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
fun pretty_theory ctxt name =
(Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
-(* Isar output *)
+(* default output *)
+
+val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
-fun output_list pretty src ctxt xs =
- map (pretty ctxt) xs (*always pretty in order to exhibit errors!*)
- |> (if ! source then K [pretty_text (str_of_source src)] else I)
+fun maybe_pretty_source pretty src xs =
+ map pretty xs (*always pretty in order to exhibit errors!*)
+ |> (if ! source then K [pretty_text (str_of_source src)] else I);
+
+fun output prts =
+ prts
|> (if ! quotes then map Pretty.quote else I)
|> (if ! display then
map (Output.output o Pretty.string_of o Pretty.indent (! indent))
@@ -519,69 +501,99 @@
#> space_implode "\\isasep\\isanewline%\n"
#> enclose "\\isa{" "}");
-fun output pretty src ctxt = output_list pretty src ctxt o single;
+
+
+(** concrete antiquotations **)
+
+(* basic entities *)
+
+local
+
+fun basic_entities name scan pretty = antiquotation name scan
+ (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
+
+fun basic_entity name scan = basic_entities name (scan >> single);
+
+in
+
+val _ = basic_entities "thm" Attrib.thms pretty_thm;
+val _ = basic_entity "thm_style" (Scan.lift Args.liberal_name -- Attrib.thm) pretty_thm_style;
+val _ = basic_entity "prop" Args.prop pretty_term;
+val _ = basic_entity "term" Args.term pretty_term;
+val _ = basic_entity "term_style" (Scan.lift Args.liberal_name -- Args.term) pretty_term_style;
+val _ = basic_entity "term_type" Args.term pretty_term_typ;
+val _ = basic_entity "typeof" Args.term pretty_term_typeof;
+val _ = basic_entity "const" Args.const_proper pretty_const;
+val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
+val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
+val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);
+val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
+val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
+val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
+
+end;
+
+
+(* goal state *)
+
+local
fun proof_state state =
(case try Toplevel.proof_of state of
SOME prf => prf
| _ => error "No proof state");
-fun output_goals main_goal src state = args (Scan.succeed ()) (output (fn _ => fn _ =>
- Pretty.chunks (Proof.pretty_goals main_goal (proof_state state)))) src state;
-
-fun ml_val txt = "fn _ => (" ^ txt ^ ");";
-fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
-fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
+fun goal_state name main_goal = antiquotation name (Scan.succeed ())
+ (fn {state, ...} => fn () => output
+ [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
-fun output_ml ml _ ctxt (txt, pos) =
- (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
- SymbolPos.content (SymbolPos.explode (txt, pos))
- |> (if ! quotes then quote else I)
- |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
- else
- split_lines
- #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
- #> space_implode "\\isasep\\isanewline%\n"));
+in
+
+val _ = goal_state "goals" true;
+val _ = goal_state "subgoals" false;
+
+end;
-(* embedded lemmas *)
-
-fun pretty_lemma ctxt (prop, methods) =
- let
- val _ = ctxt
- |> Proof.theorem_i NONE (K I) [[(prop, [])]]
- |> Proof.global_terminal_proof methods;
- in pretty_term ctxt prop end;
-
-val embedded_lemma =
- args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
- (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
-
-
-(* commands *)
+(* embedded lemma *)
val _ = OuterKeyword.keyword "by";
-val _ = add_commands
- [("thm", args Attrib.thms (output_list pretty_thm)),
- ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
- ("prop", args Args.prop (output pretty_term)),
- ("lemma", embedded_lemma),
- ("term", args Args.term (output pretty_term)),
- ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
- ("term_type", args Args.term (output pretty_term_typ)),
- ("typeof", args Args.term (output pretty_term_typeof)),
- ("const", args Args.const_proper (output pretty_const)),
- ("abbrev", args (Scan.lift Args.name_source) (output pretty_abbrev)),
- ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
- ("text", args (Scan.lift Args.name) (output (K pretty_text))),
- ("goals", output_goals true),
- ("subgoals", output_goals false),
- ("prf", args Attrib.thms (output (pretty_prf false))),
- ("full_prf", args Attrib.thms (output (pretty_prf true))),
- ("theory", args (Scan.lift Args.name) (output pretty_theory)),
- ("ML", args (Scan.lift Args.name_source_position) (output_ml ml_val)),
- ("ML_type", args (Scan.lift Args.name_source_position) (output_ml ml_type)),
- ("ML_struct", args (Scan.lift Args.name_source_position) (output_ml ml_struct))];
+val _ = antiquotation "lemma"
+ (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
+ (fn {source, context, ...} => fn (prop, methods) =>
+ let
+ val prop_src =
+ (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
+ val _ = context
+ |> Proof.theorem_i NONE (K I) [[(prop, [])]]
+ |> Proof.global_terminal_proof methods;
+ in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
+
+
+(* ML text *)
+
+local
+
+fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
+ (fn {context, ...} => fn (txt, pos) =>
+ (ML_Context.eval_in (SOME context) false pos (ml txt);
+ SymbolPos.content (SymbolPos.explode (txt, pos))
+ |> (if ! quotes then quote else I)
+ |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+ else
+ split_lines
+ #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
+ #> space_implode "\\isasep\\isanewline%\n")));
+
+in
+
+val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
+val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
+val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
+val _ = ml_text "ML_functor" (K ""); (*no check!*)
+val _ = ml_text "ML_text" (K "");
end;
+
+end;