--- a/src/Doc/Implementation/Integration.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Implementation/Integration.thy Thu Oct 22 21:16:49 2015 +0200
@@ -121,7 +121,7 @@
\<^descr> @{ML Toplevel.theory_to_proof}~\<open>tr\<close> adjoins a global
goal function, which turns a theory into a proof state. The theory
may be changed before entering the proof; the generic Isar goal
- setup includes an @{verbatim after_qed} argument that specifies how to
+ setup includes an \<^verbatim>\<open>after_qed\<close> argument that specifies how to
apply the proven result to the enclosing context, when the proof
is finished.
--- a/src/Doc/Implementation/Logic.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy Thu Oct 22 21:16:49 2015 +0200
@@ -636,11 +636,10 @@
\<^descr> @{ML Thm.peek_status}~\<open>thm\<close> informs about the current
status of the derivation object behind the given theorem. This is a
snapshot of a potentially ongoing (parallel) evaluation of proofs.
- The three Boolean values indicate the following: @{verbatim oracle}
- if the finished part contains some oracle invocation; @{verbatim
- unfinished} if some future proofs are still pending; @{verbatim
- failed} if some future proof has failed, rendering the theorem
- invalid!
+ The three Boolean values indicate the following: \<^verbatim>\<open>oracle\<close>
+ if the finished part contains some oracle invocation; \<^verbatim>\<open>unfinished\<close>
+ if some future proofs are still pending; \<^verbatim>\<open>failed\<close> if some future
+ proof has failed, rendering the theorem invalid!
\<^descr> @{ML Logic.all}~\<open>a B\<close> produces a Pure quantification
\<open>\<And>a. B\<close>, where occurrences of the atomic term \<open>a\<close> in
@@ -1219,18 +1218,18 @@
\begin{center}
\begin{supertabular}{rclr}
- @{syntax_def (inner) proof} & = & @{verbatim Lam} \<open>params\<close> @{verbatim "."} \<open>proof\<close> \\
- & \<open>|\<close> & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> @{verbatim "."} \<open>proof\<close> \\
- & \<open>|\<close> & \<open>proof\<close> @{verbatim "%"} \<open>any\<close> \\
+ @{syntax_def (inner) proof} & = & \<^verbatim>\<open>Lam\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
+ & \<open>|\<close> & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
+ & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%\<close> \<open>any\<close> \\
& \<open>|\<close> & \<open>proof\<close> \<open>\<cdot>\<close> \<open>any\<close> \\
- & \<open>|\<close> & \<open>proof\<close> @{verbatim "%%"} \<open>proof\<close> \\
+ & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%%\<close> \<open>proof\<close> \\
& \<open>|\<close> & \<open>proof\<close> \<open>\<bullet>\<close> \<open>proof\<close> \\
& \<open>|\<close> & \<open>id | longid\<close> \\
\\
\<open>param\<close> & = & \<open>idt\<close> \\
- & \<open>|\<close> & \<open>idt\<close> @{verbatim ":"} \<open>prop\<close> \\
- & \<open>|\<close> & @{verbatim "("} \<open>param\<close> @{verbatim ")"} \\
+ & \<open>|\<close> & \<open>idt\<close> \<^verbatim>\<open>:\<close> \<open>prop\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>(\<close> \<open>param\<close> \<^verbatim>\<open>)\<close> \\
\\
\<open>params\<close> & = & \<open>param\<close> \\
--- a/src/Doc/Implementation/ML.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Implementation/ML.thy Thu Oct 22 21:16:49 2015 +0200
@@ -67,8 +67,8 @@
reaching back to the earliest versions of the system by Larry
Paulson. See @{file "~~/src/Pure/thm.ML"}, for example.
- The header includes at least @{verbatim Title} and @{verbatim
- Author} entries, followed by a prose description of the purpose of
+ The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries,
+ followed by a prose description of the purpose of
the module. The latter can range from a single line to several
paragraphs of explanations.
@@ -263,8 +263,8 @@
explicit, if tactic combinators (tacticals) are used as usual.
A tactic that requires a proof context needs to make that explicit as seen
- in the @{verbatim ctxt} argument above. Do not refer to the background
- theory of @{verbatim st} -- it is not a proper context, but merely a formal
+ in the \<^verbatim>\<open>ctxt\<close> argument above. Do not refer to the background
+ theory of \<^verbatim>\<open>st\<close> -- it is not a proper context, but merely a formal
certificate.
\<close>
@@ -516,8 +516,8 @@
Object-logics like Isabelle/HOL are built within the Isabelle/ML/Isar
environment by introducing suitable theories with associated ML modules,
- either inlined within @{verbatim ".thy"} files, or as separate @{verbatim
- ".ML"} files that are loading from some theory. Thus Isabelle/HOL is defined
+ either inlined within \<^verbatim>\<open>.thy\<close> files, or as separate \<^verbatim>\<open>.ML\<close> files that are
+ loading from some theory. Thus Isabelle/HOL is defined
as a regular user-space application within the Isabelle framework. Further
add-on tools can be implemented in ML within the Isar context in the same
manner: ML is part of the standard repertoire of Isabelle, and there is no
@@ -970,8 +970,8 @@
Depending on the user interface involved, these messages may appear
in different text styles or colours. The standard output for
- batch sessions prefixes each line of warnings by @{verbatim
- "###"} and errors by @{verbatim "***"}, but leaves anything else
+ batch sessions prefixes each line of warnings by \<^verbatim>\<open>###\<close> and errors by
+ \<^verbatim>\<open>***\<close>, but leaves anything else
unchanged. The message body may contain further markup and formatting,
which is routinely used in the Prover IDE @{cite "isabelle-jedit"}.
@@ -1220,28 +1220,26 @@
in itself a small string, which has either one of the following
forms:
- \<^enum> a single ASCII character ``\<open>c\<close>'', for example
- ``@{verbatim a}'',
+ \<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'',
\<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
- \<^enum> a regular symbol ``@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"}'', for example ``@{verbatim "\<alpha>"}'',
-
- \<^enum> a control symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^"}\<open>ident\<close>@{verbatim ">"}'', for example ``@{verbatim "\<^bold>"}'',
-
- \<^enum> a raw symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^raw:"}\<open>text\<close>@{verbatim ">"}'' where \<open>text\<close> consists of printable characters
- excluding ``@{verbatim "."}'' and ``@{verbatim ">"}'', for example
- ``@{verbatim "\<^raw:$\sum_{i = 1}^n$>"}'',
-
- \<^enum> a numbered raw control symbol ``@{verbatim \<open>\\<close>}@{verbatim
- "<^raw"}\<open>n\<close>@{verbatim ">"}, where \<open>n\<close> consists of digits, for
- example ``@{verbatim "\<^raw42>"}''.
+ \<^enum> a regular symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'',
+
+ \<^enum> a control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
+
+ \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of printable characters
+ excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
+ ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
+
+ \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
+ of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
The \<open>ident\<close> syntax for symbol names is \<open>letter
(letter | digit)\<^sup>*\<close>, where \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular symbols and
control symbols, but a fixed collection of standard symbols is
- treated specifically. For example, ``@{verbatim "\<alpha>"}'' is
+ treated specifically. For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is
classified as a letter, which means it may occur within regular
Isabelle identifiers.
@@ -1255,9 +1253,9 @@
\<^medskip>
Output of Isabelle symbols depends on the print mode. For example,
the standard {\LaTeX} setup of the Isabelle document preparation system
- would present ``@{verbatim "\<alpha>"}'' as \<open>\<alpha>\<close>, and ``@{verbatim
- "\<^bold>\<alpha>"}'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering usually works by mapping a
- finite subset of Isabelle symbols to suitable Unicode characters.
+ would present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering
+ usually works by mapping a finite subset of Isabelle symbols to suitable
+ Unicode characters.
\<close>
text %mlref \<open>
@@ -1361,7 +1359,7 @@
with @{ML YXML.parse_body} as key operation.
Note that Isabelle/ML string literals may refer Isabelle symbols like
- ``@{verbatim \<alpha>}'' natively, \<^emph>\<open>without\<close> escaping the backslash. This is a
+ ``\<^verbatim>\<open>\<alpha>\<close>'' natively, \<^emph>\<open>without\<close> escaping the backslash. This is a
consequence of Isabelle treating all source text as strings of symbols,
instead of raw characters.
\<close>
@@ -1382,7 +1380,7 @@
variations of encodings like UTF-8 or UTF-16 pose delicate questions
about the multi-byte representations of its codepoint, which is outside
of the 16-bit address space of the original Unicode standard from
- the 1990-ies. In Isabelle/ML it is just ``@{verbatim \<A>}''
+ the 1990-ies. In Isabelle/ML it is just ``\<^verbatim>\<open>\<A>\<close>''
literally, using plain ASCII characters beyond any doubts.\<close>
@@ -1541,13 +1539,13 @@
Isabelle/ML, following standard conventions for their names and
types.
- Note that a function called @{verbatim lookup} is obliged to express its
+ Note that a function called \<^verbatim>\<open>lookup\<close> is obliged to express its
partiality via an explicit option element. There is no choice to
raise an exception, without changing the name to something like
\<open>the_element\<close> or \<open>get\<close>.
The \<open>defined\<close> operation is essentially a contraction of @{ML
- is_some} and @{verbatim "lookup"}, but this is sufficiently frequent to
+ is_some} and \<^verbatim>\<open>lookup\<close>, but this is sufficiently frequent to
justify its independent existence. This also gives the
implementation some opportunity for peep-hole optimization.
@@ -1842,9 +1840,9 @@
\<^medskip>
An \<^emph>\<open>unevaluated expression\<close> is represented either as
- unit abstraction @{verbatim "fn () => a"} of type
- @{verbatim "unit -> 'a"} or as regular function
- @{verbatim "fn a => b"} of type @{verbatim "'a -> 'b"}. Both forms
+ unit abstraction \<^verbatim>\<open>fn () => a\<close> of type
+ \<^verbatim>\<open>unit -> 'a\<close> or as regular function
+ \<^verbatim>\<open>fn a => b\<close> of type \<^verbatim>\<open>'a -> 'b\<close>. Both forms
occur routinely, and special care is required to tell them apart ---
the static type-system of SML is only of limited help here.
@@ -1908,7 +1906,7 @@
all results are regular values, that list is returned. Otherwise,
the collection of all exceptions is raised, wrapped-up as collective
parallel exception. Note that the latter prevents access to
- individual exceptions by conventional @{verbatim "handle"} of ML.
+ individual exceptions by conventional \<^verbatim>\<open>handle\<close> of ML.
\<^descr> @{ML Par_Exn.release_first} is similar to @{ML
Par_Exn.release_all}, but only the first (meaningful) exception that has
@@ -2010,8 +2008,7 @@
@{index_ML Lazy.force: "'a lazy -> 'a"} \\
\end{mldecls}
- \<^descr> Type @{ML_type "'a lazy"} represents lazy values over type @{verbatim
- "'a"}.
+ \<^descr> Type @{ML_type "'a lazy"} represents lazy values over type \<^verbatim>\<open>'a\<close>.
\<^descr> @{ML Lazy.lazy}~\<open>(fn () => e)\<close> wraps the unevaluated
expression \<open>e\<close> as unfinished lazy value.
@@ -2099,8 +2096,7 @@
@{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\
\end{mldecls}
- \<^descr> Type @{ML_type "'a future"} represents future values over type
- @{verbatim "'a"}.
+ \<^descr> Type @{ML_type "'a future"} represents future values over type \<^verbatim>\<open>'a\<close>.
\<^descr> @{ML Future.fork}~\<open>(fn () => e)\<close> registers the unevaluated
expression \<open>e\<close> as unfinished future value, to be evaluated eventually
--- a/src/Doc/Implementation/Prelim.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy Thu Oct 22 21:16:49 2015 +0200
@@ -576,7 +576,7 @@
``\<open>Foo.bar.baz\<close>'' is considered as a long name consisting of
qualifier \<open>Foo.bar\<close> and base name \<open>baz\<close>. The
individual constituents of a name may have further substructure,
- e.g.\ the string ``@{verbatim \<alpha>}'' encodes as a single
+ e.g.\ the string ``\<^verbatim>\<open>\<alpha>\<close>'' encodes as a single
symbol (\secref{sec:symbols}).
\<^medskip>
--- a/src/Doc/Implementation/Tactic.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Implementation/Tactic.thy Thu Oct 22 21:16:49 2015 +0200
@@ -517,8 +517,8 @@
subsection \<open>Combining tactics\<close>
text \<open>Sequential composition and alternative choices are the most
- basic ways to combine tactics, similarly to ``@{verbatim ","}'' and
- ``@{verbatim "|"}'' in Isar method notation. This corresponds to
+ basic ways to combine tactics, similarly to ``\<^verbatim>\<open>,\<close>'' and
+ ``\<^verbatim>\<open>|\<close>'' in Isar method notation. This corresponds to
@{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further
possibilities for fine-tuning alternation of tactics such as @{ML_op
"APPEND"}. Further details become visible in ML due to explicit
@@ -577,8 +577,8 @@
subsection \<open>Repetition tacticals\<close>
text \<open>These tacticals provide further control over repetition of
- tactics, beyond the stylized forms of ``@{verbatim "?"}'' and
- ``@{verbatim "+"}'' in Isar method expressions.\<close>
+ tactics, beyond the stylized forms of ``\<^verbatim>\<open>?\<close>'' and
+ ``\<^verbatim>\<open>+\<close>'' in Isar method expressions.\<close>
text %mlref \<open>
\begin{mldecls}
@@ -595,7 +595,8 @@
once.
Note that for tactics with subgoal addressing, the combinator can be
- applied via functional composition: @{ML "TRY"}~@{ML_op o}~\<open>tac\<close>. There is no need for @{verbatim TRY'}.
+ applied via functional composition: @{ML "TRY"}~@{ML_op o}~\<open>tac\<close>.
+ There is no need for \<^verbatim>\<open>TRY'\<close>.
\<^descr> @{ML REPEAT}~\<open>tac\<close> applies \<open>tac\<close> to the goal
state and, recursively, to each element of the resulting sequence.
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Oct 22 21:16:49 2015 +0200
@@ -53,13 +53,11 @@
\<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark
section headings within the theory source. This works in any context, even
before the initial @{command theory} command. The corresponding {\LaTeX}
- macros are @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim
- \<open>\isamarkupsection\<close>}, @{verbatim \<open>\isamarkupsubsection\<close>} etc.\
+ macros are \<^verbatim>\<open>\isamarkupchapter\<close>, \<^verbatim>\<open>\isamarkupsection\<close>, \<^verbatim>\<open>\isamarkupsubsection\<close> etc.\
\<^descr> @{command text} and @{command txt} specify paragraphs of plain text.
- This corresponds to a {\LaTeX} environment @{verbatim
- \<open>\begin{isamarkuptext}\<close>} \<open>\<dots>\<close> @{verbatim \<open>\end{isamarkuptext}\<close>}
- etc.
+ This corresponds to a {\LaTeX} environment \<^verbatim>\<open>\begin{isamarkuptext}\<close> \<open>\<dots>\<close>
+ \<^verbatim>\<open>\end{isamarkuptext}\<close> etc.
\<^descr> @{command text_raw} is similar to @{command text}, but without
any surrounding markup environment. This allows to inject arbitrary
@@ -120,7 +118,7 @@
in the resulting document, but may again refer to formal entities
via \<^emph>\<open>document antiquotations\<close>.
- For example, embedding @{verbatim \<open>@{term [show_types] "f x = a + x"}\<close>}
+ For example, embedding \<^verbatim>\<open>@{term [show_types] "f x = a + x"}\<close>
within a text block makes
\isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} appear in the final {\LaTeX} document.
@@ -131,15 +129,14 @@
antiquotations are checked within the current theory or proof
context.
- \<^medskip> Antiquotations are in general written as @{verbatim "@{"}\<open>name\<close>~@{verbatim "["}\<open>options\<close>@{verbatim "]"}~\<open>arguments\<close>@{verbatim "}"}. The short form @{verbatim \<open>\\<close>}@{verbatim
- "<^"}\<open>name\<close>@{verbatim ">"}\<open>\<open>argument_content\<close>\<close> (without
- surrounding @{verbatim "@{"}\<open>\<dots>\<close>@{verbatim "}"}) works for a single
+ \<^medskip> Antiquotations are in general written as \<^verbatim>\<open>@{\<close>\<open>name\<close>~\<^verbatim>\<open>[\<close>\<open>options\<close>\<^verbatim>\<open>]\<close>~\<open>arguments\<close>\<^verbatim>\<open>}\<close>.
+ The short form \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>name\<close>\<^verbatim>\<open>>\<close>\<open>\<open>argument_content\<close>\<close> (without
+ surrounding \<^verbatim>\<open>@{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>) works for a single
argument that is a cartouche.
Omitting the control symbol is also possible: a cartouche without special
- decoration is equivalent to @{verbatim \<open>\\<close>}@{verbatim
- "<^cartouche>"}\<open>\<open>argument_content\<close>\<close>, which is equivalent to
- @{verbatim "@{cartouche"}~\<open>\<open>argument_content\<close>\<close>@{verbatim "}"}. The
+ decoration is equivalent to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
+ is equivalent to \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The
special name @{antiquotation_def cartouche} is defined in the context:
Isabelle/Pure introduces that as an alias to @{antiquotation_ref text}
(see below). Consequently, \<open>\<open>foo_bar + baz \<le> bazar\<close>\<close> prints literal
@@ -161,8 +158,7 @@
\endgroup
Note that the syntax of antiquotations may \<^emph>\<open>not\<close> include source
- comments @{verbatim "(*"}~\<open>\<dots>\<close>~@{verbatim "*)"} nor verbatim
- text @{verbatim "{*"}~\<open>\<dots>\<close>~@{verbatim "*}"}.
+ comments \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> nor verbatim text \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>.
%% FIXME less monolithic presentation, move to individual sections!?
@{rail \<open>
@@ -280,10 +276,10 @@
and functor respectively. The source is printed verbatim.
\<^descr> \<open>@{emph s}\<close> prints document source recursively, with {\LaTeX}
- markup @{verbatim \<open>\emph{\<close>}\<open>\<dots>\<close>@{verbatim \<open>}\<close>}.
+ markup \<^verbatim>\<open>\emph{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>.
\<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX}
- markup @{verbatim \<open>\textbf{\<close>}\<open>\<dots>\<close>@{verbatim \<open>}\<close>}.
+ markup \<^verbatim>\<open>\textbf{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>.
\<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally
as ASCII characters, using some type-writer font style.
@@ -298,19 +294,18 @@
\<^descr> \<open>@{url name}\<close> produces markup for the given URL, which
results in an active hyperlink within the text.
- \<^descr> \<open>@{cite name}\<close> produces a citation @{verbatim
- \<open>\cite{name}\<close>} in {\LaTeX}, where the name refers to some Bib{\TeX}
- database entry.
+ \<^descr> \<open>@{cite name}\<close> produces a citation \<^verbatim>\<open>\cite{name}\<close> in {\LaTeX},
+ where the name refers to some Bib{\TeX} database entry.
- The variant \<open>@{cite \<open>opt\<close> name}\<close> produces @{verbatim
- \<open>\cite[opt]{name}\<close>} with some free-form optional argument. Multiple names
+ The variant \<open>@{cite \<open>opt\<close> name}\<close> produces \<^verbatim>\<open>\cite[opt]{name}\<close> with
+ some free-form optional argument. Multiple names
are output with commas, e.g. \<open>@{cite foo \<AND> bar}\<close> becomes
- @{verbatim \<open>\cite{foo,bar}\<close>}.
+ \<^verbatim>\<open>\cite{foo,bar}\<close>.
The {\LaTeX} macro name is determined by the antiquotation option
@{antiquotation_option_def cite_macro}, or the configuration option
@{attribute cite_macro} in the context. For example, \<open>@{cite
- [cite_macro = nocite] foobar}\<close> produces @{verbatim \<open>\nocite{foobar}\<close>}.
+ [cite_macro = nocite] foobar}\<close> produces \<^verbatim>\<open>\nocite{foobar}\<close>.
\<^descr> @{command "print_antiquotations"} prints all document antiquotations
that are defined in the current context; the ``\<open>!\<close>'' option
@@ -422,7 +417,7 @@
For Boolean flags, ``\<open>name = true\<close>'' may be abbreviated as
``\<open>name\<close>''. All of the above flags are disabled by default,
unless changed specifically for a logic session in the corresponding
- @{verbatim "ROOT"} file.
+ \<^verbatim>\<open>ROOT\<close> file.
\<close>
@@ -494,8 +489,7 @@
The @{antiquotation rail} antiquotation allows to include syntax
diagrams into Isabelle documents. {\LaTeX} requires the style file
@{file "~~/lib/texinputs/railsetup.sty"}, which can be used via
- @{verbatim \<open>\usepackage{railsetup}\<close>} in @{verbatim "root.tex"}, for
- example.
+ \<^verbatim>\<open>\usepackage{railsetup}\<close> in \<^verbatim>\<open>root.tex\<close>, for example.
The rail specification language is quoted here as Isabelle @{syntax
string} or text @{syntax "cartouche"}; it has its own grammar given
@@ -528,62 +522,59 @@
recursion. The meaning and visual appearance of these rail language
elements is illustrated by the following representative examples.
- \<^item> Empty @{verbatim "()"}
+ \<^item> Empty \<^verbatim>\<open>()\<close>
@{rail \<open>()\<close>}
- \<^item> Nonterminal @{verbatim "A"}
+ \<^item> Nonterminal \<^verbatim>\<open>A\<close>
@{rail \<open>A\<close>}
- \<^item> Nonterminal via Isabelle antiquotation
- @{verbatim "@{syntax method}"}
+ \<^item> Nonterminal via Isabelle antiquotation \<^verbatim>\<open>@{syntax method}\<close>
@{rail \<open>@{syntax method}\<close>}
- \<^item> Terminal @{verbatim "'xyz'"}
+ \<^item> Terminal \<^verbatim>\<open>'xyz'\<close>
@{rail \<open>'xyz'\<close>}
- \<^item> Terminal in keyword style @{verbatim "@'xyz'"}
+ \<^item> Terminal in keyword style \<^verbatim>\<open>@'xyz'\<close>
@{rail \<open>@'xyz'\<close>}
- \<^item> Terminal via Isabelle antiquotation
- @{verbatim "@@{method rule}"}
+ \<^item> Terminal via Isabelle antiquotation \<^verbatim>\<open>@@{method rule}\<close>
@{rail \<open>@@{method rule}\<close>}
- \<^item> Concatenation @{verbatim "A B C"}
+ \<^item> Concatenation \<^verbatim>\<open>A B C\<close>
@{rail \<open>A B C\<close>}
- \<^item> Newline inside concatenation
- @{verbatim "A B C \<newline> D E F"}
+ \<^item> Newline inside concatenation \<^verbatim>\<open>A B C \<newline> D E F\<close>
@{rail \<open>A B C \<newline> D E F\<close>}
- \<^item> Variants @{verbatim "A | B | C"}
+ \<^item> Variants \<^verbatim>\<open>A | B | C\<close>
@{rail \<open>A | B | C\<close>}
- \<^item> Option @{verbatim "A ?"}
+ \<^item> Option \<^verbatim>\<open>A ?\<close>
@{rail \<open>A ?\<close>}
- \<^item> Repetition @{verbatim "A *"}
+ \<^item> Repetition \<^verbatim>\<open>A *\<close>
@{rail \<open>A *\<close>}
- \<^item> Repetition with separator @{verbatim "A * sep"}
+ \<^item> Repetition with separator \<^verbatim>\<open>A * sep\<close>
@{rail \<open>A * sep\<close>}
- \<^item> Strict repetition @{verbatim "A +"}
+ \<^item> Strict repetition \<^verbatim>\<open>A +\<close>
@{rail \<open>A +\<close>}
- \<^item> Strict repetition with separator @{verbatim "A + sep"}
+ \<^item> Strict repetition with separator \<^verbatim>\<open>A + sep\<close>
@{rail \<open>A + sep\<close>}
\<close>
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Oct 22 21:16:49 2015 +0200
@@ -2469,9 +2469,9 @@
hierarchy. Omitting the file specification denotes standard output.
Serializers take an optional list of arguments in parentheses. For
- \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' argument; ``\<open>string_classes\<close>'' adds a ``@{verbatim
- "deriving (Read, Show)"}'' clause to each appropriate datatype
- declaration.
+ \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' argument;
+ ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause to each
+ appropriate datatype declaration.
\<^descr> @{attribute (HOL) code} declare code equations for code generation.
Variant \<open>code equation\<close> declares a conventional equation as code
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Oct 22 21:16:49 2015 +0200
@@ -8,8 +8,8 @@
the main entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type classes. Applications may either
extend existing syntactic categories by additional notation, or
define new sub-languages that are linked to the standard term
- language via some explicit markers. For example @{verbatim
- FOO}~\<open>foo\<close> could embed the syntax corresponding for some
+ language via some explicit markers. For example \<^verbatim>\<open>FOO\<close>~\<open>foo\<close> could
+ embed the syntax corresponding for some
user-defined nonterminal \<open>foo\<close> --- within the bounds of the
given lexical syntax of Isabelle/Pure.
@@ -267,24 +267,20 @@
Mode names can be arbitrary, but the following ones have a specific
meaning by convention:
- \<^item> @{verbatim \<open>""\<close>} (the empty string): default mode;
+ \<^item> \<^verbatim>\<open>""\<close> (the empty string): default mode;
implicitly active as last element in the list of modes.
- \<^item> @{verbatim input}: dummy print mode that is never active; may
+ \<^item> \<^verbatim>\<open>input\<close>: dummy print mode that is never active; may
be used to specify notation that is only available for input.
- \<^item> @{verbatim internal} dummy print mode that is never active;
+ \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active;
used internally in Isabelle/Pure.
- \<^item> @{verbatim xsymbols}: enable proper mathematical symbols
+ \<^item> \<^verbatim>\<open>xsymbols\<close>: enable proper mathematical symbols
instead of ASCII art.\footnote{This traditional mode name stems from
the ``X-Symbol'' package for classic Proof~General with XEmacs.}
- \<^item> @{verbatim HTML}: additional mode that is active in HTML
- presentation of Isabelle theory sources; allows to provide
- alternative output notation.
-
- \<^item> @{verbatim latex}: additional mode that is active in {\LaTeX}
+ \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX}
document preparation of Isabelle theory sources; allows to provide
alternative output notation.
\<close>
@@ -318,7 +314,7 @@
The string given as \<open>template\<close> may include literal text,
spacing, blocks, and arguments (denoted by ``\<open>_\<close>''); the
- special symbol ``@{verbatim "\<index>"}'' (printed as ``\<open>\<index>\<close>'')
+ special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as ``\<open>\<index>\<close>'')
represents an index argument that specifies an implicit @{keyword
"structure"} reference (see also \secref{sec:locale}). Only locally
fixed variables may be declared as @{keyword "structure"}.
@@ -326,7 +322,8 @@
Infix and binder declarations provide common abbreviations for
particular mixfix declarations. So in practice, mixfix templates
mostly degenerate to literal text for concrete syntax, such as
- ``@{verbatim "++"}'' for an infix symbol.\<close>
+ ``\<^verbatim>\<open>++\<close>'' for an infix symbol.
+\<close>
subsection \<open>The general mixfix form\<close>
@@ -364,16 +361,16 @@
\<^medskip>
\begin{tabular}{ll}
- @{verbatim "'"} & single quote \\
- @{verbatim "_"} & underscore \\
+ \<^verbatim>\<open>'\<close> & single quote \\
+ \<^verbatim>\<open>_\<close> & underscore \\
\<open>\<index>\<close> & index symbol \\
- @{verbatim "("} & open parenthesis \\
- @{verbatim ")"} & close parenthesis \\
- @{verbatim "/"} & slash \\
+ \<^verbatim>\<open>(\<close> & open parenthesis \\
+ \<^verbatim>\<open>)\<close> & close parenthesis \\
+ \<^verbatim>\<open>/\<close> & slash \\
\end{tabular}
\<^medskip>
- \<^descr> @{verbatim "'"} escapes the special meaning of these
+ \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these
meta-characters, producing a literal version of the following
character, unless that is a blank.
@@ -381,7 +378,7 @@
affecting printing, but input tokens may have additional white space
here.
- \<^descr> @{verbatim "_"} is an argument position, which stands for a
+ \<^descr> \<^verbatim>\<open>_\<close> is an argument position, which stands for a
certain syntactic category in the underlying grammar.
\<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place
@@ -390,17 +387,17 @@
\<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing.
This and the following specifications do not affect parsing at all.
- \<^descr> @{verbatim "("}\<open>n\<close> opens a pretty printing block. The
+ \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The
optional number specifies how much indentation to add when a line
break occurs within the block. If the parenthesis is not followed
by digits, the indentation defaults to 0. A block specified via
- @{verbatim "(00"} is unbreakable.
+ \<^verbatim>\<open>(00\<close> is unbreakable.
- \<^descr> @{verbatim ")"} closes a pretty printing block.
+ \<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block.
- \<^descr> @{verbatim "//"} forces a line break.
+ \<^descr> \<^verbatim>\<open>//\<close> forces a line break.
- \<^descr> @{verbatim "/"}\<open>s\<close> allows a line break. Here \<open>s\<close>
+ \<^descr> \<^verbatim>\<open>/\<close>\<open>s\<close> allows a line break. Here \<open>s\<close>
stands for the string of spaces (zero or more) right after the
slash. These spaces are printed if the break is \<^emph>\<open>not\<close> taken.
@@ -418,25 +415,25 @@
\begin{center}
\begin{tabular}{lll}
- @{verbatim "("}@{keyword_def "infix"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>"\<close>} \<open>p\<close>@{verbatim ")"}
+ \<^verbatim>\<open>(\<close>@{keyword_def "infix"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>"\<close> \<open>p\<close>\<^verbatim>\<open>)\<close>
& \<open>\<mapsto>\<close> &
- @{verbatim \<open>("(_\<close>}~\<open>sy\<close>@{verbatim \<open>/ _)" [\<close>}\<open>p + 1\<close>@{verbatim ","}~\<open>p + 1\<close>@{verbatim "]"}~\<open>p\<close>@{verbatim ")"} \\
- @{verbatim "("}@{keyword_def "infixl"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>"\<close>} \<open>p\<close>@{verbatim ")"}
+ \<^verbatim>\<open>("(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)" [\<close>\<open>p + 1\<close>\<^verbatim>\<open>,\<close>~\<open>p + 1\<close>\<^verbatim>\<open>]\<close>~\<open>p\<close>\<^verbatim>\<open>)\<close> \\
+ \<^verbatim>\<open>(\<close>@{keyword_def "infixl"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>"\<close> \<open>p\<close>\<^verbatim>\<open>)\<close>
& \<open>\<mapsto>\<close> &
- @{verbatim \<open>("(_\<close>}~\<open>sy\<close>@{verbatim \<open>/ _)" [\<close>}\<open>p\<close>@{verbatim ","}~\<open>p + 1\<close>@{verbatim "]"}~\<open>p\<close>@{verbatim ")"} \\
- @{verbatim "("}@{keyword_def "infixr"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>"\<close>}~\<open>p\<close>@{verbatim ")"}
+ \<^verbatim>\<open>("(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)" [\<close>\<open>p\<close>\<^verbatim>\<open>,\<close>~\<open>p + 1\<close>\<^verbatim>\<open>]\<close>~\<open>p\<close>\<^verbatim>\<open>)\<close> \\
+ \<^verbatim>\<open>(\<close>@{keyword_def "infixr"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>"\<close>~\<open>p\<close>\<^verbatim>\<open>)\<close>
& \<open>\<mapsto>\<close> &
- @{verbatim \<open>("(_\<close>}~\<open>sy\<close>@{verbatim \<open>/ _)" [\<close>}\<open>p + 1\<close>@{verbatim ","}~\<open>p\<close>@{verbatim "]"}~\<open>p\<close>@{verbatim ")"} \\
+ \<^verbatim>\<open>("(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)" [\<close>\<open>p + 1\<close>\<^verbatim>\<open>,\<close>~\<open>p\<close>\<^verbatim>\<open>]\<close>~\<open>p\<close>\<^verbatim>\<open>)\<close> \\
\end{tabular}
\end{center}
- The mixfix template @{verbatim \<open>"(_\<close>}~\<open>sy\<close>@{verbatim \<open>/ _)"\<close>}
+ The mixfix template \<^verbatim>\<open>"(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)"\<close>
specifies two argument positions; the delimiter is preceded by a
space and followed by a space or line break; the entire phrase is a
pretty printing block.
- The alternative notation @{verbatim "op"}~\<open>sy\<close> is introduced
+ The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced
in addition. Thus any infix operator may be written in prefix form
(as in ML), independently of the number of arguments in the term.
\<close>
@@ -452,7 +449,7 @@
as follows:
\begin{center}
- \<open>c ::\<close>~@{verbatim \<open>"\<close>}\<open>(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3\<close>@{verbatim \<open>" (\<close>}@{keyword "binder"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>" [\<close>}\<open>p\<close>@{verbatim "]"}~\<open>q\<close>@{verbatim ")"}
+ \<open>c ::\<close>~\<^verbatim>\<open>"\<close>\<open>(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3\<close>\<^verbatim>\<open>" (\<close>@{keyword "binder"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>" [\<close>\<open>p\<close>\<^verbatim>\<open>]\<close>~\<open>q\<close>\<^verbatim>\<open>)\<close>
\end{center}
This introduces concrete binder syntax \<open>sy x. b\<close>, where
@@ -463,13 +460,13 @@
Internally, the binder syntax is expanded to something like this:
\begin{center}
- \<open>c_binder ::\<close>~@{verbatim \<open>"\<close>}\<open>idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close>@{verbatim \<open>" ("(3\<close>}\<open>sy\<close>@{verbatim \<open>_./ _)" [0,\<close>}~\<open>p\<close>@{verbatim "]"}~\<open>q\<close>@{verbatim ")"}
+ \<open>c_binder ::\<close>~\<^verbatim>\<open>"\<close>\<open>idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close>\<^verbatim>\<open>" ("(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)" [0,\<close>~\<open>p\<close>\<^verbatim>\<open>]\<close>~\<open>q\<close>\<^verbatim>\<open>)\<close>
\end{center}
Here @{syntax (inner) idts} is the nonterminal symbol for a list of
identifiers with optional type constraints (see also
- \secref{sec:pure-grammar}). The mixfix template @{verbatim
- \<open>"(3\<close>}\<open>sy\<close>@{verbatim \<open>_./ _)"\<close>} defines argument positions
+ \secref{sec:pure-grammar}). The mixfix template \<^verbatim>\<open>"(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)"\<close>
+ defines argument positions
for the bound identifiers and the body, separated by a dot with
optional line break; the entire phrase is a pretty printing block of
indentation level 3. Note that there is no extra space after \<open>sy\<close>, so it needs to be included user specification if the binder
@@ -563,9 +560,9 @@
@{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
@{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
@{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
- @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
- @{syntax_def (inner) str_token} & = & @{verbatim "''"} \<open>\<dots>\<close> @{verbatim "''"} \\
- @{syntax_def (inner) string_token} & = & @{verbatim \<open>"\<close>} \<open>\<dots>\<close> @{verbatim \<open>"\<close>} \\
+ @{syntax_def (inner) float_token} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
+ @{syntax_def (inner) str_token} & = & \<^verbatim>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
+ @{syntax_def (inner) string_token} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
@{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
\end{supertabular}
\end{center}
@@ -614,17 +611,17 @@
\begin{center}
\begin{tabular}{rclr}
- \<open>A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>=\<close> & @{verbatim "("} \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim ")"} \\
- \<open>A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>=\<close> & @{verbatim 0} \\
- \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> & \<open>=\<close> & \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim "+"} \<open>A\<^sup>(\<^sup>1\<^sup>)\<close> \\
- \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>=\<close> & \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> @{verbatim "*"} \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> \\
- \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>=\<close> & @{verbatim "-"} \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \\
+ \<open>A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>(\<close> \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> \<^verbatim>\<open>)\<close> \\
+ \<open>A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>0\<close> \\
+ \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> & \<open>=\<close> & \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> \<^verbatim>\<open>+\<close> \<open>A\<^sup>(\<^sup>1\<^sup>)\<close> \\
+ \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>=\<close> & \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \<^verbatim>\<open>*\<close> \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> \\
+ \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>-\<close> \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \\
\end{tabular}
\end{center}
- The choice of priorities determines that @{verbatim "-"} binds
- tighter than @{verbatim "*"}, which binds tighter than @{verbatim
- "+"}. Furthermore @{verbatim "+"} associates to the left and
- @{verbatim "*"} to the right.
+ The choice of priorities determines that \<^verbatim>\<open>-\<close> binds
+ tighter than \<^verbatim>\<open>*\<close>, which binds tighter than \<^verbatim>\<open>+\<close>.
+ Furthermore \<^verbatim>\<open>+\<close> associates to the left and
+ \<^verbatim>\<open>*\<close> to the right.
\<^medskip>
For clarity, grammars obey these conventions:
@@ -648,11 +645,11 @@
takes the form:
\begin{center}
\begin{tabular}{rclc}
- \<open>A\<close> & \<open>=\<close> & @{verbatim "("} \<open>A\<close> @{verbatim ")"} \\
- & \<open>|\<close> & @{verbatim 0} & \qquad\qquad \\
- & \<open>|\<close> & \<open>A\<close> @{verbatim "+"} \<open>A\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(0)\<close> \\
- & \<open>|\<close> & \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> @{verbatim "*"} \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>(2)\<close> \\
- & \<open>|\<close> & @{verbatim "-"} \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
+ \<open>A\<close> & \<open>=\<close> & \<^verbatim>\<open>(\<close> \<open>A\<close> \<^verbatim>\<open>)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>0\<close> & \qquad\qquad \\
+ & \<open>|\<close> & \<open>A\<close> \<^verbatim>\<open>+\<close> \<open>A\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(0)\<close> \\
+ & \<open>|\<close> & \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \<^verbatim>\<open>*\<close> \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>(2)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>-\<close> \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
\end{tabular}
\end{center}
\<close>
@@ -668,46 +665,46 @@
@{syntax_def (inner) any} & = & \<open>prop | logic\<close> \\\\
- @{syntax_def (inner) prop} & = & @{verbatim "("} \<open>prop\<close> @{verbatim ")"} \\
- & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>4\<^sup>)\<close> @{verbatim "::"} \<open>type\<close> & \<open>(3)\<close> \\
- & \<open>|\<close> & \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> @{verbatim "=="} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(2)\<close> \\
+ @{syntax_def (inner) prop} & = & \<^verbatim>\<open>(\<close> \<open>prop\<close> \<^verbatim>\<open>)\<close> \\
+ & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>4\<^sup>)\<close> \<^verbatim>\<open>::\<close> \<open>type\<close> & \<open>(3)\<close> \\
+ & \<open>|\<close> & \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> \<^verbatim>\<open>==\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(2)\<close> \\
& \<open>|\<close> & \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> \<open>\<equiv>\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(2)\<close> \\
- & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>3\<^sup>)\<close> @{verbatim "&&&"} \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>(2)\<close> \\
- & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> @{verbatim "==>"} \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
+ & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>3\<^sup>)\<close> \<^verbatim>\<open>&&&\<close> \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>(2)\<close> \\
+ & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> \<^verbatim>\<open>==>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
& \<open>|\<close> & \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> \<open>\<Longrightarrow>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
- & \<open>|\<close> & @{verbatim "[|"} \<open>prop\<close> @{verbatim ";"} \<open>\<dots>\<close> @{verbatim ";"} \<open>prop\<close> @{verbatim "|]"} @{verbatim "==>"} \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
- & \<open>|\<close> & \<open>\<lbrakk>\<close> \<open>prop\<close> @{verbatim ";"} \<open>\<dots>\<close> @{verbatim ";"} \<open>prop\<close> \<open>\<rbrakk>\<close> \<open>\<Longrightarrow>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
- & \<open>|\<close> & @{verbatim "!!"} \<open>idts\<close> @{verbatim "."} \<open>prop\<close> & \<open>(0)\<close> \\
- & \<open>|\<close> & \<open>\<And>\<close> \<open>idts\<close> @{verbatim "."} \<open>prop\<close> & \<open>(0)\<close> \\
- & \<open>|\<close> & @{verbatim OFCLASS} @{verbatim "("} \<open>type\<close> @{verbatim ","} \<open>logic\<close> @{verbatim ")"} \\
- & \<open>|\<close> & @{verbatim SORT_CONSTRAINT} @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\
- & \<open>|\<close> & @{verbatim TERM} \<open>logic\<close> \\
- & \<open>|\<close> & @{verbatim PROP} \<open>aprop\<close> \\\\
+ & \<open>|\<close> & \<^verbatim>\<open>[|\<close> \<open>prop\<close> \<^verbatim>\<open>;\<close> \<open>\<dots>\<close> \<^verbatim>\<open>;\<close> \<open>prop\<close> \<^verbatim>\<open>|]\<close> \<^verbatim>\<open>==>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
+ & \<open>|\<close> & \<open>\<lbrakk>\<close> \<open>prop\<close> \<^verbatim>\<open>;\<close> \<open>\<dots>\<close> \<^verbatim>\<open>;\<close> \<open>prop\<close> \<open>\<rbrakk>\<close> \<open>\<Longrightarrow>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>!!\<close> \<open>idts\<close> \<^verbatim>\<open>.\<close> \<open>prop\<close> & \<open>(0)\<close> \\
+ & \<open>|\<close> & \<open>\<And>\<close> \<open>idts\<close> \<^verbatim>\<open>.\<close> \<open>prop\<close> & \<open>(0)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>OFCLASS\<close> \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>logic\<close> \<^verbatim>\<open>)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>SORT_CONSTRAINT\<close> \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>TERM\<close> \<open>logic\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>PROP\<close> \<open>aprop\<close> \\\\
- @{syntax_def (inner) aprop} & = & @{verbatim "("} \<open>aprop\<close> @{verbatim ")"} \\
- & \<open>|\<close> & \<open>id | longid | var |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "..."} \\
- & \<open>|\<close> & @{verbatim CONST} \<open>id |\<close>~~@{verbatim CONST} \<open>longid\<close> \\
- & \<open>|\<close> & @{verbatim XCONST} \<open>id |\<close>~~@{verbatim XCONST} \<open>longid\<close> \\
+ @{syntax_def (inner) aprop} & = & \<^verbatim>\<open>(\<close> \<open>aprop\<close> \<^verbatim>\<open>)\<close> \\
+ & \<open>|\<close> & \<open>id | longid | var |\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>...\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>CONST\<close> \<open>id |\<close>~~\<^verbatim>\<open>CONST\<close> \<open>longid\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>XCONST\<close> \<open>id |\<close>~~\<^verbatim>\<open>XCONST\<close> \<open>longid\<close> \\
& \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\\\
- @{syntax_def (inner) logic} & = & @{verbatim "("} \<open>logic\<close> @{verbatim ")"} \\
- & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>4\<^sup>)\<close> @{verbatim "::"} \<open>type\<close> & \<open>(3)\<close> \\
- & \<open>|\<close> & \<open>id | longid | var |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "..."} \\
- & \<open>|\<close> & @{verbatim CONST} \<open>id |\<close>~~@{verbatim CONST} \<open>longid\<close> \\
- & \<open>|\<close> & @{verbatim XCONST} \<open>id |\<close>~~@{verbatim XCONST} \<open>longid\<close> \\
+ @{syntax_def (inner) logic} & = & \<^verbatim>\<open>(\<close> \<open>logic\<close> \<^verbatim>\<open>)\<close> \\
+ & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>4\<^sup>)\<close> \<^verbatim>\<open>::\<close> \<open>type\<close> & \<open>(3)\<close> \\
+ & \<open>|\<close> & \<open>id | longid | var |\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>...\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>CONST\<close> \<open>id |\<close>~~\<^verbatim>\<open>CONST\<close> \<open>longid\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>XCONST\<close> \<open>id |\<close>~~\<^verbatim>\<open>XCONST\<close> \<open>longid\<close> \\
& \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\
& \<open>|\<close> & \<open>\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> \\
- & \<open>|\<close> & @{verbatim "%"} \<open>pttrns\<close> @{verbatim "."} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
- & \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> @{verbatim "."} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
- & \<open>|\<close> & @{verbatim op} @{verbatim "=="}~~\<open>|\<close>~~@{verbatim op} \<open>\<equiv>\<close>~~\<open>|\<close>~~@{verbatim op} @{verbatim "&&&"} \\
- & \<open>|\<close> & @{verbatim op} @{verbatim "==>"}~~\<open>|\<close>~~@{verbatim op} \<open>\<Longrightarrow>\<close> \\
- & \<open>|\<close> & @{verbatim TYPE} @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\\\
+ & \<open>|\<close> & \<^verbatim>\<open>%\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
+ & \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>op\<close> \<^verbatim>\<open>==\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<open>\<equiv>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<^verbatim>\<open>&&&\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>op\<close> \<^verbatim>\<open>==>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<open>\<Longrightarrow>\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>TYPE\<close> \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \\\\
- @{syntax_def (inner) idt} & = & @{verbatim "("} \<open>idt\<close> @{verbatim ")"}~~\<open>| id |\<close>~~@{verbatim "_"} \\
- & \<open>|\<close> & \<open>id\<close> @{verbatim "::"} \<open>type\<close> & \<open>(0)\<close> \\
- & \<open>|\<close> & @{verbatim "_"} @{verbatim "::"} \<open>type\<close> & \<open>(0)\<close> \\\\
+ @{syntax_def (inner) idt} & = & \<^verbatim>\<open>(\<close> \<open>idt\<close> \<^verbatim>\<open>)\<close>~~\<open>| id |\<close>~~\<^verbatim>\<open>_\<close> \\
+ & \<open>|\<close> & \<open>id\<close> \<^verbatim>\<open>::\<close> \<open>type\<close> & \<open>(0)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>_\<close> \<^verbatim>\<open>::\<close> \<open>type\<close> & \<open>(0)\<close> \\\\
- @{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} \<open>logic\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim "\<^esub>"}~~\<open>| | \<index>\<close> \\\\
+ @{syntax_def (inner) index} & = & \<^verbatim>\<open>\<^bsub>\<close> \<open>logic\<^sup>(\<^sup>0\<^sup>)\<close> \<^verbatim>\<open>\<^esub>\<close>~~\<open>| | \<index>\<close> \\\\
@{syntax_def (inner) idts} & = & \<open>idt | idt\<^sup>(\<^sup>1\<^sup>) idts\<close> & \<open>(0)\<close> \\\\
@@ -715,25 +712,25 @@
@{syntax_def (inner) pttrns} & = & \<open>pttrn | pttrn\<^sup>(\<^sup>1\<^sup>) pttrns\<close> & \<open>(0)\<close> \\\\
- @{syntax_def (inner) type} & = & @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\
- & \<open>|\<close> & \<open>tid | tvar |\<close>~~@{verbatim "_"} \\
- & \<open>|\<close> & \<open>tid\<close> @{verbatim "::"} \<open>sort | tvar\<close>~~@{verbatim "::"} \<open>sort |\<close>~~@{verbatim "_"} @{verbatim "::"} \<open>sort\<close> \\
+ @{syntax_def (inner) type} & = & \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \\
+ & \<open>|\<close> & \<open>tid | tvar |\<close>~~\<^verbatim>\<open>_\<close> \\
+ & \<open>|\<close> & \<open>tid\<close> \<^verbatim>\<open>::\<close> \<open>sort | tvar\<close>~~\<^verbatim>\<open>::\<close> \<open>sort |\<close>~~\<^verbatim>\<open>_\<close> \<^verbatim>\<open>::\<close> \<open>sort\<close> \\
& \<open>|\<close> & \<open>type_name | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name\<close> \\
- & \<open>|\<close> & @{verbatim "("} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim ")"} \<open>type_name\<close> \\
- & \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> @{verbatim "=>"} \<open>type\<close> & \<open>(0)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \<open>type_name\<close> \\
+ & \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> \<^verbatim>\<open>=>\<close> \<open>type\<close> & \<open>(0)\<close> \\
& \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
- & \<open>|\<close> & @{verbatim "["} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim "]"} @{verbatim "=>"} \<open>type\<close> & \<open>(0)\<close> \\
- & \<open>|\<close> & @{verbatim "["} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim "]"} \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>[\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> \<open>type\<close> \<^verbatim>\<open>]\<close> \<^verbatim>\<open>=>\<close> \<open>type\<close> & \<open>(0)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>[\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> \<open>type\<close> \<^verbatim>\<open>]\<close> \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
@{syntax_def (inner) type_name} & = & \<open>id | longid\<close> \\\\
- @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~@{verbatim "{}"} \\
- & \<open>|\<close> & @{verbatim "{"} @{syntax class_name} @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} @{syntax class_name} @{verbatim "}"} \\
+ @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~\<^verbatim>\<open>{}\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>{\<close> @{syntax class_name} \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> @{syntax class_name} \<^verbatim>\<open>}\<close> \\
@{syntax_def (inner) class_name} & = & \<open>id | longid\<close> \\
\end{supertabular}
\end{center}
\<^medskip>
- Here literal terminals are printed @{verbatim "verbatim"};
+ Here literal terminals are printed \<^verbatim>\<open>verbatim\<close>;
see also \secref{sec:inner-lex} for further token categories of the
inner syntax. The meaning of the nonterminals defined by the above
grammar is as follows:
@@ -748,7 +745,7 @@
\<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which
are embedded into regular @{syntax (inner) prop} by means of an
- explicit @{verbatim PROP} token.
+ explicit \<^verbatim>\<open>PROP\<close> token.
Terms of type @{typ prop} with non-constant head, e.g.\ a plain
variable, are printed in this form. Constants that yield type @{typ
@@ -828,18 +825,18 @@
x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by
using both bound and schematic dummies.
- \<^descr> The three literal dots ``@{verbatim "..."}'' may be also
- written as ellipsis symbol @{verbatim "\<dots>"}. In both cases this
+ \<^descr> The three literal dots ``\<^verbatim>\<open>...\<close>'' may be also
+ written as ellipsis symbol \<^verbatim>\<open>\<dots>\<close>. In both cases this
refers to a special schematic variable, which is bound in the
context. This special term abbreviation works nicely with
calculational reasoning (\secref{sec:calculation}).
- \<^descr> @{verbatim CONST} ensures that the given identifier is treated
+ \<^descr> \<^verbatim>\<open>CONST\<close> ensures that the given identifier is treated
as constant term, and passed through the parse tree in fully
internalized form. This is particularly relevant for translation
rules (\secref{sec:syn-trans}), notably on the RHS.
- \<^descr> @{verbatim XCONST} is similar to @{verbatim CONST}, but
+ \<^descr> \<^verbatim>\<open>XCONST\<close> is similar to \<^verbatim>\<open>CONST\<close>, but
retains the constant name as given. This is only relevant to
translation rules (\secref{sec:syn-trans}), notably on the LHS.
\<close>
@@ -995,22 +992,22 @@
applications as a parenthesized list of subtrees. For example, the
AST
@{ML [display] \<open>Ast.Appl [Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"]\<close>}
- is pretty-printed as @{verbatim \<open>("_abs" x t)\<close>}. Note that
- @{verbatim "()"} and @{verbatim "(x)"} are excluded as ASTs, because
+ is pretty-printed as \<^verbatim>\<open>("_abs" x t)\<close>. Note that
+ \<^verbatim>\<open>()\<close> and \<^verbatim>\<open>(x)\<close> are excluded as ASTs, because
they have too few subtrees.
\<^medskip>
AST application is merely a pro-forma mechanism to indicate
- certain syntactic structures. Thus @{verbatim "(c a b)"} could mean
+ certain syntactic structures. Thus \<^verbatim>\<open>(c a b)\<close> could mean
either term application or type application, depending on the
syntactic context.
- Nested application like @{verbatim \<open>(("_abs" x t) u)\<close>} is also
+ Nested application like \<^verbatim>\<open>(("_abs" x t) u)\<close> is also
possible, but ASTs are definitely first-order: the syntax constant
- @{verbatim \<open>"_abs"\<close>} does not bind the @{verbatim x} in any way.
+ \<^verbatim>\<open>"_abs"\<close> does not bind the \<^verbatim>\<open>x\<close> in any way.
Proper bindings are introduced in later stages of the term syntax,
- where @{verbatim \<open>("_abs" x t)\<close>} becomes an @{ML Abs} node and
- occurrences of @{verbatim x} in @{verbatim t} are replaced by bound
+ where \<^verbatim>\<open>("_abs" x t)\<close> becomes an @{ML Abs} node and
+ occurrences of \<^verbatim>\<open>x\<close> in \<^verbatim>\<open>t\<close> are replaced by bound
variables (represented as de-Bruijn indices).
\<close>
@@ -1136,14 +1133,14 @@
\<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the
priority grammar and the pretty printer table for the given print
- mode (default @{verbatim \<open>""\<close>}). An optional keyword @{keyword_ref
+ mode (default \<^verbatim>\<open>""\<close>). An optional keyword @{keyword_ref
"output"} means that only the pretty printer table is affected.
Following \secref{sec:mixfix}, the mixfix annotation \<open>mx =
template ps q\<close> together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and
specify a grammar production. The \<open>template\<close> contains
delimiter tokens that surround \<open>n\<close> argument positions
- (@{verbatim "_"}). The latter correspond to nonterminal symbols
+ (\<^verbatim>\<open>_\<close>). The latter correspond to nonterminal symbols
\<open>A\<^sub>i\<close> derived from the argument types \<open>\<tau>\<^sub>i\<close> as
follows:
@@ -1173,8 +1170,8 @@
with other syntax declarations.
\<^medskip>
- The special case of copy production is specified by \<open>c =\<close>~@{verbatim \<open>""\<close>} (empty string). It means that the
- resulting parse tree \<open>t\<close> is copied directly, without any
+ The special case of copy production is specified by \<open>c =\<close>~\<^verbatim>\<open>""\<close> (empty string).
+ It means that the resulting parse tree \<open>t\<close> is copied directly, without any
further decoration.
\<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar
@@ -1184,10 +1181,10 @@
\<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic
translation rules (i.e.\ macros) as first-order rewrite rules on
ASTs (\secref{sec:ast}). The theory context maintains two
- independent lists translation rules: parse rules (@{verbatim "=>"}
- or \<open>\<rightharpoonup>\<close>) and print rules (@{verbatim "<="} or \<open>\<leftharpoondown>\<close>).
+ independent lists translation rules: parse rules (\<^verbatim>\<open>=>\<close>
+ or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>).
For convenience, both can be specified simultaneously as parse~/
- print rules (@{verbatim "=="} or \<open>\<rightleftharpoons>\<close>).
+ print rules (\<^verbatim>\<open>==\<close> or \<open>\<rightleftharpoons>\<close>).
Translation patterns may be prefixed by the syntactic category to be
used for parsing; the default is \<open>logic\<close> which means that
@@ -1482,13 +1479,13 @@
\begin{tabular}{ll}
input source & AST \\
\hline
- \<open>f x y z\<close> & @{verbatim "(f x y z)"} \\
- \<open>'a ty\<close> & @{verbatim "(ty 'a)"} \\
- \<open>('a, 'b)ty\<close> & @{verbatim "(ty 'a 'b)"} \\
- \<open>\<lambda>x y z. t\<close> & @{verbatim \<open>("_abs" x ("_abs" y ("_abs" z t)))\<close>} \\
- \<open>\<lambda>x :: 'a. t\<close> & @{verbatim \<open>("_abs" ("_constrain" x 'a) t)\<close>} \\
- \<open>\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S\<close> & @{verbatim \<open>("Pure.imp" P ("Pure.imp" Q ("Pure.imp" R S)))\<close>} \\
- \<open>['a, 'b, 'c] \<Rightarrow> 'd\<close> & @{verbatim \<open>("fun" 'a ("fun" 'b ("fun" 'c 'd)))\<close>} \\
+ \<open>f x y z\<close> & \<^verbatim>\<open>(f x y z)\<close> \\
+ \<open>'a ty\<close> & \<^verbatim>\<open>(ty 'a)\<close> \\
+ \<open>('a, 'b)ty\<close> & \<^verbatim>\<open>(ty 'a 'b)\<close> \\
+ \<open>\<lambda>x y z. t\<close> & \<^verbatim>\<open>("_abs" x ("_abs" y ("_abs" z t)))\<close> \\
+ \<open>\<lambda>x :: 'a. t\<close> & \<^verbatim>\<open>("_abs" ("_constrain" x 'a) t)\<close> \\
+ \<open>\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S\<close> & \<^verbatim>\<open>("Pure.imp" P ("Pure.imp" Q ("Pure.imp" R S)))\<close> \\
+ \<open>['a, 'b, 'c] \<Rightarrow> 'd\<close> & \<^verbatim>\<open>("fun" 'a ("fun" 'b ("fun" 'c 'd)))\<close> \\
\end{tabular}
\end{center}
@@ -1504,7 +1501,7 @@
text \<open>After application of macros (\secref{sec:syn-trans}), the AST
is transformed into a term. This term still lacks proper type
information, but it might contain some constraints consisting of
- applications with head @{verbatim "_constrain"}, where the second
+ applications with head \<^verbatim>\<open>_constrain\<close>, where the second
argument is a type encoded as a pre-term within the syntax. Type
inference later introduces correct types, or indicates type errors
in the input.
@@ -1516,8 +1513,8 @@
The outcome is still a first-order term. Proper abstractions and
bound variables are introduced by parse translations associated with
- certain syntax constants. Thus @{verbatim \<open>("_abs" x x)\<close>} eventually
- becomes a de-Bruijn term @{verbatim \<open>Abs ("x", _, Bound 0)\<close>}.
+ certain syntax constants. Thus \<^verbatim>\<open>("_abs" x x)\<close> eventually
+ becomes a de-Bruijn term \<^verbatim>\<open>Abs ("x", _, Bound 0)\<close>.
\<close>
@@ -1530,8 +1527,8 @@
Ignoring print translations, the transformation maps term constants,
variables and applications to the corresponding constructs on ASTs.
Abstractions are mapped to applications of the special constant
- @{verbatim "_abs"} as seen before. Type constraints are represented
- via special @{verbatim "_constrain"} forms, according to various
+ \<^verbatim>\<open>_abs\<close> as seen before. Type constraints are represented
+ via special \<^verbatim>\<open>_constrain\<close> forms, according to various
policies of type annotation determined elsewhere. Sort constraints
of type variables are handled in a similar fashion.
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Oct 22 21:16:49 2015 +0200
@@ -23,13 +23,13 @@
syntax is that of Isabelle/Isar theory sources (specifications and
proofs). As a general rule, inner syntax entities may occur only as
\<^emph>\<open>atomic entities\<close> within outer syntax. For example, the string
- @{verbatim \<open>"x + y"\<close>} and identifier @{verbatim z} are legal term
- specifications within a theory, while @{verbatim "x + y"} without
+ \<^verbatim>\<open>"x + y"\<close> and identifier \<^verbatim>\<open>z\<close> are legal term
+ specifications within a theory, while \<^verbatim>\<open>x + y\<close> without
quotes is not.
Printed theory documents usually omit quotes to gain readability
- (this is a matter of {\LaTeX} macro setup, say via @{verbatim
- "\\isabellestyle"}, see also @{cite "isabelle-system"}). Experienced
+ (this is a matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>,
+ see also @{cite "isabelle-system"}). Experienced
users of Isabelle/Isar may easily reconstruct the lost technical
information, while mere readers need not care about quotes at all.
\<close>
@@ -86,8 +86,8 @@
proof command etc.).
Keywords override named tokens. For example, the presence of a
- command called @{verbatim term} inhibits the identifier @{verbatim
- term}, but the string @{verbatim \<open>"term"\<close>} can be used instead.
+ command called \<^verbatim>\<open>term\<close> inhibits the identifier \<^verbatim>\<open>term\<close>, but the
+ string \<^verbatim>\<open>"term"\<close> can be used instead.
By convention, the outer syntax always allows quoted strings in
addition to identifiers, wherever a named entity is expected.
@@ -102,55 +102,55 @@
\begin{center}
\begin{supertabular}{rcl}
@{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
- @{syntax_def longident} & = & \<open>ident(\<close>@{verbatim "."}\<open>ident)\<^sup>+\<close> \\
- @{syntax_def symident} & = & \<open>sym\<^sup>+ |\<close>~~@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"} \\
+ @{syntax_def longident} & = & \<open>ident(\<close>\<^verbatim>\<open>.\<close>\<open>ident)\<^sup>+\<close> \\
+ @{syntax_def symident} & = & \<open>sym\<^sup>+ |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close> \\
@{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
- @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}~~\<open>|\<close>~~@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
- @{syntax_def var} & = & @{verbatim "?"}\<open>ident |\<close>~~@{verbatim "?"}\<open>ident\<close>@{verbatim "."}\<open>nat\<close> \\
- @{syntax_def typefree} & = & @{verbatim "'"}\<open>ident\<close> \\
- @{syntax_def typevar} & = & @{verbatim "?"}\<open>typefree |\<close>~~@{verbatim "?"}\<open>typefree\<close>@{verbatim "."}\<open>nat\<close> \\
- @{syntax_def string} & = & @{verbatim \<open>"\<close>} \<open>\<dots>\<close> @{verbatim \<open>"\<close>} \\
- @{syntax_def altstring} & = & @{verbatim "`"} \<open>\<dots>\<close> @{verbatim "`"} \\
+ @{syntax_def float} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat}~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>@{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
+ @{syntax_def var} & = & \<^verbatim>\<open>?\<close>\<open>ident |\<close>~~\<^verbatim>\<open>?\<close>\<open>ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
+ @{syntax_def typefree} & = & \<^verbatim>\<open>'\<close>\<open>ident\<close> \\
+ @{syntax_def typevar} & = & \<^verbatim>\<open>?\<close>\<open>typefree |\<close>~~\<^verbatim>\<open>?\<close>\<open>typefree\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
+ @{syntax_def string} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
+ @{syntax_def altstring} & = & \<^verbatim>\<open>`\<close> \<open>\<dots>\<close> \<^verbatim>\<open>`\<close> \\
@{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
- @{syntax_def verbatim} & = & @{verbatim "{*"} \<open>\<dots>\<close> @{verbatim "*}"} \\[1ex]
+ @{syntax_def verbatim} & = & \<^verbatim>\<open>{*\<close> \<open>\<dots>\<close> \<^verbatim>\<open>*}\<close> \\[1ex]
- \<open>letter\<close> & = & \<open>latin |\<close>~~@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin\<close>@{verbatim ">"}~~\<open>|\<close>~~@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin latin\<close>@{verbatim ">"}~~\<open>| greek |\<close> \\
- \<open>subscript\<close> & = & @{verbatim "\<^sub>"} \\
- \<open>quasiletter\<close> & = & \<open>letter | digit |\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "'"} \\
- \<open>latin\<close> & = & @{verbatim a}~~\<open>| \<dots> |\<close>~~@{verbatim z}~~\<open>|\<close>~~@{verbatim A}~~\<open>| \<dots> |\<close>~~@{verbatim Z} \\
- \<open>digit\<close> & = & @{verbatim "0"}~~\<open>| \<dots> |\<close>~~@{verbatim "9"} \\
- \<open>sym\<close> & = & @{verbatim "!"}~~\<open>|\<close>~~@{verbatim "#"}~~\<open>|\<close>~~@{verbatim "$"}~~\<open>|\<close>~~@{verbatim "%"}~~\<open>|\<close>~~@{verbatim "&"}~~\<open>|\<close>~~@{verbatim "*"}~~\<open>|\<close>~~@{verbatim "+"}~~\<open>|\<close>~~@{verbatim "-"}~~\<open>|\<close>~~@{verbatim "/"}~~\<open>|\<close> \\
- & & @{verbatim "<"}~~\<open>|\<close>~~@{verbatim "="}~~\<open>|\<close>~~@{verbatim ">"}~~\<open>|\<close>~~@{verbatim "?"}~~\<open>|\<close>~~@{verbatim "@"}~~\<open>|\<close>~~@{verbatim "^"}~~\<open>|\<close>~~@{verbatim "_"}~~\<open>|\<close>~~@{verbatim "|"}~~\<open>|\<close>~~@{verbatim "~"} \\
- \<open>greek\<close> & = & @{verbatim "\<alpha>"}~~\<open>|\<close>~~@{verbatim "\<beta>"}~~\<open>|\<close>~~@{verbatim "\<gamma>"}~~\<open>|\<close>~~@{verbatim "\<delta>"}~~\<open>|\<close> \\
- & & @{verbatim "\<epsilon>"}~~\<open>|\<close>~~@{verbatim "\<zeta>"}~~\<open>|\<close>~~@{verbatim "\<eta>"}~~\<open>|\<close>~~@{verbatim "\<theta>"}~~\<open>|\<close> \\
- & & @{verbatim "\<iota>"}~~\<open>|\<close>~~@{verbatim "\<kappa>"}~~\<open>|\<close>~~@{verbatim "\<mu>"}~~\<open>|\<close>~~@{verbatim "\<nu>"}~~\<open>|\<close> \\
- & & @{verbatim "\<xi>"}~~\<open>|\<close>~~@{verbatim "\<pi>"}~~\<open>|\<close>~~@{verbatim "\<rho>"}~~\<open>|\<close>~~@{verbatim "\<sigma>"}~~\<open>|\<close>~~@{verbatim "\<tau>"}~~\<open>|\<close> \\
- & & @{verbatim "\<upsilon>"}~~\<open>|\<close>~~@{verbatim "\<phi>"}~~\<open>|\<close>~~@{verbatim "\<chi>"}~~\<open>|\<close>~~@{verbatim "\<psi>"}~~\<open>|\<close> \\
- & & @{verbatim "\<omega>"}~~\<open>|\<close>~~@{verbatim "\<Gamma>"}~~\<open>|\<close>~~@{verbatim "\<Delta>"}~~\<open>|\<close>~~@{verbatim "\<Theta>"}~~\<open>|\<close> \\
- & & @{verbatim "\<Lambda>"}~~\<open>|\<close>~~@{verbatim "\<Xi>"}~~\<open>|\<close>~~@{verbatim "\<Pi>"}~~\<open>|\<close>~~@{verbatim "\<Sigma>"}~~\<open>|\<close> \\
- & & @{verbatim "\<Upsilon>"}~~\<open>|\<close>~~@{verbatim "\<Phi>"}~~\<open>|\<close>~~@{verbatim "\<Psi>"}~~\<open>|\<close>~~@{verbatim "\<Omega>"} \\
+ \<open>letter\<close> & = & \<open>latin |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>latin\<close>\<^verbatim>\<open>>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>latin latin\<close>\<^verbatim>\<open>>\<close>~~\<open>| greek |\<close> \\
+ \<open>subscript\<close> & = & \<^verbatim>\<open>\<^sub>\<close> \\
+ \<open>quasiletter\<close> & = & \<open>letter | digit |\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>'\<close> \\
+ \<open>latin\<close> & = & \<^verbatim>\<open>a\<close>~~\<open>| \<dots> |\<close>~~\<^verbatim>\<open>z\<close>~~\<open>|\<close>~~\<^verbatim>\<open>A\<close>~~\<open>| \<dots> |\<close>~~\<^verbatim>\<open>Z\<close> \\
+ \<open>digit\<close> & = & \<^verbatim>\<open>0\<close>~~\<open>| \<dots> |\<close>~~\<^verbatim>\<open>9\<close> \\
+ \<open>sym\<close> & = & \<^verbatim>\<open>!\<close>~~\<open>|\<close>~~\<^verbatim>\<open>#\<close>~~\<open>|\<close>~~\<^verbatim>\<open>$\<close>~~\<open>|\<close>~~\<^verbatim>\<open>%\<close>~~\<open>|\<close>~~\<^verbatim>\<open>&\<close>~~\<open>|\<close>~~\<^verbatim>\<open>*\<close>~~\<open>|\<close>~~\<^verbatim>\<open>+\<close>~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>~~\<open>|\<close>~~\<^verbatim>\<open>/\<close>~~\<open>|\<close> \\
+ & & \<^verbatim>\<open><\<close>~~\<open>|\<close>~~\<^verbatim>\<open>=\<close>~~\<open>|\<close>~~\<^verbatim>\<open>>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>?\<close>~~\<open>|\<close>~~\<^verbatim>\<open>@\<close>~~\<open>|\<close>~~\<^verbatim>\<open>^\<close>~~\<open>|\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>|\<close>~~\<open>|\<close>~~\<^verbatim>\<open>~\<close> \\
+ \<open>greek\<close> & = & \<^verbatim>\<open>\<alpha>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<beta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<gamma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<delta>\<close>~~\<open>|\<close> \\
+ & & \<^verbatim>\<open>\<epsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<zeta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<eta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<theta>\<close>~~\<open>|\<close> \\
+ & & \<^verbatim>\<open>\<iota>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<kappa>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<mu>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<nu>\<close>~~\<open>|\<close> \\
+ & & \<^verbatim>\<open>\<xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<rho>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<sigma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<tau>\<close>~~\<open>|\<close> \\
+ & & \<^verbatim>\<open>\<upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<chi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<psi>\<close>~~\<open>|\<close> \\
+ & & \<^verbatim>\<open>\<omega>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Gamma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Delta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Theta>\<close>~~\<open>|\<close> \\
+ & & \<^verbatim>\<open>\<Lambda>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Sigma>\<close>~~\<open>|\<close> \\
+ & & \<^verbatim>\<open>\<Upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Psi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Omega>\<close> \\
\end{supertabular}
\end{center}
A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
which is internally a pair of base name and index (ML type @{ML_type
indexname}). These components are either separated by a dot as in
- \<open>?x.1\<close> or \<open>?x7.3\<close> or run together as in \<open>?x1\<close>. The latter form is possible if the base name does not end
- with digits. If the index is 0, it may be dropped altogether:
- \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the
+ \<open>?x.1\<close> or \<open>?x7.3\<close> or run together as in \<open>?x1\<close>. The latter form is possible
+ if the base name does not end with digits. If the index is 0, it may be
+ dropped altogether: \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the
same unknown, with basename \<open>x\<close> and index 0.
The syntax of @{syntax_ref string} admits any characters, including
- newlines; ``@{verbatim \<open>"\<close>}'' (double-quote) and ``@{verbatim \<open>\\<close>}''
+ newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>''
(backslash) need to be escaped by a backslash; arbitrary
- character codes may be specified as ``@{verbatim \<open>\\<close>}\<open>ddd\<close>'',
+ character codes may be specified as ``\<^verbatim>\<open>\\<close>\<open>ddd\<close>'',
with three decimal digits. Alternative strings according to
@{syntax_ref altstring} are analogous, using single back-quotes
instead.
The body of @{syntax_ref verbatim} may consist of any text not containing
- ``@{verbatim "*}"}''; this allows to include quotes without further
- escapes, but there is no way to escape ``@{verbatim "*}"}''. Cartouches
+ ``\<^verbatim>\<open>*}\<close>''; this allows to include quotes without further
+ escapes, but there is no way to escape ``\<^verbatim>\<open>*}\<close>''. Cartouches
do not have this limitation.
A @{syntax_ref cartouche} consists of arbitrary text, with properly
@@ -158,18 +158,18 @@
"\<close>"}''. Note that the rendering of cartouche delimiters is
usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
- Source comments take the form @{verbatim "(*"}~\<open>\<dots>\<close>~@{verbatim "*)"} and may be nested, although the user-interface
+ Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although the user-interface
might prevent this. Note that this form indicates source comments
only, which are stripped after lexical analysis of the input. The
Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are
considered as part of the text (see \secref{sec:comments}).
Common mathematical symbols such as \<open>\<forall>\<close> are represented in
- Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle
+ Isabelle as \<^verbatim>\<open>\<forall>\<close>. There are infinitely many Isabelle
symbols like this, although proper presentation is left to front-end
tools such as {\LaTeX} or Isabelle/jEdit. A list of
predefined Isabelle symbols that work well with these tools is given
- in \appref{app:symbols}. Note that @{verbatim "\<lambda>"} does not belong
+ in \appref{app:symbols}. Note that \<^verbatim>\<open>\<lambda>\<close> does not belong
to the \<open>letter\<close> category, since it is already used differently
in the Pure term language.\<close>
@@ -189,7 +189,7 @@
constants, theorems etc.\ that are to be \<^emph>\<open>declared\<close> or
\<^emph>\<open>defined\<close> (so qualified identifiers are excluded here). Quoted
strings provide an escape for non-identifier names or those ruled
- out by outer syntax keywords (e.g.\ quoted @{verbatim \<open>"let"\<close>}).
+ out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>).
Already existing objects are usually referenced by @{syntax
nameref}.
@@ -224,10 +224,10 @@
subsection \<open>Comments \label{sec:comments}\<close>
text \<open>Large chunks of plain @{syntax text} are usually given @{syntax
- verbatim}, i.e.\ enclosed in @{verbatim "{*"}~\<open>\<dots>\<close>~@{verbatim "*}"},
+ verbatim}, i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>,
or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For convenience, any of the
smaller text units conforming to @{syntax nameref} are admitted as well. A
- marginal @{syntax comment} is of the form @{verbatim "--"}~@{syntax text}.
+ marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax text}.
Any number of these may occur within Isabelle/Isar commands.
@{rail \<open>
@@ -267,10 +267,11 @@
is performed internally later). For convenience, a slightly more
liberal convention is adopted: quotes may be omitted for any type or
term that is already atomic at the outer level. For example, one
- may just write @{verbatim x} instead of quoted @{verbatim \<open>"x"\<close>}.
- Note that symbolic identifiers (e.g.\ @{verbatim "++"} or \<open>\<forall>\<close> are available as well, provided these have not been superseded
- by commands or other keywords already (such as @{verbatim "="} or
- @{verbatim "+"}).
+ may just write \<^verbatim>\<open>x\<close> instead of quoted \<^verbatim>\<open>"x"\<close>.
+ Note that symbolic identifiers (e.g.\ \<^verbatim>\<open>++\<close> or \<open>\<forall>\<close> are available as well,
+ provided these have not been superseded
+ by commands or other keywords already (such as \<^verbatim>\<open>=\<close> or
+ \<^verbatim>\<open>+\<close>).
@{rail \<open>
@{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
@@ -408,7 +409,7 @@
\<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>,
\<^enum> literal fact propositions using token syntax @{syntax_ref altstring}
- @{verbatim "`"}\<open>\<phi>\<close>@{verbatim "`"} or @{syntax_ref cartouche}
+ \<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close> or @{syntax_ref cartouche}
\<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}).
--- a/src/Doc/Isar_Ref/Proof.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Thu Oct 22 21:16:49 2015 +0200
@@ -598,16 +598,15 @@
subsection \<open>Proof method expressions \label{sec:proof-meth}\<close>
text \<open>Proof methods are either basic ones, or expressions composed of
- methods via ``@{verbatim ","}'' (sequential composition), ``@{verbatim
- ";"}'' (structural composition), ``@{verbatim "|"}'' (alternative
- choices), ``@{verbatim "?"}'' (try), ``@{verbatim "+"}'' (repeat at least
- once), ``@{verbatim "["}\<open>n\<close>@{verbatim "]"}'' (restriction to first
+ methods via ``\<^verbatim>\<open>,\<close>'' (sequential composition), ``\<^verbatim>\<open>;\<close>'' (structural
+ composition), ``\<^verbatim>\<open>|\<close>'' (alternative
+ choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
+ once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first
\<open>n\<close> subgoals). In practice, proof methods are usually just a comma
separated list of @{syntax nameref}~@{syntax args} specifications. Note
that parentheses may be dropped for single method specifications (with no
- arguments). The syntactic precedence of method combinators is @{verbatim
- "|"} @{verbatim ";"} @{verbatim ","} @{verbatim "[]"} @{verbatim "+"}
- @{verbatim "?"} (from low to high).
+ arguments). The syntactic precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close>
+ \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low to high).
@{rail \<open>
@{syntax_def method}:
@@ -627,7 +626,7 @@
elsewhere. Thus a proof method has no other chance than to operate on the
subgoals that are presently exposed.
- Structural composition ``\<open>m\<^sub>1\<close>@{verbatim ";"}~\<open>m\<^sub>2\<close>'' means
+ Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means
that method \<open>m\<^sub>1\<close> is applied with restriction to the first subgoal,
then \<open>m\<^sub>2\<close> is applied consecutively with restriction to each subgoal
that has newly emerged due to \<open>m\<^sub>1\<close>. This is analogous to the tactic
@@ -846,7 +845,7 @@
structure is not taken into account, i.e.\ meta-level implication is
considered atomic. This is the same principle underlying literal
facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command
- "note"}~@{verbatim "`"}\<open>\<phi>\<close>@{verbatim "`"}'' provided that
+ "note"}~\<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close>'' provided that
\<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close> in the
proof context.
--- a/src/Doc/Isar_Ref/Proof_Script.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Thu Oct 22 21:16:49 2015 +0200
@@ -111,7 +111,7 @@
to them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x
y z\<close>'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
"for"}~\<open>\<dots> x y z\<close>'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
- latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
+ latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol as notation. Parameter
positions may be skipped via dummies (underscore). Unspecified names
remain internal, and thus inaccessible in the proof text.
--- a/src/Doc/Isar_Ref/Spec.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu Oct 22 21:16:49 2015 +0200
@@ -93,14 +93,14 @@
order to make parsing of proof documents work properly. Command
keywords need to be classified according to their structural role in
the formal text. Examples may be seen in Isabelle/HOL sources
- itself, such as @{keyword "keywords"}~@{verbatim \<open>"typedef"\<close>}
- \<open>:: thy_goal\<close> or @{keyword "keywords"}~@{verbatim
- \<open>"datatype"\<close>} \<open>:: thy_decl\<close> for theory-level declarations
+ itself, such as @{keyword "keywords"}~\<^verbatim>\<open>"typedef"\<close>
+ \<open>:: thy_goal\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close>
+ for theory-level declarations
with and without proof, respectively. Additional @{syntax tags}
provide defaults for document preparation (\secref{sec:tags}).
- It is possible to specify an alternative completion via @{verbatim
- "=="}~\<open>text\<close>, while the default is the corresponding keyword name.
+ It is possible to specify an alternative completion via \<^verbatim>\<open>==\<close>~\<open>text\<close>,
+ while the default is the corresponding keyword name.
\<^descr> @{command (global) "end"} concludes the current theory
definition. Note that some other commands, e.g.\ local theory
@@ -495,9 +495,9 @@
Instances have an optional qualifier which applies to names in
declarations. Names include local definitions and theorem names.
If present, the qualifier itself is either optional
- (``@{verbatim "?"}''), which means that it may be omitted on input of the
- qualified name, or mandatory (``@{verbatim "!"}''). If neither
- ``@{verbatim "?"}'' nor ``@{verbatim "!"}'' are present, the command's default
+ (``\<^verbatim>\<open>?\<close>''), which means that it may be omitted on input of the
+ qualified name, or mandatory (``\<^verbatim>\<open>!\<close>''). If neither
+ ``\<^verbatim>\<open>?\<close>'' nor ``\<^verbatim>\<open>!\<close>'' are present, the command's default
is used. For @{command "interpretation"} and @{command "interpret"}
the default is ``mandatory'', for @{command "locale"} and @{command
"sublocale"} the default is ``optional''. Qualifiers play no role
--- a/src/Doc/Isar_Ref/Symbols.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Symbols.thy Thu Oct 22 21:16:49 2015 +0200
@@ -6,25 +6,24 @@
text \<open>
Isabelle supports an infinite number of non-ASCII symbols, which are
- represented in source text as @{verbatim \<open>\\<close>}@{verbatim "<"}\<open>name\<close>@{verbatim ">"} (where \<open>name\<close> may be any identifier). It
+ represented in source text as \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> (where \<open>name\<close> may be any identifier). It
is left to front-end tools how to present these symbols to the user.
The collection of predefined standard symbols given below is
available by default for Isabelle document output, due to
- appropriate definitions of @{verbatim \<open>\isasym\<close>}\<open>name\<close> for each @{verbatim \<open>\\<close>}@{verbatim "<"}\<open>name\<close>@{verbatim
- ">"} in the @{verbatim isabellesym.sty} file. Most of these symbols
+ appropriate definitions of \<^verbatim>\<open>\isasym\<close>\<open>name\<close> for each \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> in
+ the \<^verbatim>\<open>isabellesym.sty\<close> file. Most of these symbols
are displayed properly in Isabelle/jEdit and {\LaTeX} generated from Isabelle.
Moreover, any single symbol (or ASCII character) may be prefixed by
- @{verbatim "\<^sup>"} for superscript and @{verbatim "\<^sub>"} for subscript,
- such as @{verbatim "A\<^sup>\<star>"} for \<open>A\<^sup>\<star>\<close> and @{verbatim "A\<^sub>1"} for
+ \<^verbatim>\<open>\<^sup>\<close> for superscript and \<^verbatim>\<open>\<^sub>\<close> for subscript,
+ such as \<^verbatim>\<open>A\<^sup>\<star>\<close> for \<open>A\<^sup>\<star>\<close> and \<^verbatim>\<open>A\<^sub>1\<close> for
\<open>A\<^sub>1\<close>. Sub- and superscripts that span a region of text can
- be marked up with @{verbatim "\<^bsub>"}\<open>\<dots>\<close>@{verbatim
- "\<^esub>"} and @{verbatim "\<^bsup>"}\<open>\<dots>\<close>@{verbatim "\<^esup>"}
+ be marked up with \<^verbatim>\<open>\<^bsub>\<close>\<open>\<dots>\<close>\<^verbatim>\<open>\<^esub>\<close> and \<^verbatim>\<open>\<^bsup>\<close>\<open>\<dots>\<close>\<^verbatim>\<open>\<^esup>\<close>
respectively, but note that there are limitations in the typographic
rendering quality of this form. Furthermore, all ASCII characters
and most other symbols may be printed in bold by prefixing
- @{verbatim "\<^bold>"} such as @{verbatim "\<^bold>\<alpha>"} for \<open>\<^bold>\<alpha>\<close>. Note that
- @{verbatim "\<^sup>"}, @{verbatim "\<^sub>"}, @{verbatim "\<^bold>"} cannot be combined.
+ \<^verbatim>\<open>\<^bold>\<close> such as \<^verbatim>\<open>\<^bold>\<alpha>\<close> for \<open>\<^bold>\<alpha>\<close>. Note that
+ \<^verbatim>\<open>\<^sup>\<close>, \<^verbatim>\<open>\<^sub>\<close>, \<^verbatim>\<open>\<^bold>\<close> cannot be combined.
Further details of Isabelle document preparation are covered in
\chref{ch:document-prep}.
--- a/src/Doc/JEdit/JEdit.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Oct 22 21:16:49 2015 +0200
@@ -93,8 +93,8 @@
feedback via markup, which is rendered in the editor via colors, boxes,
squiggly underlines, hyperlinks, popup windows, icons, clickable output etc.
- Using the mouse together with the modifier key @{verbatim CONTROL} (Linux,
- Windows) or @{verbatim COMMAND} (Mac OS X) exposes additional formal content
+ Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux,
+ Windows) or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes additional formal content
via tooltips and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}).
Output (in popups etc.) may be explored recursively, using the same
techniques as in the editor source buffer.
@@ -113,8 +113,8 @@
standard Isabelle documentation: PDF files are opened by regular desktop
operations of the underlying platform. The section ``Original jEdit
Documentation'' contains the original \<^emph>\<open>User's Guide\<close> of this
- sophisticated text editor. The same is accessible via the @{verbatim Help}
- menu or @{verbatim F1} keyboard shortcut, using the built-in HTML viewer of
+ sophisticated text editor. The same is accessible via the \<^verbatim>\<open>Help\<close>
+ menu or \<^verbatim>\<open>F1\<close> keyboard shortcut, using the built-in HTML viewer of
Java/Swing. The latter also includes \<^emph>\<open>Frequently Asked Questions\<close> and
documentation of individual plugins.
@@ -201,7 +201,7 @@
text \<open>Keyboard shortcuts used to be managed as jEdit properties in
the past, but recent versions (2013) have a separate concept of
\<^emph>\<open>keymap\<close> that is configurable via \<^emph>\<open>Global Options~/
- Shortcuts\<close>. The @{verbatim imported} keymap is derived from the
+ Shortcuts\<close>. The \<^verbatim>\<open>imported\<close> keymap is derived from the
initial environment of properties that is available at the first
start of the editor; afterwards the keymap file takes precedence.
@@ -209,7 +209,7 @@
properties, and additional keyboard shortcuts for Isabelle-specific
functionality. Users may change their keymap later, but need to copy some
keyboard shortcuts manually (see also @{file_unchecked
- "$ISABELLE_HOME_USER/jedit/keymaps"} versus @{verbatim shortcut} properties
+ "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties
in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
\<close>
@@ -239,30 +239,30 @@
Start jEdit with Isabelle plugin setup and open theory FILES
(default "$USER_HOME/Scratch.thy").\<close>}
- The @{verbatim "-l"} option specifies the session name of the logic
+ The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic
image to be used for proof processing. Additional session root
- directories may be included via option @{verbatim "-d"} to augment
+ directories may be included via option \<^verbatim>\<open>-d\<close> to augment
that name space of @{tool build} @{cite "isabelle-system"}.
By default, the specified image is checked and built on demand. The
- @{verbatim "-s"} option determines where to store the result session image
- of @{tool build}. The @{verbatim "-n"} option bypasses the implicit build
+ \<^verbatim>\<open>-s\<close> option determines where to store the result session image
+ of @{tool build}. The \<^verbatim>\<open>-n\<close> option bypasses the implicit build
process for the selected session image.
- The @{verbatim "-m"} option specifies additional print modes for the prover
+ The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover
process. Note that the system option @{system_option_ref jedit_print_mode}
allows to do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close>
dialog of Isabelle/jEdit), without requiring command-line invocation.
- The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass additional
+ The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options allow to pass additional
low-level options to the JVM or jEdit, respectively. The defaults are
provided by the Isabelle settings environment @{cite "isabelle-system"}, but
note that these only work for the command-line tool described here, and not
the regular application.
- The @{verbatim "-b"} and @{verbatim "-f"} options control the self-build
+ The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build
mechanism of Isabelle/jEdit. This is only relevant for building from
- sources, which also requires an auxiliary @{verbatim jedit_build} component
+ sources, which also requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component
from @{url "http://isabelle.in.tum.de/components"}. The official
Isabelle release already includes a pre-built version of Isabelle/jEdit.
\<close>
@@ -445,10 +445,10 @@
or Bi-directional Text.} See also @{cite "Wenzel:2011:CICM"}.
For the prover back-end, formal text consists of ASCII characters that are
- grouped according to some simple rules, e.g.\ as plain ``@{verbatim a}'' or
- symbolic ``@{verbatim "\<alpha>"}''. For the editor front-end, a certain subset of
+ grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or
+ symbolic ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of
symbols is rendered physically via Unicode glyphs, in order to show
- ``@{verbatim "\<alpha>"}'' as ``\<open>\<alpha>\<close>'', for example. This symbol
+ ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for example. This symbol
interpretation is specified by the Isabelle system distribution in @{file
"$ISABELLE_HOME/etc/symbols"} and may be augmented by the user in
@{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
@@ -456,7 +456,7 @@
The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
standard interpretation of finitely many symbols from the infinite
collection. Uninterpreted symbols are displayed literally, e.g.\
- ``@{verbatim "\<foobar>"}''. Overlap of Unicode characters used in symbol
+ ``\<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol
interpretation with informal ones (which might appear e.g.\ in comments)
needs to be avoided. Raw Unicode characters within prover source files
should be restricted to informal parts, e.g.\ to write text in non-latin
@@ -464,12 +464,12 @@
\<^medskip>
\paragraph{Encoding.} Technically, the Unicode view on Isabelle
- symbols is an \<^emph>\<open>encoding\<close> called @{verbatim "UTF-8-Isabelle"} in jEdit
+ symbols is an \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit
(not in the underlying JVM). It is provided by the Isabelle/jEdit plugin and
enabled by default for all source files. Sometimes such defaults are reset
accidentally, or malformed UTF-8 sequences in the text force jEdit to fall
- back on a different encoding like @{verbatim "ISO-8859-15"}. In that case,
- verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer instead of its
+ back on a different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case,
+ verbatim ``\<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text buffer instead of its
Unicode rendering ``\<open>\<alpha>\<close>''. The jEdit menu operation \<^emph>\<open>File~/
Reload with Encoding~/ UTF-8-Isabelle\<close> helps to resolve such problems (after
repairing malformed parts of the text).
@@ -478,18 +478,18 @@
\paragraph{Font.} Correct rendering via Unicode requires a
font that contains glyphs for the corresponding codepoints. Most
system fonts lack that, so Isabelle/jEdit prefers its own
- application font @{verbatim IsabelleText}, which ensures that
+ application font \<^verbatim>\<open>IsabelleText\<close>, which ensures that
standard collection of Isabelle symbols are actually seen on the
screen (or printer).
Note that a Java/AWT/Swing application can load additional fonts only if
they are not installed on the operating system already! Some outdated
- version of @{verbatim IsabelleText} that happens to be provided by the
+ version of \<^verbatim>\<open>IsabelleText\<close> that happens to be provided by the
operating system would prevent Isabelle/jEdit to use its bundled version.
This could lead to missing glyphs (black rectangles), when the system
- version of @{verbatim IsabelleText} is older than the application version.
+ version of \<^verbatim>\<open>IsabelleText\<close> is older than the application version.
This problem can be avoided by refraining to ``install'' any version of
- @{verbatim IsabelleText} in the first place, although it is occasionally
+ \<^verbatim>\<open>IsabelleText\<close> in the first place, although it is occasionally
tempting to use the same font in other applications.
\<^medskip>
@@ -518,17 +518,17 @@
\<^enum> Copy/paste from prover output within Isabelle/jEdit. The same
principles as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary
- Isabelle/jEdit windows works via the keyboard shortcuts @{verbatim "C+c"} or
- @{verbatim "C+INSERT"}, while jEdit menu actions always refer to the primary
+ Isabelle/jEdit windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or
+ \<^verbatim>\<open>C+INSERT\<close>, while jEdit menu actions always refer to the primary
text area!
\<^enum> Completion provided by Isabelle plugin (see
\secref{sec:completion}). Isabelle symbols have a canonical name
and optional abbreviations. This can be used with the text
completion mechanism of Isabelle/jEdit, to replace a prefix of the
- actual symbol like @{verbatim "\<lambda>"}, or its name preceded by backslash
- @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
- @{verbatim "%"} by the Unicode rendering.
+ actual symbol like \<^verbatim>\<open>\<lambda>\<close>, or its name preceded by backslash
+ \<^verbatim>\<open>\\<close>\<^verbatim>\<open>lambda\<close>, or its ASCII abbreviation
+ \<^verbatim>\<open>%\<close> by the Unicode rendering.
The following table is an extract of the information provided by the
standard @{file "$ISABELLE_HOME/etc/symbols"} file:
@@ -536,32 +536,32 @@
\<^medskip>
\begin{tabular}{lll}
\<^bold>\<open>symbol\<close> & \<^bold>\<open>name with backslash\<close> & \<^bold>\<open>abbreviation\<close> \\\hline
- \<open>\<lambda>\<close> & @{verbatim "\\lambda"} & @{verbatim "%"} \\
- \<open>\<Rightarrow>\<close> & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\
- \<open>\<Longrightarrow>\<close> & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex]
- \<open>\<And>\<close> & @{verbatim "\\And"} & @{verbatim "!!"} \\
- \<open>\<equiv>\<close> & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex]
- \<open>\<forall>\<close> & @{verbatim "\\forall"} & @{verbatim "!"} \\
- \<open>\<exists>\<close> & @{verbatim "\\exists"} & @{verbatim "?"} \\
- \<open>\<longrightarrow>\<close> & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\
- \<open>\<and>\<close> & @{verbatim "\\and"} & @{verbatim "&"} \\
- \<open>\<or>\<close> & @{verbatim "\\or"} & @{verbatim "|"} \\
- \<open>\<not>\<close> & @{verbatim "\\not"} & @{verbatim "~"} \\
- \<open>\<noteq>\<close> & @{verbatim "\\noteq"} & @{verbatim "~="} \\
- \<open>\<in>\<close> & @{verbatim "\\in"} & @{verbatim ":"} \\
- \<open>\<notin>\<close> & @{verbatim "\\notin"} & @{verbatim "~:"} \\
+ \<open>\<lambda>\<close> & \<^verbatim>\<open>\lambda\<close> & \<^verbatim>\<open>%\<close> \\
+ \<open>\<Rightarrow>\<close> & \<^verbatim>\<open>\Rightarrow\<close> & \<^verbatim>\<open>=>\<close> \\
+ \<open>\<Longrightarrow>\<close> & \<^verbatim>\<open>\Longrightarrow\<close> & \<^verbatim>\<open>==>\<close> \\[0.5ex]
+ \<open>\<And>\<close> & \<^verbatim>\<open>\And\<close> & \<^verbatim>\<open>!!\<close> \\
+ \<open>\<equiv>\<close> & \<^verbatim>\<open>\equiv\<close> & \<^verbatim>\<open>==\<close> \\[0.5ex]
+ \<open>\<forall>\<close> & \<^verbatim>\<open>\forall\<close> & \<^verbatim>\<open>!\<close> \\
+ \<open>\<exists>\<close> & \<^verbatim>\<open>\exists\<close> & \<^verbatim>\<open>?\<close> \\
+ \<open>\<longrightarrow>\<close> & \<^verbatim>\<open>\longrightarrow\<close> & \<^verbatim>\<open>-->\<close> \\
+ \<open>\<and>\<close> & \<^verbatim>\<open>\and\<close> & \<^verbatim>\<open>&\<close> \\
+ \<open>\<or>\<close> & \<^verbatim>\<open>\or\<close> & \<^verbatim>\<open>|\<close> \\
+ \<open>\<not>\<close> & \<^verbatim>\<open>\not\<close> & \<^verbatim>\<open>~\<close> \\
+ \<open>\<noteq>\<close> & \<^verbatim>\<open>\noteq\<close> & \<^verbatim>\<open>~=\<close> \\
+ \<open>\<in>\<close> & \<^verbatim>\<open>\in\<close> & \<^verbatim>\<open>:\<close> \\
+ \<open>\<notin>\<close> & \<^verbatim>\<open>\notin\<close> & \<^verbatim>\<open>~:\<close> \\
\end{tabular}
\<^medskip>
Note that the above abbreviations refer to the input method. The logical
notation provides ASCII alternatives that often coincide, but sometimes
deviate. This occasionally causes user confusion with very old-fashioned
- Isabelle source that use ASCII replacement notation like @{verbatim "!"} or
- @{verbatim "ALL"} directly in the text.
+ Isabelle source that use ASCII replacement notation like \<^verbatim>\<open>!\<close> or
+ \<^verbatim>\<open>ALL\<close> directly in the text.
On the other hand, coincidence of symbol abbreviations with ASCII
replacement syntax syntax helps to update old theory sources via
- explicit completion (see also @{verbatim "C+b"} explained in
+ explicit completion (see also \<^verbatim>\<open>C+b\<close> explained in
\secref{sec:completion}).
@@ -576,17 +576,16 @@
\<^medskip>
\begin{tabular}{llll}
\<^bold>\<open>style\<close> & \<^bold>\<open>symbol\<close> & \<^bold>\<open>shortcut\<close> & \<^bold>\<open>action\<close> \\\hline
- superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action_ref "isabelle.control-sup"} \\
- subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action_ref "isabelle.control-sub"} \\
- bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action_ref "isabelle.control-bold"} \\
- emphasized & @{verbatim "\<^emph>"} & @{verbatim "C+e LEF"} & @{action_ref "isabelle.control-emph"} \\
- reset & & @{verbatim "C+e BACK_SPACE"} & @{action_ref "isabelle.control-reset"} \\
+ superscript & \<^verbatim>\<open>\<^sup>\<close> & \<^verbatim>\<open>C+e UP\<close> & @{action_ref "isabelle.control-sup"} \\
+ subscript & \<^verbatim>\<open>\<^sub>\<close> & \<^verbatim>\<open>C+e DOWN\<close> & @{action_ref "isabelle.control-sub"} \\
+ bold face & \<^verbatim>\<open>\<^bold>\<close> & \<^verbatim>\<open>C+e RIGHT\<close> & @{action_ref "isabelle.control-bold"} \\
+ emphasized & \<^verbatim>\<open>\<^emph>\<close> & \<^verbatim>\<open>C+e LEFT\<close> & @{action_ref "isabelle.control-emph"} \\
+ reset & & \<^verbatim>\<open>C+e BACK_SPACE\<close> & @{action_ref "isabelle.control-reset"} \\
\end{tabular}
\<^medskip>
To produce a single control symbol, it is also possible to complete on
- @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub}, @{verbatim
- "\\"}@{verbatim bold}, @{verbatim "\\"}@{verbatim emph} as for regular
+ \<^verbatim>\<open>\\<close>\<^verbatim>\<open>sup\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>sub\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>bold\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>emph\<close> as for regular
symbols.
The emphasized style only takes effect in document output, not in the
@@ -601,9 +600,9 @@
structure in a tree view.
Isabelle/jEdit provides SideKick parsers for its main mode for theory files,
- as well as some minor modes for the @{verbatim NEWS} file (see
- \figref{fig:sidekick}), session @{verbatim ROOT} files, and system
- @{verbatim options}.
+ as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file (see
+ \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, and system
+ \<^verbatim>\<open>options\<close>.
\begin{figure}[htb]
\begin{center}
@@ -613,7 +612,7 @@
\label{fig:sidekick}
\end{figure}
- Moreover, the special SideKick parser @{verbatim "isabelle-markup"}
+ Moreover, the special SideKick parser \<^verbatim>\<open>isabelle-markup\<close>
provides access to the full (uninterpreted) markup tree of the PIDE
document model of the current buffer. This is occasionally useful
for informative purposes, but the amount of displayed information
@@ -628,19 +627,19 @@
The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters),
e.g.\ \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and
the cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar
- functionality than the Emacs buffers @{verbatim "*scratch*"} and
- @{verbatim "*shell*"}.
+ functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and
+ \<^verbatim>\<open>*shell*\<close>.
Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which
is the regular Scala toplevel loop running inside the same JVM process as
Isabelle/jEdit itself. This means the Scala command interpreter has access
to the JVM name space and state of the running Prover IDE application. The
- default environment imports the full content of packages @{verbatim
- "isabelle"} and @{verbatim "isabelle.jedit"}.
+ default environment imports the full content of packages \<^verbatim>\<open>isabelle\<close> and
+ \<^verbatim>\<open>isabelle.jedit\<close>.
- For example, @{verbatim PIDE} refers to the Isabelle/jEdit plugin object,
- and @{verbatim view} to the current editor view of jEdit. The Scala
- expression @{verbatim "PIDE.snapshot(view)"} makes a PIDE document snapshot
+ For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object,
+ and \<^verbatim>\<open>view\<close> to the current editor view of jEdit. The Scala
+ expression \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot
of the current buffer within the current editor view.
This helps to explore Isabelle/Scala functionality interactively. Some care
@@ -654,8 +653,8 @@
text \<open>
File specifications in jEdit follow various formats and conventions
according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by
- additional plugins. This allows to access remote files via the @{verbatim
- "http:"} protocol prefix, for example. Isabelle/jEdit attempts to work with
+ additional plugins. This allows to access remote files via the \<^verbatim>\<open>http:\<close>
+ protocol prefix, for example. Isabelle/jEdit attempts to work with
the file-system model of jEdit as far as possible. In particular, theory
sources are passed directly from the editor to the prover, without
indirection via physical files.
@@ -686,8 +685,8 @@
wrapper, in contrast to @{tool jedit} run from the command line
(\secref{sec:command-line}).
- Isabelle/jEdit imitates @{verbatim "$ISABELLE_HOME"} and @{verbatim
- "$ISABELLE_HOME_USER"} within the Java process environment, in order to
+ Isabelle/jEdit imitates \<^verbatim>\<open>$ISABELLE_HOME\<close> and \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> within
+ the Java process environment, in order to
allow easy access to these important places from the editor. The file
browser of jEdit also includes \<^emph>\<open>Favorites\<close> for these two important
locations.
@@ -733,9 +732,9 @@
\<^medskip>
\begin{tabular}{lll}
\<^bold>\<open>mode\<close> & \<^bold>\<open>file extension\<close> & \<^bold>\<open>content\<close> \\\hline
- @{verbatim "isabelle"} & @{verbatim ".thy"} & theory source \\
- @{verbatim "isabelle-ml"} & @{verbatim ".ML"} & Isabelle/ML source \\
- @{verbatim "sml"} & @{verbatim ".sml"} or @{verbatim ".sig"} & Standard ML source \\
+ \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>.thy\<close> & theory source \\
+ \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>.ML\<close> & Isabelle/ML source \\
+ \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>.sml\<close> or \<^verbatim>\<open>.sig\<close> & Standard ML source \\
\end{tabular}
\<^medskip>
@@ -837,7 +836,7 @@
document-model on demand, the first time when opened explicitly in the
editor. There are further tricks to manage markup of ML files, such that
Isabelle/HOL may be edited conveniently in the Prover IDE on small machines
- with only 8\,GB of main memory. Using @{verbatim Pure} as logic session
+ with only 8\,GB of main memory. Using \<^verbatim>\<open>Pure\<close> as logic session
image, the exploration may start at the top @{file
"$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file
"$ISABELLE_HOME/src/HOL/HOL.thy"}, for example.
@@ -1046,8 +1045,8 @@
text \<open>
Formally processed text (prover input or output) contains rich markup
- information that can be explored further by using the @{verbatim CONTROL}
- modifier key on Linux and Windows, or @{verbatim COMMAND} on Mac OS X.
+ information that can be explored further by using the \<^verbatim>\<open>CONTROL\<close>
+ modifier key on Linux and Windows, or \<^verbatim>\<open>COMMAND\<close> on Mac OS X.
Hovering with the mouse while the modifier is pressed reveals a
\<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup) and/or a
\<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse
@@ -1075,14 +1074,14 @@
The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or
\<^emph>\<open>detach\<close> the window, turning it into a separate \<^emph>\<open>Info\<close>
- window managed by jEdit. The @{verbatim ESCAPE} key closes
+ window managed by jEdit. The \<^verbatim>\<open>ESCAPE\<close> key closes
\<^emph>\<open>all\<close> popups, which is particularly relevant when nested
tooltips are stacking up.
\<^medskip>
A black rectangle in the text indicates a hyperlink that may be
- followed by a mouse click (while the @{verbatim CONTROL} or @{verbatim
- COMMAND} modifier key is still pressed). Such jumps to other text locations
+ followed by a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier
+ key is still pressed). Such jumps to other text locations
are recorded by the \<^emph>\<open>Navigator\<close> plugin, which is bundled with
Isabelle/jEdit and enabled by default, including navigation arrows in the
main jEdit toolbar.
@@ -1106,9 +1105,8 @@
\<^medskip>
\<^emph>\<open>Explicit completion\<close> is triggered by the action @{action_ref
- "isabelle.complete"}, which is bound to the keyboard shortcut @{verbatim
- "C+b"}, and thus overrides the jEdit default for @{action_ref
- "complete-word"}.
+ "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\<open>C+b\<close>,
+ and thus overrides the jEdit default for @{action_ref "complete-word"}.
\<^emph>\<open>Implicit completion\<close> hooks into the regular keyboard input stream of
the editor, with some event filtering and optional delays.
@@ -1139,16 +1137,16 @@
kinds and purposes. The completion mechanism supports this by the following
built-in templates:
- \<^descr> @{verbatim "`"} (single ASCII back-quote) supports \<^emph>\<open>quotations\<close>
+ \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) supports \<^emph>\<open>quotations\<close>
via text cartouches. There are three selections, which are always presented
in the same order and do not depend on any context information. The default
choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the box indicates the
cursor position after insertion; the other choices help to repair the block
structure of unbalanced text cartouches.
- \<^descr> @{verbatim "@{"} is completed to the template ``\<open>@{\<box>}\<close>'',
+ \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'',
where the box indicates the cursor position after insertion. Here it is
- convenient to use the wildcard ``@{verbatim __}'' or a more specific name
+ convenient to use the wildcard ``\<^verbatim>\<open>__\<close>'' or a more specific name
prefix to let semantic completion of name-space entries propose
antiquotation names.
@@ -1191,19 +1189,19 @@
\<^medskip>
\begin{tabular}{ll}
\<^bold>\<open>completion entry\<close> & \<^bold>\<open>example\<close> \\\hline
- literal symbol & @{verbatim "\<forall>"} \\
- symbol name with backslash & @{verbatim "\\"}@{verbatim forall} \\
- symbol abbreviation & @{verbatim "ALL"} or @{verbatim "!"} \\
+ literal symbol & \<^verbatim>\<open>\<forall>\<close> \\
+ symbol name with backslash & \<^verbatim>\<open>\\<close>\<^verbatim>\<open>forall\<close> \\
+ symbol abbreviation & \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>!\<close> \\
\end{tabular}
\<^medskip>
When inserted into the text, the above examples all produce the same Unicode
- rendering \<open>\<forall>\<close> of the underlying symbol @{verbatim "\<forall>"}.
+ rendering \<open>\<forall>\<close> of the underlying symbol \<^verbatim>\<open>\<forall>\<close>.
- A symbol abbreviation that is a plain word, like @{verbatim "ALL"}, is
- treated like a syntax keyword. Non-word abbreviations like @{verbatim "-->"}
+ A symbol abbreviation that is a plain word, like \<^verbatim>\<open>ALL\<close>, is
+ treated like a syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close>
are inserted more aggressively, except for single-character abbreviations
- like @{verbatim "!"} above.
+ like \<^verbatim>\<open>!\<close> above.
\<^medskip>
Symbol completion depends on the semantic language context
@@ -1227,11 +1225,11 @@
Already recognized names are \<^emph>\<open>not\<close> completed further, but completion
may be extended by appending a suffix of underscores. This provokes a failed
lookup, and another completion attempt while ignoring the underscores. For
- example, in a name space where @{verbatim "foo"} and @{verbatim "foobar"}
- are known, the input @{verbatim "foo"} remains unchanged, but @{verbatim
- "foo_"} may be completed to @{verbatim "foo"} or @{verbatim "foobar"}.
+ example, in a name space where \<^verbatim>\<open>foo\<close> and \<^verbatim>\<open>foobar\<close>
+ are known, the input \<^verbatim>\<open>foo\<close> remains unchanged, but \<^verbatim>\<open>foo_\<close> may be completed
+ to \<^verbatim>\<open>foo\<close> or \<^verbatim>\<open>foobar\<close>.
- The special identifier ``@{verbatim "__"}'' serves as a wild-card for
+ The special identifier ``\<^verbatim>\<open>__\<close>'' serves as a wild-card for
arbitrary completion: it exposes the name-space content to the completion
mechanism (truncated according to @{system_option completion_limit}). This
is occasionally useful to explore an unknown name-space, e.g.\ in some
@@ -1278,7 +1276,7 @@
Instead of the specific @{action_ref "isabelle.complete-word"}, it is also
possible to use the generic @{action_ref "isabelle.complete"} with its
- default keyboard shortcut @{verbatim "C+b"}.
+ default keyboard shortcut \<^verbatim>\<open>C+b\<close>.
\<^medskip>
Dictionary lookup uses some educated guesses about lower-case,
@@ -1305,12 +1303,12 @@
The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional
situations, to tell that some language keywords should be excluded from
- further completion attempts. For example, @{verbatim ":"} within accepted
+ further completion attempts. For example, \<^verbatim>\<open>:\<close> within accepted
Isar syntax looses its meaning as abbreviation for symbol \<open>\<in>\<close>.
\<^medskip>
The completion context is \<^emph>\<open>ignored\<close> for built-in templates and
- symbols in their explicit form ``@{verbatim "\<foobar>"}''; see also
+ symbols in their explicit form ``\<^verbatim>\<open>\<foobar>\<close>''; see also
\secref{sec:completion-varieties}. This allows to complete within broken
input that escapes its normal semantic context, e.g.\ antiquotations or
string literals in ML, which do not allow arbitrary backslash sequences.
@@ -1325,7 +1323,7 @@
jedit_completion_delay}.
\<^descr>[Explicit completion] works via action @{action_ref
- "isabelle.complete"} with keyboard shortcut @{verbatim "C+b"}. This
+ "isabelle.complete"} with keyboard shortcut \<^verbatim>\<open>C+b\<close>. This
overrides the shortcut for @{action_ref "complete-word"} in jEdit, but it is
possible to restore the original jEdit keyboard mapping of @{action
"complete-word"} via \<^emph>\<open>Global Options~/ Shortcuts\<close> and invent a
@@ -1368,9 +1366,9 @@
text area that offers a selection of completion items to be inserted into
the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to
the frequency of selection, with persistent history. The popup may interpret
- special keys @{verbatim ENTER}, @{verbatim TAB}, @{verbatim ESCAPE},
- @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP}, @{verbatim
- PAGE_DOWN}, but all other key events are passed to the underlying text area.
+ special keys \<^verbatim>\<open>ENTER\<close>, \<^verbatim>\<open>TAB\<close>, \<^verbatim>\<open>ESCAPE\<close>,
+ \<^verbatim>\<open>UP\<close>, \<^verbatim>\<open>DOWN\<close>, \<^verbatim>\<open>PAGE_UP\<close>, \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are
+ passed to the underlying text area.
This allows to ignore unwanted completions most of the time and continue
typing quickly. Thus the popup serves as a mechanism of confirmation of
proposed items, but the default is to continue without completion.
@@ -1380,13 +1378,13 @@
\<^medskip>
\begin{tabular}{ll}
\<^bold>\<open>key\<close> & \<^bold>\<open>action\<close> \\\hline
- @{verbatim "ENTER"} & select completion (if @{system_option jedit_completion_select_enter}) \\
- @{verbatim "TAB"} & select completion (if @{system_option jedit_completion_select_tab}) \\
- @{verbatim "ESCAPE"} & dismiss popup \\
- @{verbatim "UP"} & move up one item \\
- @{verbatim "DOWN"} & move down one item \\
- @{verbatim "PAGE_UP"} & move up one page of items \\
- @{verbatim "PAGE_DOWN"} & move down one page of items \\
+ \<^verbatim>\<open>ENTER\<close> & select completion (if @{system_option jedit_completion_select_enter}) \\
+ \<^verbatim>\<open>TAB\<close> & select completion (if @{system_option jedit_completion_select_tab}) \\
+ \<^verbatim>\<open>ESCAPE\<close> & dismiss popup \\
+ \<^verbatim>\<open>UP\<close> & move up one item \\
+ \<^verbatim>\<open>DOWN\<close> & move down one item \\
+ \<^verbatim>\<open>PAGE_UP\<close> & move up one page of items \\
+ \<^verbatim>\<open>PAGE_DOWN\<close> & move down one page of items \\
\end{tabular}
\<^medskip>
@@ -1424,15 +1422,15 @@
Support for multiple selections is particularly useful for
\<^emph>\<open>HyperSearch\<close>: clicking on one of the items in the \<^emph>\<open>HyperSearch
Results\<close> window makes jEdit select all its occurrences in the corresponding
- line of text. Then explicit completion can be invoked via @{verbatim "C+b"},
- e.g.\ to replace occurrences of @{verbatim "-->"} by \<open>\<longrightarrow>\<close>.
+ line of text. Then explicit completion can be invoked via \<^verbatim>\<open>C+b\<close>,
+ e.g.\ to replace occurrences of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>.
\<^medskip>
Insertion works by removing and inserting pieces of text from the
buffer. This counts as one atomic operation on the jEdit history. Thus
unintended completions may be reverted by the regular @{action undo} action
of jEdit. According to normal jEdit policies, the recovered text after
- @{action undo} is selected: @{verbatim ESCAPE} is required to reset the
+ @{action undo} is selected: \<^verbatim>\<open>ESCAPE\<close> is required to reset the
selection and to continue typing more text.
\<close>
@@ -1466,11 +1464,10 @@
jedit_completion_immediate} determine the handling of keyboard events for
implicit completion (\secref{sec:completion-input}).
- A @{system_option jedit_completion_delay}~@{verbatim "> 0"} postpones the
+ A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the
processing of key events, until after the user has stopped typing for the
- given time span, but @{system_option jedit_completion_immediate}~@{verbatim
- "= true"} means that abbreviations of Isabelle symbols are handled
- nonetheless.
+ given time span, but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>"= true\<close>
+ means that abbreviations of Isabelle symbols are handled nonetheless.
\<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob''
patterns to ignore in file-system path completion (separated by colons),
@@ -1650,14 +1647,14 @@
It is also possible to use text folding according to this structure, by
adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The
- default mode @{verbatim isabelle} uses the structure of formal definitions,
- statements, and proofs. The alternative mode @{verbatim sidekick} uses the
+ default mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions,
+ statements, and proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the
document structure of the SideKick parser, as explained above.\<close>
section \<open>Citations and Bib{\TeX} entries\<close>
-text \<open>Citations are managed by {\LaTeX} and Bib{\TeX} in @{verbatim ".bib"}
+text \<open>Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close>
files. The Isabelle session build process and the @{tool latex} tool @{cite
"isabelle-system"} are smart enough to assemble the result, based on the
session directory layout.
@@ -1666,9 +1663,8 @@
"isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for
tooltips, hyperlinks, and completion for Bib{\TeX} database entries.
Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment
- used in {\LaTeX} batch-mode, but it can take citations from those @{verbatim
- ".bib"} files that happen to be open in the editor; see
- \figref{fig:cite-completion}.
+ used in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close>
+ files that happen to be open in the editor; see \figref{fig:cite-completion}.
\begin{figure}[htb]
\begin{center}
@@ -1678,7 +1674,7 @@
\label{fig:cite-completion}
\end{figure}
- Isabelle/jEdit also provides some support for editing @{verbatim ".bib"}
+ Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close>
files themselves. There is syntax highlighting based on entry types
(according to standard Bib{\TeX} styles), a context-menu to compose entries
systematically, and a SideKick tree view of the overall content; see
@@ -1717,7 +1713,7 @@
It is also possible to reveal individual timing information via some
tooltip for the corresponding command keyword, using the technique
- of mouse hovering with @{verbatim CONTROL}/@{verbatim COMMAND}
+ of mouse hovering with \<^verbatim>\<open>CONTROL\<close>/\<^verbatim>\<open>COMMAND\<close>
modifier key as explained in \secref{sec:tooltips-hyperlinks}.
Actual display of timing depends on the global option
@{system_option_ref jedit_timing_threshold}, which can be configured in
@@ -1729,9 +1725,9 @@
system. The display is continuously updated according to @{system_option_ref
editor_chart_delay}. Note that the painting of the chart takes considerable
runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not
- Isabelle/ML. Internally, the Isabelle/Scala module @{verbatim
- isabelle.ML_Statistics} provides further access to statistics of
- Isabelle/ML.\<close>
+ Isabelle/ML. Internally, the Isabelle/Scala module \<^verbatim>\<open>isabelle.ML_Statistics\<close>
+ provides further access to statistics of Isabelle/ML.
+\<close>
section \<open>Low-level output\<close>
@@ -1752,8 +1748,8 @@
it is important to undock all \<^emph>\<open>Protocol\<close> panels for production
work.
- \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the @{verbatim
- stdout} and @{verbatim stderr} channels of the prover process.
+ \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close>
+ channels of the prover process.
Recording of output starts with the first activation of the
corresponding dockable window; earlier output is lost.
@@ -1771,7 +1767,7 @@
\<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose
problems with the startup or shutdown phase of the prover process; this also
- includes raw output on @{verbatim stderr}. Isabelle/ML also provides an
+ includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an
explicit @{ML Output.system_message} operation, which is occasionally useful
for diagnostic purposes within the system infrastructure itself.
@@ -1800,39 +1796,39 @@
\<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close
\<^emph>\<open>without\<close> saving changes.
- \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts @{verbatim "C+PLUS"} and
- @{verbatim "C+MINUS"} for adjusting the editor font size depend on
+ \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and
+ \<^verbatim>\<open>C+MINUS\<close> for adjusting the editor font size depend on
platform details and national keyboards.
\<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/
Shortcuts\<close>.
- \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence @{verbatim
- "COMMAND+COMMA"} for application \<^emph>\<open>Preferences\<close> is in conflict with the
+ \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application
+ \<^emph>\<open>Preferences\<close> is in conflict with the
jEdit default keyboard shortcut for \<^emph>\<open>Incremental Search Bar\<close> (action
@{action_ref "quick-search"}).
\<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/
- Shortcuts\<close> according to national keyboard, e.g.\ @{verbatim
- "COMMAND+SLASH"} on English ones.
+ Shortcuts\<close> according to national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close>
+ on English ones.
\<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to
character drop-outs in the main text area.
- \<^bold>\<open>Workaround:\<close> Use the default @{verbatim IsabelleText} font.
+ \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
(Do not install that font on the system.)
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus
tend to disrupt key event handling of Java/AWT/Swing.
\<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment
- variable @{verbatim XMODIFIERS} is reset by default within Isabelle
+ variable \<^verbatim>\<open>XMODIFIERS\<close> is reset by default within Isabelle
settings.
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 window managers that are
not ``re-parenting'' cause problems with additional windows opened
by Java. This affects either historic or neo-minimalistic window
- managers like @{verbatim awesome} or @{verbatim xmonad}.
+ managers like \<^verbatim>\<open>awesome\<close> or \<^verbatim>\<open>xmonad\<close>.
\<^bold>\<open>Workaround:\<close> Use a regular re-parenting X11 window manager.
@@ -1849,7 +1845,7 @@
primary and secondary font as explained in \secref{sec:hdpi}.
\<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref
- "toggle-full-screen"} (default keyboard shortcut @{verbatim F11}) works on
+ "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on
Windows, but not on Mac OS X or various Linux/X11 window managers.
\<^bold>\<open>Workaround:\<close> Use native full-screen control of the window
--- a/src/Doc/System/Basics.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/System/Basics.thy Thu Oct 22 21:16:49 2015 +0200
@@ -93,8 +93,7 @@
\<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
exists) is run in the same way as the site default settings. Note
that the variable @{setting ISABELLE_HOME_USER} has already been set
- before --- usually to something like @{verbatim
- "$USER_HOME/.isabelle/IsabelleXXXX"}.
+ before --- usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
Thus individual users may override the site-wide defaults.
Typically, a user settings file contains only a few lines, with some
@@ -103,8 +102,8 @@
Since settings files are regular GNU @{executable_def bash} scripts,
- one may use complex shell commands, such as @{verbatim "if"} or
- @{verbatim "case"} statements to set variables depending on the
+ one may use complex shell commands, such as \<^verbatim>\<open>if\<close> or
+ \<^verbatim>\<open>case\<close> statements to set variables depending on the
system architecture or other environment variables. Such advanced
features should be added only with great care, though. In
particular, external environment references should be kept at a
@@ -157,12 +156,12 @@
circumstances this may be changed in the global setting file.
Typically, the @{setting ISABELLE_HOME_USER} directory mimics
@{setting ISABELLE_HOME} to some extend. In particular, site-wide
- defaults may be overridden by a private @{verbatim
- "$ISABELLE_HOME_USER/etc/settings"}.
+ defaults may be overridden by a private
+ \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
\<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is
- automatically set to the general platform family: @{verbatim linux},
- @{verbatim macos}, @{verbatim windows}. Note that
+ automatically set to the general platform family: \<^verbatim>\<open>linux\<close>,
+ \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
platform-dependent tools usually need to refer to the more specific
identification according to @{setting ISABELLE_PLATFORM}, @{setting
ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
@@ -190,8 +189,7 @@
on the current search path of the shell.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers
- to the name of this Isabelle distribution, e.g.\ ``@{verbatim
- Isabelle2012}''.
+ to the name of this Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
@{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
@@ -208,7 +206,7 @@
automatically obtained by composing the values of @{setting
ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
- \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is @{verbatim true}
+ \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is \<^verbatim>\<open>true\<close>
for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to
SML/NJ where it is empty. This is particularly useful with the
build option @{system_option condition}
@@ -216,10 +214,10 @@
that SML/NJ can still handle.
\<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
- (Java Development Kit) installation with @{verbatim javac} and
- @{verbatim jar} executables. This is essential for Isabelle/Scala
+ (Java Development Kit) installation with \<^verbatim>\<open>javac\<close> and
+ \<^verbatim>\<open>jar\<close> executables. This is essential for Isabelle/Scala
and other JVM-based tools to work properly. Note that conventional
- @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime
+ \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
Environment), not JDK.
\<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories
@@ -238,7 +236,7 @@
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
load if none is given explicitely by the user. The default value is
- @{verbatim HOL}.
+ \<^verbatim>\<open>HOL\<close>.
\<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the
line editor for the @{tool_ref console} interface.
@@ -256,10 +254,10 @@
directories with documentation files.
\<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used
- for displaying @{verbatim pdf} files.
+ for displaying \<^verbatim>\<open>pdf\<close> files.
\<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used
- for displaying @{verbatim dvi} files.
+ for displaying \<^verbatim>\<open>dvi\<close> files.
\<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the
prefix from which any running @{executable "isabelle_process"}
@@ -274,11 +272,11 @@
Isabelle distribution itself, and the following two files (both
optional) have a special meaning:
- \<^item> @{verbatim "etc/settings"} holds additional settings that are
+ \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are
initialized when bootstrapping the overall Isabelle environment,
cf.\ \secref{sec:boot}. As usual, the content is interpreted as a
- @{verbatim bash} script. It may refer to the component's enclosing
- directory via the @{verbatim "COMPONENT"} shell variable.
+ \<^verbatim>\<open>bash\<close> script. It may refer to the component's enclosing
+ directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
For example, the following setting allows to refer to files within
the component later on, without having to hardwire absolute paths:
@@ -290,9 +288,9 @@
example:
@{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
- \<^item> @{verbatim "etc/components"} holds a list of further
+ \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further
sub-components of the same structure. The directory specifications
- given here can be either absolute (with leading @{verbatim "/"}) or
+ given here can be either absolute (with leading \<^verbatim>\<open>/\<close>) or
relative to the component's main directory.
@@ -302,8 +300,8 @@
that directory exists). This allows to install private components
via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is
often more convenient to do that programmatically via the
- @{verbatim init_component} shell function in the @{verbatim "etc/settings"}
- script of @{verbatim "$ISABELLE_HOME_USER"} (or any other component
+ \<^verbatim>\<open>init_component\<close> shell function in the \<^verbatim>\<open>etc/settings\<close>
+ script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
directory). For example:
@{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
@@ -358,7 +356,7 @@
internally. In a similar way, base names are relative to the
directory specified by @{setting ISABELLE_OUTPUT}. In any case,
actual file locations may also be given by including at least one
- slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
+ slash (\<^verbatim>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> to
refer to the current directory).
\<close>
@@ -367,7 +365,7 @@
text \<open>
If the input heap file does not have write permission bits set, or
- the @{verbatim "-r"} option is given explicitly, then the session
+ the \<^verbatim>\<open>-r\<close> option is given explicitly, then the session
started will be read-only. That is, the ML world cannot be
committed back into the image file. Otherwise, a writable session
enables commits into either the input file, or into another output
@@ -381,45 +379,45 @@
when they are no longer needed.
\<^medskip>
- The @{verbatim "-w"} option makes the output heap file
+ The \<^verbatim>\<open>-w\<close> option makes the output heap file
read-only after terminating. Thus subsequent invocations cause the
logic image to be read-only automatically.
\<^medskip>
- Using the @{verbatim "-e"} option, arbitrary ML code may be
+ Using the \<^verbatim>\<open>-e\<close> option, arbitrary ML code may be
passed to the Isabelle session from the command line. Multiple
- @{verbatim "-e"}'s are evaluated in the given order. Strange things
+ \<^verbatim>\<open>-e\<close> options are evaluated in the given order. Strange things
may happen when erroneous ML code is provided. Also make sure that
the ML commands are terminated properly by semicolon.
\<^medskip>
- The @{verbatim "-m"} option adds identifiers of print modes
+ The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes
to be made active for this session. Typically, this is used by some
user interface, e.g.\ to enable output of proper mathematical
symbols.
\<^medskip>
Isabelle normally enters an interactive top-level loop
- (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
+ (after processing the \<^verbatim>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close>
option inhibits interaction, thus providing a pure batch mode
facility.
\<^medskip>
- Option @{verbatim "-o"} allows to override Isabelle system
+ Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system
options for this process, see also \secref{sec:system-options}.
- Alternatively, option @{verbatim "-O"} specifies the full environment of
+ Alternatively, option \<^verbatim>\<open>-O\<close> specifies the full environment of
system options as a file in YXML format (according to the Isabelle/Scala
- function @{verbatim isabelle.Options.encode}).
+ function \<^verbatim>\<open>isabelle.Options.encode\<close>).
\<^medskip>
- The @{verbatim "-P"} option starts the Isabelle process wrapper
+ The \<^verbatim>\<open>-P\<close> option starts the Isabelle process wrapper
for Isabelle/Scala, with a private protocol running over the specified TCP
socket. Isabelle/ML and Isabelle/Scala provide various programming
interfaces to invoke protocol functions over untyped strings and XML
trees.
\<^medskip>
- The @{verbatim "-S"} option makes the Isabelle process more
+ The \<^verbatim>\<open>-S\<close> option makes the Isabelle process more
secure by disabling some critical operations, notably runtime
compilation and evaluation of ML source code.
\<close>
@@ -434,30 +432,30 @@
Usually @{setting ISABELLE_LOGIC} refers to one of the standard
logic images, which are read-only by default. A writable session
- --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the
+ --- based on \<^verbatim>\<open>HOL\<close>, but output to \<^verbatim>\<open>Test\<close> (in the
directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
may be invoked as follows:
@{verbatim [display] \<open>isabelle_process HOL Test\<close>}
Ending this session normally (e.g.\ by typing control-D) dumps the
- whole ML system state into @{verbatim Test} (be prepared for more
+ whole ML system state into \<^verbatim>\<open>Test\<close> (be prepared for more
than 100\,MB):
- The @{verbatim Test} session may be continued later (still in
+ The \<^verbatim>\<open>Test\<close> session may be continued later (still in
writable state) by: @{verbatim [display] \<open>isabelle_process Test\<close>}
- A read-only @{verbatim Test} session may be started by:
+ A read-only \<^verbatim>\<open>Test\<close> session may be started by:
@{verbatim [display] \<open>isabelle_process -r Test\<close>}
\<^bigskip>
The next example demonstrates batch execution of Isabelle.
- We retrieve the @{verbatim Main} theory value from the theory loader
+ We retrieve the \<^verbatim>\<open>Main\<close> theory value from the theory loader
within ML (observe the delicate quoting rules for the Bash shell
vs.\ ML):
@{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL\<close>}
Note that the output text will be interspersed with additional junk
- messages by the ML runtime environment. The @{verbatim "-W"} option
+ messages by the ML runtime environment. The \<^verbatim>\<open>-W\<close> option
allows to communicate with the Isabelle process via an external
program in a more robust fashion.
\<close>
--- a/src/Doc/System/Misc.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/System/Misc.thy Thu Oct 22 21:16:49 2015 +0200
@@ -36,16 +36,16 @@
the directory @{setting ISABELLE_BROWSER_INFO}.
\<^medskip>
- The @{verbatim "-b"} option indicates that this is for
+ The \<^verbatim>\<open>-b\<close> option indicates that this is for
administrative build only, i.e.\ no browser popup if no files are
given.
- The @{verbatim "-c"} option causes the input file to be removed
+ The \<^verbatim>\<open>-c\<close> option causes the input file to be removed
after use.
- The @{verbatim "-o"} option indicates batch-mode operation, with the
- output written to the indicated file; note that @{verbatim pdf}
- produces an @{verbatim eps} copy as well.
+ The \<^verbatim>\<open>-o\<close> option indicates batch-mode operation, with the
+ output written to the indicated file; note that \<^verbatim>\<open>pdf\<close>
+ produces an \<^verbatim>\<open>eps\<close> copy as well.
\<^medskip>
The applet version of the browser is part of the standard
@@ -105,9 +105,9 @@
nodes, respectively. The arrow's color then changes to red,
indicating that the predecessor or successor nodes are currently
collapsed. The node corresponding to the collapsed nodes has the
- name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
- click on the red arrow or on the node with the name ``@{verbatim
- "[....]"}''. Similar to the directory browser, the contents of
+ name ``\<^verbatim>\<open>[....]\<close>''. To uncollapse the nodes again, simply
+ click on the red arrow or on the node with the name ``\<^verbatim>\<open>[....]\<close>''.
+ Similar to the directory browser, the contents of
theory files can be displayed by double clicking on the
corresponding node.
\<close>
@@ -141,8 +141,8 @@
\begin{center}\small
\begin{tabular}{rcl}
- \<open>graph\<close> & \<open>=\<close> & \<open>{ vertex\<close>~@{verbatim ";"}~\<open>}+\<close> \\
- \<open>vertex\<close> & \<open>=\<close> & \<open>vertex_name vertex_ID dir_name [\<close>~@{verbatim "+"}~\<open>] path [\<close>~@{verbatim "<"}~\<open>|\<close>~@{verbatim ">"}~\<open>] { vertex_ID }*\<close>
+ \<open>graph\<close> & \<open>=\<close> & \<open>{ vertex\<close>~\<^verbatim>\<open>;\<close>~\<open>}+\<close> \\
+ \<open>vertex\<close> & \<open>=\<close> & \<open>vertex_name vertex_ID dir_name [\<close>~\<^verbatim>\<open>+\<close>~\<open>] path [\<close>~\<^verbatim>\<open><\<close>~\<open>|\<close>~\<^verbatim>\<open>>\<close>~\<open>] { vertex_ID }*\<close>
\end{tabular}
\end{center}
@@ -155,16 +155,16 @@
unique.
\<^descr>[\<open>dir_name\<close>] The name of the ``directory'' the vertex
- should be placed in. A ``@{verbatim "+"}'' sign after \<open>dir_name\<close> indicates that the nodes in the directory are initially
+ should be placed in. A ``\<^verbatim>\<open>+\<close>'' sign after \<open>dir_name\<close> indicates that the nodes in the directory are initially
visible. Directories are initially invisible by default.
\<^descr>[\<open>path\<close>] The path of the corresponding theory file. This
is specified relatively to the path of the graph definition file.
- \<^descr>[List of successor/predecessor nodes] A ``@{verbatim "<"}''
+ \<^descr>[List of successor/predecessor nodes] A ``\<^verbatim>\<open><\<close>''
sign before the list means that successor nodes are listed, a
- ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
- neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
+ ``\<^verbatim>\<open>>\<close>'' sign means that predecessor nodes are listed. If
+ neither ``\<^verbatim>\<open><\<close>'' nor ``\<^verbatim>\<open>>\<close>'' is found, the
browser assumes that successor nodes are listed.
\<close>
@@ -195,22 +195,22 @@
repository @{url "http://isabelle.in.tum.de/components/"} in
particular.
- Option @{verbatim "-R"} specifies an alternative component
- repository. Note that @{verbatim "file:///"} URLs can be used for
+ Option \<^verbatim>\<open>-R\<close> specifies an alternative component
+ repository. Note that \<^verbatim>\<open>file:///\<close> URLs can be used for
local directories.
- Option @{verbatim "-a"} selects all missing components to be
+ Option \<^verbatim>\<open>-a\<close> selects all missing components to be
resolved. Explicit components may be named as command
line-arguments as well. Note that components are uniquely
identified by their base name, while the installation takes place in
the location that was specified in the attempt to initialize the
component before.
- Option @{verbatim "-l"} lists the current state of available and
+ Option \<^verbatim>\<open>-l\<close> lists the current state of available and
missing components with their location (full name) within the
file-system.
- Option @{verbatim "-I"} initializes the user settings file to
+ Option \<^verbatim>\<open>-I\<close> initializes the user settings file to
subscribe to the standard components specified in the Isabelle
repository clone --- this does not make any sense for regular
Isabelle releases. If the file already exists, it needs to be
@@ -236,14 +236,13 @@
Run Isabelle process with raw ML console and line editor
(default ISABELLE_LINE_EDITOR).\<close>}
- The @{verbatim "-l"} option specifies the logic session name. By default,
- its heap image is checked and built on demand, but the option @{verbatim
- "-n"} skips that.
+ The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default,
+ its heap image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
- Options @{verbatim "-d"}, @{verbatim "-o"}, @{verbatim "-s"} are passed
+ Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed
directly to @{tool build} (\secref{sec:tool-build}).
- Options @{verbatim "-m"}, @{verbatim "-o"} are passed directly to the
+ Options \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> are passed directly to the
underlying Isabelle process (\secref{sec:isabelle-process}).
The Isabelle process is run through the line editor that is specified via
@@ -300,11 +299,11 @@
section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close>
text \<open>The @{tool_def env} tool is a direct wrapper for the standard
- @{verbatim "/usr/bin/env"} command on POSIX systems, running within
+ \<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within
the Isabelle settings environment (\secref{sec:settings}).
The command-line arguments are that of the underlying version of
- @{verbatim env}. For example, the following invokes an instance of
+ \<^verbatim>\<open>env\<close>. For example, the following invokes an instance of
the GNU Bash shell within the Isabelle environment:
@{verbatim [display] \<open>isabelle env bash\<close>}
\<close>
@@ -326,13 +325,13 @@
Get value of VARNAMES from the Isabelle settings.\<close>}
- With the @{verbatim "-a"} option, one may inspect the full process
+ With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process
environment that Isabelle related programs are run in. This usually
contains much more variables than are actually Isabelle settings.
- Normally, output is a list of lines of the form \<open>name\<close>@{verbatim "="}\<open>value\<close>. The @{verbatim "-b"} option
+ Normally, output is a list of lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option
causes only the values to be printed.
- Option @{verbatim "-d"} produces a dump of the complete environment
+ Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment
to the specified file. Entries are terminated by the ASCII null
character, i.e.\ the C string terminator.
\<close>
@@ -368,13 +367,13 @@
Install Isabelle executables with absolute references to the
distribution directory.\<close>}
- The @{verbatim "-d"} option overrides the current Isabelle
+ The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle
distribution directory as determined by @{setting ISABELLE_HOME}.
The \<open>BINDIR\<close> argument tells where executable wrapper scripts
for @{executable "isabelle_process"} and @{executable isabelle}
should be placed, which is typically a directory in the shell's
- @{setting PATH}, such as @{verbatim "$HOME/bin"}.
+ @{setting PATH}, such as \<^verbatim>\<open>$HOME/bin\<close>.
\<^medskip>
It is also possible to make symbolic links of the main
@@ -395,11 +394,11 @@
-n NAME alternative output base name (default "isabelle_xyx")
-q quiet mode\<close>}
- Option @{verbatim "-n"} specifies an altenative (base) name for the
- generated files. The default is @{verbatim "isabelle_"}\<open>xyz\<close>
+ Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the
+ generated files. The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close>
in lower-case.
- Option @{verbatim "-q"} omits printing of the result file name.
+ Option \<^verbatim>\<open>-q\<close> omits printing of the result file name.
\<^medskip>
Implementors of Isabelle tools and applications are
@@ -421,9 +420,9 @@
\<^medskip>
The default is to output the full version string of the
- Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}.
+ Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012: May 2012\<close>.
- The @{verbatim "-i"} option produces a short identification derived
+ The \<^verbatim>\<open>-i\<close> option produces a short identification derived
from the Mercurial id of the @{setting ISABELLE_HOME} directory.
\<close>
@@ -446,13 +445,13 @@
\begin{tabular}{ll}
XML & YXML \\\hline
- @{verbatim "<"}\<open>name attribute\<close>@{verbatim "="}\<open>value \<dots>\<close>@{verbatim ">"} &
- \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>@{verbatim "="}\<open>value\<dots>\<^bold>X\<close> \\
- @{verbatim "</"}\<open>name\<close>@{verbatim ">"} & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
+ \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
+ \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
+ \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
\end{tabular}
- There is no special case for empty body text, i.e.\ @{verbatim
- "<foo/>"} is treated like @{verbatim "<foo></foo>"}. Also note that
+ There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close>
+ is treated like \<^verbatim>\<open><foo></foo>\<close>. Also note that
\<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
well-formed XML documents.
--- a/src/Doc/System/Presentation.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/System/Presentation.thy Thu Oct 22 21:16:49 2015 +0200
@@ -25,7 +25,7 @@
\begin{tabular}{lp{0.6\textwidth}}
@{tool_ref mkroot} & invoked once by the user to initialize the
- session @{verbatim ROOT} with optional @{verbatim document}
+ session \<^verbatim>\<open>ROOT\<close> with optional \<^verbatim>\<open>document\<close>
directory; \\
@{tool_ref build} & invoked repeatedly by the user to keep
@@ -77,11 +77,10 @@
options:
@{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>}
- The presentation output will appear in @{verbatim
- "$ISABELLE_BROWSER_INFO/FOL/FOL"} as reported by the above verbose
- invocation of the build process.
+ The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close>
+ as reported by the above verbose invocation of the build process.
- Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file
+ Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{file
"~~/src/HOL/Library"}) also provide actual printable documents.
These are prepared automatically as well if enabled like this:
@{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
@@ -104,7 +103,7 @@
section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
text \<open>The @{tool_def mkroot} tool configures a given directory as
- session root, with some @{verbatim ROOT} file and optional document
+ session root, with some \<^verbatim>\<open>ROOT\<close> file and optional document
source directory. Its usage is:
@{verbatim [display]
\<open>Usage: isabelle mkroot [OPTIONS] [DIR]
@@ -122,24 +121,24 @@
need to be deleted manually.
\<^medskip>
- Option @{verbatim "-d"} indicates that the session shall be
- accompanied by a formal document, with \<open>DIR\<close>@{verbatim
- "/document/root.tex"} as its {\LaTeX} entry point (see also
- \chref{ch:present}).
+ Option \<^verbatim>\<open>-d\<close> indicates that the session shall be
+ accompanied by a formal document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close>
+ as its {\LaTeX} entry point (see also \chref{ch:present}).
- Option @{verbatim "-n"} allows to specify an alternative session
+ Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session
name; otherwise the base name of the given directory is used.
\<^medskip>
The implicit Isabelle settings variable @{setting
ISABELLE_LOGIC} specifies the parent session, and @{setting
ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
- into the generated @{verbatim ROOT} file.\<close>
+ into the generated \<^verbatim>\<open>ROOT\<close> file.
+\<close>
subsubsection \<open>Examples\<close>
-text \<open>Produce session @{verbatim Test} (with document preparation)
+text \<open>Produce session \<^verbatim>\<open>Test\<close> (with document preparation)
within a separate directory of the same name:
@{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}
@@ -174,31 +173,28 @@
encountered in the batch run.
\<^medskip>
- The @{verbatim "-c"} option tells @{tool document} to
+ The \<^verbatim>\<open>-c\<close> option tells @{tool document} to
dispose the document sources after successful operation! This is
the right thing to do for sources generated by an Isabelle process,
but take care of your files in manual document preparation!
\<^medskip>
- The @{verbatim "-n"} and @{verbatim "-o"} option specify
- the final output file name and format, the default is ``@{verbatim
- document.dvi}''. Note that the result will appear in the parent of
- the target @{verbatim DIR}.
+ The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify
+ the final output file name and format, the default is ``\<^verbatim>\<open>document.dvi\<close>''.
+ Note that the result will appear in the parent of the target \<^verbatim>\<open>DIR\<close>.
\<^medskip>
- The @{verbatim "-t"} option tells {\LaTeX} how to interpret
+ The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret
tagged Isabelle command regions. Tags are specified as a comma
- separated list of modifier/name pairs: ``@{verbatim "+"}\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``@{verbatim
- "-"}\<open>foo\<close>'' to drop, and ``@{verbatim "/"}\<open>foo\<close>'' to
+ separated list of modifier/name pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'')
+ means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to
fold text tagged as \<open>foo\<close>. The builtin default is equivalent
- to the tag specification ``@{verbatim
- "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX}
- macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
- @{verbatim "\\isafoldtag"}, in @{file
- "~~/lib/texinputs/isabelle.sty"}.
+ to the tag specification ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>'';
+ see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
+ \<^verbatim>\<open>\isafoldtag\<close>, in @{file "~~/lib/texinputs/isabelle.sty"}.
\<^medskip>
- Document preparation requires a @{verbatim document}
+ Document preparation requires a \<^verbatim>\<open>document\<close>
directory within the session sources. This directory is supposed to
contain all the files needed to produce the final document --- apart
from the actual theories which are generated by Isabelle.
@@ -206,42 +202,41 @@
\<^medskip>
For most practical purposes, @{tool document} is smart
enough to create any of the specified output formats, taking
- @{verbatim root.tex} supplied by the user as a starting point. This
+ \<^verbatim>\<open>root.tex\<close> supplied by the user as a starting point. This
even includes multiple runs of {\LaTeX} to accommodate references
- and bibliographies (the latter assumes @{verbatim root.bib} within
+ and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close> within
the same directory).
- In more complex situations, a separate @{verbatim build} script for
+ In more complex situations, a separate \<^verbatim>\<open>build\<close> script for
the document sources may be given. It is invoked with command-line
arguments for the document format and the document variant name.
The script needs to produce corresponding output files, e.g.\
- @{verbatim root.pdf} for target format @{verbatim pdf} (and default
+ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and default
variants). The main work can be again delegated to @{tool latex},
but it is also possible to harvest generated {\LaTeX} sources and
copy them elsewhere.
\<^medskip>
When running the session, Isabelle copies the content of
- the original @{verbatim document} directory into its proper place
+ the original \<^verbatim>\<open>document\<close> directory into its proper place
within @{setting ISABELLE_BROWSER_INFO}, according to the session
path and document variant. Then, for any processed theory \<open>A\<close>
- some {\LaTeX} source is generated and put there as \<open>A\<close>@{verbatim ".tex"}. Furthermore, a list of all generated theory
- files is put into @{verbatim session.tex}. Typically, the root
- {\LaTeX} file provided by the user would include @{verbatim
- session.tex} to get a document containing all the theories.
+ some {\LaTeX} source is generated and put there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>.
+ Furthermore, a list of all generated theory
+ files is put into \<^verbatim>\<open>session.tex\<close>. Typically, the root
+ {\LaTeX} file provided by the user would include \<^verbatim>\<open>session.tex\<close>
+ to get a document containing all the theories.
The {\LaTeX} versions of the theories require some macros defined in
- @{file "~~/lib/texinputs/isabelle.sty"}. Doing @{verbatim
- "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine;
- the underlying @{tool latex} already includes an appropriate path
- specification for {\TeX} inputs.
+ @{file "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close>
+ in \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already
+ includes an appropriate path specification for {\TeX} inputs.
If the text contains any references to Isabelle symbols (such as
- @{verbatim "\\"}@{verbatim "<forall>"}) then @{verbatim
- "isabellesym.sty"} should be included as well. This package
- contains a standard set of {\LaTeX} macro definitions @{verbatim
- "\\isasym"}\<open>foo\<close> corresponding to @{verbatim "\\"}@{verbatim
- "<"}\<open>foo\<close>@{verbatim ">"}, see @{cite "isabelle-implementation"} for a
+ \<^verbatim>\<open>\\<close>\<^verbatim>\<open><forall>\<close>) then \<^verbatim>\<open>isabellesym.sty\<close> should be included as well.
+ This package contains a standard set of {\LaTeX} macro definitions
+ \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>,
+ see @{cite "isabelle-implementation"} for a
complete list of predefined Isabelle symbols. Users may invent
further symbols as well, just by providing {\LaTeX} macros in a
similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
@@ -253,8 +248,8 @@
\<^medskip>
As a final step of Isabelle document preparation, @{tool
- document}~@{verbatim "-c"} is run on the resulting copy of the
- @{verbatim document} directory. Thus the actual output document is
+ document}~\<^verbatim>\<open>-c\<close> is run on the resulting copy of the
+ \<^verbatim>\<open>document\<close> directory. Thus the actual output document is
built and installed in its proper place. The generated sources are
deleted after successful run of {\LaTeX} and friends.
@@ -282,16 +277,16 @@
Appropriate {\LaTeX}-related programs are run on the input file,
according to the given output format: @{executable latex},
@{executable pdflatex}, @{executable dvips}, @{executable bibtex}
- (for @{verbatim bbl}), and @{executable makeindex} (for @{verbatim
- idx}). The actual commands are determined from the settings
+ (for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>).
+ The actual commands are determined from the settings
environment (@{setting ISABELLE_PDFLATEX} etc.).
- The @{verbatim sty} output format causes the Isabelle style files to
+ The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to
be updated from the distribution. This is useful in special
situations where the document sources are to be processed another
time by separate tools.
- The @{verbatim syms} output is for internal use; it generates lists
+ The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists
of symbols that are available without loading additional {\LaTeX}
packages.
\<close>
--- a/src/Doc/System/Scala.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/System/Scala.thy Thu Oct 22 21:16:49 2015 +0200
@@ -17,18 +17,17 @@
text \<open>The @{tool_def java} tool is a direct wrapper for the Java
Runtime Environment, within the regular Isabelle settings
environment (\secref{sec:settings}). The command line arguments are
- that of the underlying Java version. It is run in @{verbatim
- "-server"} mode if possible, to improve performance (at the cost of
- extra startup time).
+ that of the underlying Java version. It is run in \<^verbatim>\<open>-server\<close> mode
+ if possible, to improve performance (at the cost of extra startup time).
- The @{verbatim java} executable is the one within @{setting
+ The \<^verbatim>\<open>java\<close> executable is the one within @{setting
ISABELLE_JDK_HOME}, according to the standard directory layout for
official JDK distributions. The class loader is augmented such that
- the name space of @{verbatim "Isabelle/Pure.jar"} is available,
+ the name space of \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available,
which is the main Isabelle/Scala module.
For example, the following command-line invokes the main method of
- class @{verbatim isabelle.GUI_Setup}, which opens a windows with
+ class \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with
some diagnostic information about the Isabelle environment:
@{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
\<close>
@@ -58,7 +57,7 @@
This allows to compile further Scala modules, depending on existing
Isabelle/Scala functionality. The resulting class or jar files can
- be added to the Java classpath using the @{verbatim classpath} Bash
+ be added to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash
function that is provided by the Isabelle process environment. Thus
add-on components can register themselves in a modular manner, see
also \secref{sec:components}.
--- a/src/Doc/System/Sessions.thy Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/System/Sessions.thy Thu Oct 22 21:16:49 2015 +0200
@@ -29,7 +29,7 @@
section \<open>Session ROOT specifications \label{sec:session-root}\<close>
-text \<open>Session specifications reside in files called @{verbatim ROOT}
+text \<open>Session specifications reside in files called \<^verbatim>\<open>ROOT\<close>
within certain directories, such as the home locations of registered
Isabelle components or additional project directories given by the
user.
@@ -45,7 +45,7 @@
meaning. The default chapter is ``\<open>Unsorted\<close>''.
Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing
- mode @{verbatim "isabelle-root"} for session ROOT files, which is
+ mode \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is
enabled by default for any file of that name.
@{rail \<open>
@@ -98,7 +98,7 @@
\<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close>
specifies an explicit directory for this session; by default this is
- the current directory of the @{verbatim ROOT} file.
+ the current directory of the \<^verbatim>\<open>ROOT\<close> file.
All theories and auxiliary source files are located relatively to
the session directory. The prover process is run within the same as
@@ -128,7 +128,7 @@
declared again.
\<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists source files for document preparation,
- typically @{verbatim ".tex"} and @{verbatim ".sty"} for {\LaTeX}.
+ typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for {\LaTeX}.
Only these explicitly given files are copied from the base directory
to the document output directory, before formal document processing
is started (see also \secref{sec:tool-document}). The local path
@@ -137,7 +137,7 @@
\<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates
\isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\ document sources are taken from the base
- directory @{verbatim document} within the session root directory.
+ directory \<^verbatim>\<open>document\<close> within the session root directory.
\<close>
@@ -156,7 +156,7 @@
text \<open>See @{file "~~/etc/options"} for the main defaults provided by
the Isabelle distribution. Isabelle/jEdit @{cite "isabelle-jedit"}
- includes a simple editing mode @{verbatim "isabelle-options"} for
+ includes a simple editing mode \<^verbatim>\<open>isabelle-options\<close> for
this file-format.
The following options are particularly relevant to build Isabelle
@@ -167,9 +167,9 @@
browser info, see also \secref{sec:info}.
\<^item> @{system_option_def "document"} specifies the document output
- format, see @{tool document} option @{verbatim "-o"} in
+ format, see @{tool document} option \<^verbatim>\<open>-o\<close> in
\secref{sec:tool-document}. In practice, the most relevant values
- are @{verbatim "document=false"} or @{verbatim "document=pdf"}.
+ are \<^verbatim>\<open>document=false\<close> or \<^verbatim>\<open>document=pdf\<close>.
\<^item> @{system_option_def "document_output"} specifies an
alternative directory for generated output of the document
@@ -181,13 +181,12 @@
\<^item> @{system_option_def "document_variants"} specifies document
variants as a colon-separated list of \<open>name=tags\<close> entries,
- corresponding to @{tool document} options @{verbatim "-n"} and
- @{verbatim "-t"}.
+ corresponding to @{tool document} options \<^verbatim>\<open>-n\<close> and
+ \<^verbatim>\<open>-t\<close>.
- For example, @{verbatim
- "document_variants=document:outline=/proof,/ML"} indicates two
- documents: the one called @{verbatim document} with default tags,
- and the other called @{verbatim outline} where proofs and ML
+ For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
+ two documents: the one called \<^verbatim>\<open>document\<close> with default tags,
+ and the other called \<^verbatim>\<open>outline\<close> where proofs and ML
sections are folded.
Document variant names are just a matter of conventions. It is also
@@ -201,7 +200,7 @@
underlying hardware. For machines with many cores or with
hyperthreading, this is often requires manual adjustment (on the
command-line or within personal settings or preferences, not within
- a session @{verbatim ROOT}).
+ a session \<^verbatim>\<open>ROOT\<close>).
\<^item> @{system_option_def "condition"} specifies a comma-separated
list of process environment variables (or Isabelle settings) that
@@ -209,9 +208,9 @@
Conditions are considered ``true'' if the corresponding environment
value is defined and non-empty.
- For example, the @{verbatim "condition=ISABELLE_FULL_TEST"} may be
+ For example, the \<^verbatim>\<open>condition=ISABELLE_FULL_TEST\<close> may be
used to guard extraordinary theories, which are meant to be enabled
- explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"}
+ explicitly via some shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close>
before invoking @{tool build}.
\<^item> @{system_option_def "timeout"} specifies a real wall-clock
@@ -237,18 +236,18 @@
arguments NAME=VAL or NAME.\<close>}
The command line arguments provide additional system options of the
- form \<open>name\<close>@{verbatim "="}\<open>value\<close> or \<open>name\<close>
+ form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close>
for Boolean options.
- Option @{verbatim "-b"} augments the implicit environment of system
+ Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system
options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
\secref{sec:tool-build}.
- Option @{verbatim "-g"} prints the value of the given option.
- Option @{verbatim "-l"} lists all options with their declaration and
+ Option \<^verbatim>\<open>-g\<close> prints the value of the given option.
+ Option \<^verbatim>\<open>-l\<close> lists all options with their declaration and
current value.
- Option @{verbatim "-x"} specifies a file to export the result in
+ Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in
YXML format, instead of printing it in human-readable form.
\<close>
@@ -261,7 +260,7 @@
images. Accordingly, it runs instances of the prover process with
optional document preparation. Its command-line usage
is:\footnote{Isabelle/Scala provides the same functionality via
- @{verbatim "isabelle.Build.build"}.}
+ \<^verbatim>\<open>isabelle.Build.build\<close>.}
@{verbatim [display]
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
@@ -296,41 +295,41 @@
described in (\secref{sec:session-root}). The totality of sessions
is determined by collecting such specifications from all Isabelle
component directories (\secref{sec:components}), augmented by more
- directories given via options @{verbatim "-d"}~\<open>DIR\<close> on the
+ directories given via options \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the
command line. Each such directory may contain a session
- @{verbatim ROOT} file with several session specifications.
+ \<^verbatim>\<open>ROOT\<close> file with several session specifications.
Any session root directory may refer recursively to further
directories of the same kind, by listing them in a catalog file
- @{verbatim "ROOTS"} line-by-line. This helps to organize large
- collections of session specifications, or to make @{verbatim "-d"}
- command line options persistent (say within @{verbatim
- "$ISABELLE_HOME_USER/ROOTS"}).
+ \<^verbatim>\<open>ROOTS\<close> line-by-line. This helps to organize large
+ collections of session specifications, or to make \<^verbatim>\<open>-d\<close>
+ command line options persistent (say within
+ \<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
\<^medskip>
The subset of sessions to be managed is determined via
individual \<open>SESSIONS\<close> given as command-line arguments, or
- session groups that are given via one or more options @{verbatim
- "-g"}~\<open>NAME\<close>. Option @{verbatim "-a"} selects all sessions.
+ session groups that are given via one or more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>.
+ Option \<^verbatim>\<open>-a\<close> selects all sessions.
The build tool takes session dependencies into account: the set of
selected sessions is completed by including all ancestors.
\<^medskip>
- One or more options @{verbatim "-x"}~\<open>NAME\<close> specify
+ One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify
sessions to be excluded. All descendents of excluded sessions are removed
- from the selection as specified above. Option @{verbatim "-X"} is
+ from the selection as specified above. Option \<^verbatim>\<open>-X\<close> is
analogous to this, but excluded sessions are specified by session group
membership.
\<^medskip>
- Option @{verbatim "-R"} reverses the selection in the sense
+ Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense
that it refers to its requirements: all ancestor sessions excluding
the original selection. This allows to prepare the stage for some
build process with different options, before running the main build
- itself (without option @{verbatim "-R"}).
+ itself (without option \<^verbatim>\<open>-R\<close>).
\<^medskip>
- Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
+ Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but
selects all sessions that are defined in the given directories.
\<^medskip>
@@ -338,50 +337,49 @@
(\secref{sec:system-options}) that are passed to the prover
eventually. The settings variable @{setting_ref
ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
- @{verbatim \<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>}. Moreover,
+ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>. Moreover,
the environment of system build options may be augmented on the
- command line via @{verbatim "-o"}~\<open>name\<close>@{verbatim
- "="}\<open>value\<close> or @{verbatim "-o"}~\<open>name\<close>, which
- abbreviates @{verbatim "-o"}~\<open>name\<close>@{verbatim"=true"} for
- Boolean options. Multiple occurrences of @{verbatim "-o"} on the
+ command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which
+ abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for
+ Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on the
command-line are applied in the given order.
\<^medskip>
- Option @{verbatim "-b"} ensures that heap images are
+ Option \<^verbatim>\<open>-b\<close> ensures that heap images are
produced for all selected sessions. By default, images are only
saved for inner nodes of the hierarchy of sessions, as required for
other sessions to continue later on.
\<^medskip>
- Option @{verbatim "-c"} cleans all descendants of the
+ Option \<^verbatim>\<open>-c\<close> cleans all descendants of the
selected sessions before performing the specified build operation.
\<^medskip>
- Option @{verbatim "-n"} omits the actual build process
+ Option \<^verbatim>\<open>-n\<close> omits the actual build process
after the preparatory stage (including optional cleanup). Note that
the return code always indicates the status of the set of selected
sessions.
\<^medskip>
- Option @{verbatim "-j"} specifies the maximum number of
+ Option \<^verbatim>\<open>-j\<close> specifies the maximum number of
parallel build jobs (prover processes). Each prover process is
subject to a separate limit of parallel worker threads, cf.\ system
option @{system_option_ref threads}.
\<^medskip>
- Option @{verbatim "-s"} enables \<^emph>\<open>system mode\<close>, which
+ Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which
means that resulting heap images and log files are stored in
@{file_unchecked "$ISABELLE_HOME/heaps"} instead of the default location
@{setting ISABELLE_OUTPUT} (which is normally in @{setting
ISABELLE_HOME_USER}, i.e.\ the user's home directory).
\<^medskip>
- Option @{verbatim "-v"} increases the general level of
- verbosity. Option @{verbatim "-l"} lists the source files that
+ Option \<^verbatim>\<open>-v\<close> increases the general level of
+ verbosity. Option \<^verbatim>\<open>-l\<close> lists the source files that
contribute to a session.
\<^medskip>
- Option @{verbatim "-k"} specifies a newly proposed keyword for
+ Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for
outer syntax (multiple uses allowed). The theory sources are checked for
conflicts wrt.\ this hypothetical change of syntax, e.g.\ to reveal
occurrences of identifiers that need to be quoted.\<close>
@@ -423,7 +421,7 @@
\<^smallskip>
Build all sessions from some other directory hierarchy,
- according to the settings variable @{verbatim "AFP"} that happens to
+ according to the settings variable \<^verbatim>\<open>AFP\<close> that happens to
be defined inside the Isabelle environment:
@{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}