--- a/NEWS Tue Nov 10 16:03:59 2015 +0100
+++ b/NEWS Tue Nov 10 19:03:29 2015 +0100
@@ -91,6 +91,9 @@
standard Isabelle fonts provide glyphs to render important control
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
+* Antiquotation @{theory_text} prints uninterpreted theory source text
+(outer syntax with command keywords etc.).
+
* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
standard LaTeX macros of the same names.
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Tue Nov 10 16:03:59 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Tue Nov 10 19:03:29 2015 +0100
@@ -110,40 +110,35 @@
@{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\end{matharray}
- The overall content of an Isabelle/Isar theory may alternate between
- formal and informal text. The main body consists of formal
- specification and proof commands, interspersed with markup commands
- (\secref{sec:markup}) or document comments (\secref{sec:comments}).
- The argument of markup commands quotes informal text to be printed
- in the resulting document, but may again refer to formal entities
- via \<^emph>\<open>document antiquotations\<close>.
+ The overall content of an Isabelle/Isar theory may alternate between formal
+ and informal text. The main body consists of formal specification and proof
+ commands, interspersed with markup commands (\secref{sec:markup}) or
+ document comments (\secref{sec:comments}). The argument of markup commands
+ quotes informal text to be printed 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>
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.
- Antiquotations usually spare the author tedious typing of logical
- entities in full detail. Even more importantly, some degree of
- consistency-checking between the main body of formal text and its
- informal explanation is achieved, since terms and types appearing in
- antiquotations are checked within the current theory or proof
- context.
+ Antiquotations usually spare the author tedious typing of logical entities
+ in full detail. Even more importantly, some degree of consistency-checking
+ between the main body of formal text and its informal explanation is
+ achieved, since terms and types appearing in antiquotations are checked
+ within the current theory or proof context.
- \<^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.
-
- A cartouche without special decoration is equivalent to
- \<^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
+ \<^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. A cartouche without special
+ decoration is equivalent to \<^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 quasi-formal text
- (unchecked).
-
- A control symbol \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> within the body text, but without a
- subsequent cartouche, is equivalent to \<^verbatim>\<open>@{\<close>\<open>name\<close>\<^verbatim>\<open>}\<close>.
+ (unchecked). A control symbol \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> within the body text, but
+ without a subsequent cartouche, is equivalent to \<^verbatim>\<open>@{\<close>\<open>name\<close>\<^verbatim>\<open>}\<close>.
\begingroup
\def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}}
@@ -160,13 +155,14 @@
\<close>}
\endgroup
- Note that the syntax of antiquotations may \<^emph>\<open>not\<close> include source
- comments \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> nor verbatim text \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>.
+ Note that the syntax of antiquotations may \<^emph>\<open>not\<close> include source 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>
@{syntax_def antiquotation_body}:
- (@@{antiquotation text} | @@{antiquotation cartouche}) options @{syntax text} |
+ (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
+ options @{syntax text} |
@@{antiquotation theory} options @{syntax name} |
@@{antiquotation thm} options styles @{syntax thmrefs} |
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@ -206,113 +202,103 @@
@@{command print_antiquotations} ('!'?)
\<close>}
- \<^descr> \<open>@{text s}\<close> prints uninterpreted source text \<open>s\<close>. This is particularly useful to print portions of text according
- to the Isabelle document style, without demanding well-formedness,
- e.g.\ small pieces of terms that should not be parsed or
- type-checked yet.
+ \<^descr> \<open>@{text s}\<close> prints uninterpreted source text \<open>s\<close>, i.e.\ inner syntax. This
+ is particularly useful to print portions of text according to the Isabelle
+ document style, without demanding well-formedness, e.g.\ small pieces of
+ terms that should not be parsed or type-checked yet.
It is also possible to write this in the short form \<open>\<open>s\<close>\<close> without any
further decoration.
- \<^descr> \<open>@{theory A}\<close> prints the name \<open>A\<close>, which is
- guaranteed to refer to a valid ancestor theory in the current
- context.
+ \<^descr> \<open>@{theory_text s}\<close> prints uninterpreted theory source text \<open>s\<close>, i.e.\
+ outer syntax with command keywords and other tokens.
- \<^descr> \<open>@{thm a\<^sub>1 \<dots> a\<^sub>n}\<close> prints theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>.
- Full fact expressions are allowed here, including attributes
- (\secref{sec:syn-att}).
+ \<^descr> \<open>@{theory A}\<close> prints the name \<open>A\<close>, which is guaranteed to refer to a valid
+ ancestor theory in the current context.
+
+ \<^descr> \<open>@{thm a\<^sub>1 \<dots> a\<^sub>n}\<close> prints theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>. Full fact expressions are
+ allowed here, including attributes (\secref{sec:syn-att}).
\<^descr> \<open>@{prop \<phi>}\<close> prints a well-typed proposition \<open>\<phi>\<close>.
- \<^descr> \<open>@{lemma \<phi> by m}\<close> proves a well-typed proposition
- \<open>\<phi>\<close> by method \<open>m\<close> and prints the original \<open>\<phi>\<close>.
+ \<^descr> \<open>@{lemma \<phi> by m}\<close> proves a well-typed proposition \<open>\<phi>\<close> by method \<open>m\<close> and
+ prints the original \<open>\<phi>\<close>.
\<^descr> \<open>@{term t}\<close> prints a well-typed term \<open>t\<close>.
- \<^descr> \<open>@{value t}\<close> evaluates a term \<open>t\<close> and prints
- its result, see also @{command_ref (HOL) value}.
+ \<^descr> \<open>@{value t}\<close> evaluates a term \<open>t\<close> and prints its result, see also
+ @{command_ref (HOL) value}.
- \<^descr> \<open>@{term_type t}\<close> prints a well-typed term \<open>t\<close>
- annotated with its type.
+ \<^descr> \<open>@{term_type t}\<close> prints a well-typed term \<open>t\<close> annotated with its type.
- \<^descr> \<open>@{typeof t}\<close> prints the type of a well-typed term
- \<open>t\<close>.
+ \<^descr> \<open>@{typeof t}\<close> prints the type of a well-typed term \<open>t\<close>.
- \<^descr> \<open>@{const c}\<close> prints a logical or syntactic constant
- \<open>c\<close>.
+ \<^descr> \<open>@{const c}\<close> prints a logical or syntactic constant \<open>c\<close>.
- \<^descr> \<open>@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}\<close> prints a constant abbreviation
- \<open>c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs\<close> as defined in the current context.
+ \<^descr> \<open>@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}\<close> prints a constant abbreviation \<open>c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs\<close>
+ as defined in the current context.
\<^descr> \<open>@{typ \<tau>}\<close> prints a well-formed type \<open>\<tau>\<close>.
- \<^descr> \<open>@{type \<kappa>}\<close> prints a (logical or syntactic) type
- constructor \<open>\<kappa>\<close>.
+ \<^descr> \<open>@{type \<kappa>}\<close> prints a (logical or syntactic) type constructor \<open>\<kappa>\<close>.
\<^descr> \<open>@{class c}\<close> prints a class \<open>c\<close>.
- \<^descr> \<open>@{goals}\<close> prints the current \<^emph>\<open>dynamic\<close> goal
- state. This is mainly for support of tactic-emulation scripts
- within Isar. Presentation of goal states does not conform to the
- idea of human-readable proof documents!
+ \<^descr> \<open>@{goals}\<close> prints the current \<^emph>\<open>dynamic\<close> goal state. This is mainly for
+ support of tactic-emulation scripts within Isar. Presentation of goal states
+ does not conform to the idea of human-readable proof documents!
- When explaining proofs in detail it is usually better to spell out
- the reasoning via proper Isar proof commands, instead of peeking at
- the internal machine configuration.
+ When explaining proofs in detail it is usually better to spell out the
+ reasoning via proper Isar proof commands, instead of peeking at the internal
+ machine configuration.
- \<^descr> \<open>@{subgoals}\<close> is similar to \<open>@{goals}\<close>, but
- does not print the main goal.
+ \<^descr> \<open>@{subgoals}\<close> is similar to \<open>@{goals}\<close>, but does not print the main goal.
- \<^descr> \<open>@{prf a\<^sub>1 \<dots> a\<^sub>n}\<close> prints the (compact) proof terms
- corresponding to the theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>. Note that this
- requires proof terms to be switched on for the current logic
- session.
+ \<^descr> \<open>@{prf a\<^sub>1 \<dots> a\<^sub>n}\<close> prints the (compact) proof terms corresponding to the
+ theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>. Note that this requires proof terms to be switched on
+ for the current logic session.
- \<^descr> \<open>@{full_prf a\<^sub>1 \<dots> a\<^sub>n}\<close> is like \<open>@{prf a\<^sub>1 \<dots>
- a\<^sub>n}\<close>, but prints the full proof terms, i.e.\ also displays
- information omitted in the compact proof term, which is denoted by
- ``\<open>_\<close>'' placeholders there.
+ \<^descr> \<open>@{full_prf a\<^sub>1 \<dots> a\<^sub>n}\<close> is like \<open>@{prf a\<^sub>1 \<dots> a\<^sub>n}\<close>, but prints the full
+ proof terms, i.e.\ also displays information omitted in the compact proof
+ term, which is denoted by ``\<open>_\<close>'' placeholders there.
- \<^descr> \<open>@{ML s}\<close>, \<open>@{ML_op s}\<close>, \<open>@{ML_type
- s}\<close>, \<open>@{ML_structure s}\<close>, and \<open>@{ML_functor s}\<close>
- check text \<open>s\<close> as ML value, infix operator, type, structure,
- and functor respectively. The source is printed verbatim.
+ \<^descr> \<open>@{ML s}\<close>, \<open>@{ML_op s}\<close>, \<open>@{ML_type s}\<close>, \<open>@{ML_structure s}\<close>, and
+ \<open>@{ML_functor s}\<close> check text \<open>s\<close> as ML value, infix operator, type,
+ structure, 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>.
+ \<^descr> \<open>@{emph s}\<close> prints document source recursively, with {\LaTeX} 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>.
+ \<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX} 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.
+ \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
+ characters, using some type-writer font style.
- \<^descr> \<open>@{file path}\<close> checks that \<open>path\<close> refers to a
- file (or directory) and prints it verbatim.
+ \<^descr> \<open>@{file path}\<close> checks that \<open>path\<close> refers to a file (or directory) and
+ prints it verbatim.
- \<^descr> \<open>@{file_unchecked path}\<close> is like \<open>@{file
- path}\<close>, but does not check the existence of the \<open>path\<close>
- within the file-system.
+ \<^descr> \<open>@{file_unchecked path}\<close> is like \<open>@{file path}\<close>, but does not check the
+ existence of the \<open>path\<close> within the file-system.
- \<^descr> \<open>@{url name}\<close> produces markup for the given URL, which
- results in an active hyperlink within the text.
+ \<^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
- are output with commas, e.g. \<open>@{cite foo \<AND> bar}\<close> becomes
- \<^verbatim>\<open>\cite{foo,bar}\<close>.
+ 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>.
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>.
+ @{attribute cite_macro} in the context. For example, \<open>@{cite [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
- indicates extra verbosity.
+ \<^descr> @{command "print_antiquotations"} prints all document antiquotations that
+ are defined in the current context; the ``\<open>!\<close>'' option indicates extra
+ verbosity.
\<close>
--- a/src/Pure/Isar/token.ML Tue Nov 10 16:03:59 2015 +0100
+++ b/src/Pure/Isar/token.ML Tue Nov 10 19:03:29 2015 +0100
@@ -89,6 +89,8 @@
val pretty_value: Proof.context -> T -> Pretty.T
val pretty_src: Proof.context -> src -> Pretty.T
val ident_or_symbolic: string -> bool
+ val source': bool -> Keyword.keywords -> (Symbol_Pos.T, 'a) Source.source ->
+ (T, (Symbol_Pos.T, 'a) Source.source) Source.source
val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
val source: Keyword.keywords ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
--- a/src/Pure/PIDE/markup.ML Tue Nov 10 16:03:59 2015 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Nov 10 19:03:29 2015 +0100
@@ -28,6 +28,7 @@
val is_delimited: Properties.T -> bool
val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
+ val language_outer: bool -> T
val language_method: T
val language_attribute: T
val language_sort: bool -> T
@@ -299,6 +300,7 @@
fun language' {name, symbols, antiquotes} delimited =
language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
+val language_outer = language' {name = "", symbols = true, antiquotes = false};
val language_method =
language {name = "method", symbols = true, antiquotes = false, delimited = false};
val language_attribute =
--- a/src/Pure/Thy/thy_output.ML Tue Nov 10 16:03:59 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Nov 10 19:03:29 2015 +0100
@@ -650,6 +650,29 @@
end;
+(* theory text with tokens (unchecked) *)
+
+val _ =
+ Theory.setup
+ (antiquotation @{binding theory_text} (Scan.lift Args.text_input)
+ (fn {context = ctxt, ...} => fn source =>
+ let
+ val _ =
+ Context_Position.report ctxt (Input.pos_of source)
+ (Markup.language_outer (Input.is_delimited source));
+
+ val keywords = Thy_Header.get_keywords' ctxt;
+ val toks =
+ Source.of_list (Input.source_explode source)
+ |> Token.source' true keywords
+ |> Source.exhaust;
+ val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
+ in
+ implode (map Latex.output_token toks)
+ |> (if Config.get ctxt display then Latex.environment "isabelle" else enclose "\\isa{" "}")
+ end));
+
+
(* basic entities *)
local