added document antiquotation @{theory_text};
authorwenzelm
Tue Nov 10 19:03:29 2015 +0100 (2015-11-10)
changeset 6161434978e1b234f
parent 61613 e4194168a1eb
child 61615 e8fcd347b669
added document antiquotation @{theory_text};
tuned document;
NEWS
src/Doc/Isar_Ref/Document_Preparation.thy
src/Pure/Isar/token.ML
src/Pure/PIDE/markup.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Tue Nov 10 16:03:59 2015 +0100
     1.2 +++ b/NEWS	Tue Nov 10 19:03:29 2015 +0100
     1.3 @@ -91,6 +91,9 @@
     1.4  standard Isabelle fonts provide glyphs to render important control
     1.5  symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
     1.6  
     1.7 +* Antiquotation @{theory_text} prints uninterpreted theory source text
     1.8 +(outer syntax with command keywords etc.).
     1.9 +
    1.10  * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
    1.11  corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
    1.12  standard LaTeX macros of the same names.
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Nov 10 16:03:59 2015 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Nov 10 19:03:29 2015 +0100
     2.3 @@ -110,40 +110,35 @@
     2.4      @{command_def "print_antiquotations"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     2.5    \end{matharray}
     2.6  
     2.7 -  The overall content of an Isabelle/Isar theory may alternate between
     2.8 -  formal and informal text.  The main body consists of formal
     2.9 -  specification and proof commands, interspersed with markup commands
    2.10 -  (\secref{sec:markup}) or document comments (\secref{sec:comments}).
    2.11 -  The argument of markup commands quotes informal text to be printed
    2.12 -  in the resulting document, but may again refer to formal entities
    2.13 -  via \<^emph>\<open>document antiquotations\<close>.
    2.14 +  The overall content of an Isabelle/Isar theory may alternate between formal
    2.15 +  and informal text. The main body consists of formal specification and proof
    2.16 +  commands, interspersed with markup commands (\secref{sec:markup}) or
    2.17 +  document comments (\secref{sec:comments}). The argument of markup commands
    2.18 +  quotes informal text to be printed in the resulting document, but may again
    2.19 +  refer to formal entities via \<^emph>\<open>document antiquotations\<close>.
    2.20  
    2.21    For example, embedding \<^verbatim>\<open>@{term [show_types] "f x = a + x"}\<close>
    2.22    within a text block makes
    2.23    \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.
    2.24  
    2.25 -  Antiquotations usually spare the author tedious typing of logical
    2.26 -  entities in full detail.  Even more importantly, some degree of
    2.27 -  consistency-checking between the main body of formal text and its
    2.28 -  informal explanation is achieved, since terms and types appearing in
    2.29 -  antiquotations are checked within the current theory or proof
    2.30 -  context.
    2.31 +  Antiquotations usually spare the author tedious typing of logical entities
    2.32 +  in full detail. Even more importantly, some degree of consistency-checking
    2.33 +  between the main body of formal text and its informal explanation is
    2.34 +  achieved, since terms and types appearing in antiquotations are checked
    2.35 +  within the current theory or proof context.
    2.36  
    2.37 -  \<^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>.
    2.38 -  The short form \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>name\<close>\<^verbatim>\<open>>\<close>\<open>\<open>argument_content\<close>\<close> (without
    2.39 -  surrounding \<^verbatim>\<open>@{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>) works for a single
    2.40 -  argument that is a cartouche.
    2.41 -
    2.42 -  A cartouche without special decoration is equivalent to
    2.43 -  \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which is equivalent to
    2.44 -  \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The special name
    2.45 +  \<^medskip>
    2.46 +  Antiquotations are in general written as
    2.47 +  \<^verbatim>\<open>@{\<close>\<open>name\<close>~\<^verbatim>\<open>[\<close>\<open>options\<close>\<^verbatim>\<open>]\<close>~\<open>arguments\<close>\<^verbatim>\<open>}\<close>. The short form
    2.48 +  \<^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>)
    2.49 +  works for a single argument that is a cartouche. A cartouche without special
    2.50 +  decoration is equivalent to \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which is
    2.51 +  equivalent to \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The special name
    2.52    @{antiquotation_def cartouche} is defined in the context: Isabelle/Pure
    2.53    introduces that as an alias to @{antiquotation_ref text} (see below).
    2.54    Consequently, \<open>\<open>foo_bar + baz \<le> bazar\<close>\<close> prints literal quasi-formal text
    2.55 -  (unchecked).
    2.56 -
    2.57 -  A control symbol \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> within the body text, but without a
    2.58 -  subsequent cartouche, is equivalent to \<^verbatim>\<open>@{\<close>\<open>name\<close>\<^verbatim>\<open>}\<close>.
    2.59 +  (unchecked). A control symbol \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> within the body text, but
    2.60 +  without a subsequent cartouche, is equivalent to \<^verbatim>\<open>@{\<close>\<open>name\<close>\<^verbatim>\<open>}\<close>.
    2.61  
    2.62    \begingroup
    2.63    \def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}}
    2.64 @@ -160,13 +155,14 @@
    2.65    \<close>}
    2.66    \endgroup
    2.67  
    2.68 -  Note that the syntax of antiquotations may \<^emph>\<open>not\<close> include source
    2.69 -  comments \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> nor verbatim text \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>.
    2.70 +  Note that the syntax of antiquotations may \<^emph>\<open>not\<close> include source comments
    2.71 +  \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> nor verbatim text \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>.
    2.72  
    2.73    %% FIXME less monolithic presentation, move to individual sections!?
    2.74    @{rail \<open>
    2.75      @{syntax_def antiquotation_body}:
    2.76 -      (@@{antiquotation text} | @@{antiquotation cartouche}) options @{syntax text} |
    2.77 +      (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
    2.78 +        options @{syntax text} |
    2.79        @@{antiquotation theory} options @{syntax name} |
    2.80        @@{antiquotation thm} options styles @{syntax thmrefs} |
    2.81        @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
    2.82 @@ -206,113 +202,103 @@
    2.83      @@{command print_antiquotations} ('!'?)
    2.84    \<close>}
    2.85  
    2.86 -  \<^descr> \<open>@{text s}\<close> prints uninterpreted source text \<open>s\<close>.  This is particularly useful to print portions of text according
    2.87 -  to the Isabelle document style, without demanding well-formedness,
    2.88 -  e.g.\ small pieces of terms that should not be parsed or
    2.89 -  type-checked yet.
    2.90 +  \<^descr> \<open>@{text s}\<close> prints uninterpreted source text \<open>s\<close>, i.e.\ inner syntax. This
    2.91 +  is particularly useful to print portions of text according to the Isabelle
    2.92 +  document style, without demanding well-formedness, e.g.\ small pieces of
    2.93 +  terms that should not be parsed or type-checked yet.
    2.94  
    2.95    It is also possible to write this in the short form \<open>\<open>s\<close>\<close> without any
    2.96    further decoration.
    2.97  
    2.98 -  \<^descr> \<open>@{theory A}\<close> prints the name \<open>A\<close>, which is
    2.99 -  guaranteed to refer to a valid ancestor theory in the current
   2.100 -  context.
   2.101 +  \<^descr> \<open>@{theory_text s}\<close> prints uninterpreted theory source text \<open>s\<close>, i.e.\
   2.102 +  outer syntax with command keywords and other tokens.
   2.103  
   2.104 -  \<^descr> \<open>@{thm a\<^sub>1 \<dots> a\<^sub>n}\<close> prints theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>.
   2.105 -  Full fact expressions are allowed here, including attributes
   2.106 -  (\secref{sec:syn-att}).
   2.107 +  \<^descr> \<open>@{theory A}\<close> prints the name \<open>A\<close>, which is guaranteed to refer to a valid
   2.108 +  ancestor theory in the current context.
   2.109 +
   2.110 +  \<^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
   2.111 +  allowed here, including attributes (\secref{sec:syn-att}).
   2.112  
   2.113    \<^descr> \<open>@{prop \<phi>}\<close> prints a well-typed proposition \<open>\<phi>\<close>.
   2.114  
   2.115 -  \<^descr> \<open>@{lemma \<phi> by m}\<close> proves a well-typed proposition
   2.116 -  \<open>\<phi>\<close> by method \<open>m\<close> and prints the original \<open>\<phi>\<close>.
   2.117 +  \<^descr> \<open>@{lemma \<phi> by m}\<close> proves a well-typed proposition \<open>\<phi>\<close> by method \<open>m\<close> and
   2.118 +  prints the original \<open>\<phi>\<close>.
   2.119  
   2.120    \<^descr> \<open>@{term t}\<close> prints a well-typed term \<open>t\<close>.
   2.121    
   2.122 -  \<^descr> \<open>@{value t}\<close> evaluates a term \<open>t\<close> and prints
   2.123 -  its result, see also @{command_ref (HOL) value}.
   2.124 +  \<^descr> \<open>@{value t}\<close> evaluates a term \<open>t\<close> and prints its result, see also
   2.125 +  @{command_ref (HOL) value}.
   2.126  
   2.127 -  \<^descr> \<open>@{term_type t}\<close> prints a well-typed term \<open>t\<close>
   2.128 -  annotated with its type.
   2.129 +  \<^descr> \<open>@{term_type t}\<close> prints a well-typed term \<open>t\<close> annotated with its type.
   2.130  
   2.131 -  \<^descr> \<open>@{typeof t}\<close> prints the type of a well-typed term
   2.132 -  \<open>t\<close>.
   2.133 +  \<^descr> \<open>@{typeof t}\<close> prints the type of a well-typed term \<open>t\<close>.
   2.134  
   2.135 -  \<^descr> \<open>@{const c}\<close> prints a logical or syntactic constant
   2.136 -  \<open>c\<close>.
   2.137 +  \<^descr> \<open>@{const c}\<close> prints a logical or syntactic constant \<open>c\<close>.
   2.138    
   2.139 -  \<^descr> \<open>@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}\<close> prints a constant abbreviation
   2.140 -  \<open>c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs\<close> as defined in the current context.
   2.141 +  \<^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>
   2.142 +  as defined in the current context.
   2.143  
   2.144    \<^descr> \<open>@{typ \<tau>}\<close> prints a well-formed type \<open>\<tau>\<close>.
   2.145  
   2.146 -  \<^descr> \<open>@{type \<kappa>}\<close> prints a (logical or syntactic) type
   2.147 -    constructor \<open>\<kappa>\<close>.
   2.148 +  \<^descr> \<open>@{type \<kappa>}\<close> prints a (logical or syntactic) type constructor \<open>\<kappa>\<close>.
   2.149  
   2.150    \<^descr> \<open>@{class c}\<close> prints a class \<open>c\<close>.
   2.151  
   2.152 -  \<^descr> \<open>@{goals}\<close> prints the current \<^emph>\<open>dynamic\<close> goal
   2.153 -  state.  This is mainly for support of tactic-emulation scripts
   2.154 -  within Isar.  Presentation of goal states does not conform to the
   2.155 -  idea of human-readable proof documents!
   2.156 +  \<^descr> \<open>@{goals}\<close> prints the current \<^emph>\<open>dynamic\<close> goal state. This is mainly for
   2.157 +  support of tactic-emulation scripts within Isar. Presentation of goal states
   2.158 +  does not conform to the idea of human-readable proof documents!
   2.159  
   2.160 -  When explaining proofs in detail it is usually better to spell out
   2.161 -  the reasoning via proper Isar proof commands, instead of peeking at
   2.162 -  the internal machine configuration.
   2.163 +  When explaining proofs in detail it is usually better to spell out the
   2.164 +  reasoning via proper Isar proof commands, instead of peeking at the internal
   2.165 +  machine configuration.
   2.166    
   2.167 -  \<^descr> \<open>@{subgoals}\<close> is similar to \<open>@{goals}\<close>, but
   2.168 -  does not print the main goal.
   2.169 +  \<^descr> \<open>@{subgoals}\<close> is similar to \<open>@{goals}\<close>, but does not print the main goal.
   2.170    
   2.171 -  \<^descr> \<open>@{prf a\<^sub>1 \<dots> a\<^sub>n}\<close> prints the (compact) proof terms
   2.172 -  corresponding to the theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>. Note that this
   2.173 -  requires proof terms to be switched on for the current logic
   2.174 -  session.
   2.175 +  \<^descr> \<open>@{prf a\<^sub>1 \<dots> a\<^sub>n}\<close> prints the (compact) proof terms corresponding to the
   2.176 +  theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>. Note that this requires proof terms to be switched on
   2.177 +  for the current logic session.
   2.178    
   2.179 -  \<^descr> \<open>@{full_prf a\<^sub>1 \<dots> a\<^sub>n}\<close> is like \<open>@{prf a\<^sub>1 \<dots>
   2.180 -  a\<^sub>n}\<close>, but prints the full proof terms, i.e.\ also displays
   2.181 -  information omitted in the compact proof term, which is denoted by
   2.182 -  ``\<open>_\<close>'' placeholders there.
   2.183 +  \<^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
   2.184 +  proof terms, i.e.\ also displays information omitted in the compact proof
   2.185 +  term, which is denoted by ``\<open>_\<close>'' placeholders there.
   2.186    
   2.187 -  \<^descr> \<open>@{ML s}\<close>, \<open>@{ML_op s}\<close>, \<open>@{ML_type
   2.188 -  s}\<close>, \<open>@{ML_structure s}\<close>, and \<open>@{ML_functor s}\<close>
   2.189 -  check text \<open>s\<close> as ML value, infix operator, type, structure,
   2.190 -  and functor respectively.  The source is printed verbatim.
   2.191 +  \<^descr> \<open>@{ML s}\<close>, \<open>@{ML_op s}\<close>, \<open>@{ML_type s}\<close>, \<open>@{ML_structure s}\<close>, and
   2.192 +  \<open>@{ML_functor s}\<close> check text \<open>s\<close> as ML value, infix operator, type,
   2.193 +  structure, and functor respectively. The source is printed verbatim.
   2.194  
   2.195 -  \<^descr> \<open>@{emph s}\<close> prints document source recursively, with {\LaTeX}
   2.196 -  markup \<^verbatim>\<open>\emph{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>.
   2.197 +  \<^descr> \<open>@{emph s}\<close> prints document source recursively, with {\LaTeX} markup
   2.198 +  \<^verbatim>\<open>\emph{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>.
   2.199  
   2.200 -  \<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX}
   2.201 -  markup \<^verbatim>\<open>\textbf{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>.
   2.202 +  \<^descr> \<open>@{bold s}\<close> prints document source recursively, with {\LaTeX} markup
   2.203 +  \<^verbatim>\<open>\textbf{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>.
   2.204  
   2.205 -  \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally
   2.206 -  as ASCII characters, using some type-writer font style.
   2.207 +  \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
   2.208 +  characters, using some type-writer font style.
   2.209  
   2.210 -  \<^descr> \<open>@{file path}\<close> checks that \<open>path\<close> refers to a
   2.211 -  file (or directory) and prints it verbatim.
   2.212 +  \<^descr> \<open>@{file path}\<close> checks that \<open>path\<close> refers to a file (or directory) and
   2.213 +  prints it verbatim.
   2.214  
   2.215 -  \<^descr> \<open>@{file_unchecked path}\<close> is like \<open>@{file
   2.216 -  path}\<close>, but does not check the existence of the \<open>path\<close>
   2.217 -  within the file-system.
   2.218 +  \<^descr> \<open>@{file_unchecked path}\<close> is like \<open>@{file path}\<close>, but does not check the
   2.219 +  existence of the \<open>path\<close> within the file-system.
   2.220  
   2.221 -  \<^descr> \<open>@{url name}\<close> produces markup for the given URL, which
   2.222 -  results in an active hyperlink within the text.
   2.223 +  \<^descr> \<open>@{url name}\<close> produces markup for the given URL, which results in an
   2.224 +  active hyperlink within the text.
   2.225  
   2.226 -  \<^descr> \<open>@{cite name}\<close> produces a citation \<^verbatim>\<open>\cite{name}\<close> in {\LaTeX},
   2.227 -  where the name refers to some Bib{\TeX} database entry.
   2.228 +  \<^descr> \<open>@{cite name}\<close> produces a citation \<^verbatim>\<open>\cite{name}\<close> in {\LaTeX}, where the
   2.229 +  name refers to some Bib{\TeX} database entry.
   2.230  
   2.231 -  The variant \<open>@{cite \<open>opt\<close> name}\<close> produces \<^verbatim>\<open>\cite[opt]{name}\<close> with
   2.232 -  some free-form optional argument. Multiple names
   2.233 -  are output with commas, e.g. \<open>@{cite foo \<AND> bar}\<close> becomes
   2.234 -  \<^verbatim>\<open>\cite{foo,bar}\<close>.
   2.235 +  The variant \<open>@{cite \<open>opt\<close> name}\<close> produces \<^verbatim>\<open>\cite[opt]{name}\<close> with some
   2.236 +  free-form optional argument. Multiple names are output with commas, e.g.
   2.237 +  \<open>@{cite foo \<AND> bar}\<close> becomes \<^verbatim>\<open>\cite{foo,bar}\<close>.
   2.238  
   2.239    The {\LaTeX} macro name is determined by the antiquotation option
   2.240    @{antiquotation_option_def cite_macro}, or the configuration option
   2.241 -  @{attribute cite_macro} in the context. For example, \<open>@{cite
   2.242 -  [cite_macro = nocite] foobar}\<close> produces \<^verbatim>\<open>\nocite{foobar}\<close>.
   2.243 +  @{attribute cite_macro} in the context. For example, \<open>@{cite [cite_macro =
   2.244 +  nocite] foobar}\<close> produces \<^verbatim>\<open>\nocite{foobar}\<close>.
   2.245  
   2.246 -  \<^descr> @{command "print_antiquotations"} prints all document antiquotations
   2.247 -  that are defined in the current context; the ``\<open>!\<close>'' option
   2.248 -  indicates extra verbosity.
   2.249 +  \<^descr> @{command "print_antiquotations"} prints all document antiquotations that
   2.250 +  are defined in the current context; the ``\<open>!\<close>'' option indicates extra
   2.251 +  verbosity.
   2.252  \<close>
   2.253  
   2.254  
     3.1 --- a/src/Pure/Isar/token.ML	Tue Nov 10 16:03:59 2015 +0100
     3.2 +++ b/src/Pure/Isar/token.ML	Tue Nov 10 19:03:29 2015 +0100
     3.3 @@ -89,6 +89,8 @@
     3.4    val pretty_value: Proof.context -> T -> Pretty.T
     3.5    val pretty_src: Proof.context -> src -> Pretty.T
     3.6    val ident_or_symbolic: string -> bool
     3.7 +  val source': bool -> Keyword.keywords -> (Symbol_Pos.T, 'a) Source.source ->
     3.8 +    (T, (Symbol_Pos.T, 'a) Source.source) Source.source
     3.9    val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
    3.10    val source: Keyword.keywords ->
    3.11      Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
     4.1 --- a/src/Pure/PIDE/markup.ML	Tue Nov 10 16:03:59 2015 +0100
     4.2 +++ b/src/Pure/PIDE/markup.ML	Tue Nov 10 19:03:29 2015 +0100
     4.3 @@ -28,6 +28,7 @@
     4.4    val is_delimited: Properties.T -> bool
     4.5    val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
     4.6    val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
     4.7 +  val language_outer: bool -> T
     4.8    val language_method: T
     4.9    val language_attribute: T
    4.10    val language_sort: bool -> T
    4.11 @@ -299,6 +300,7 @@
    4.12  fun language' {name, symbols, antiquotes} delimited =
    4.13    language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
    4.14  
    4.15 +val language_outer = language' {name = "", symbols = true, antiquotes = false};
    4.16  val language_method =
    4.17    language {name = "method", symbols = true, antiquotes = false, delimited = false};
    4.18  val language_attribute =
     5.1 --- a/src/Pure/Thy/thy_output.ML	Tue Nov 10 16:03:59 2015 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Nov 10 19:03:29 2015 +0100
     5.3 @@ -650,6 +650,29 @@
     5.4  end;
     5.5  
     5.6  
     5.7 +(* theory text with tokens (unchecked) *)
     5.8 +
     5.9 +val _ =
    5.10 +  Theory.setup
    5.11 +    (antiquotation @{binding theory_text} (Scan.lift Args.text_input)
    5.12 +      (fn {context = ctxt, ...} => fn source =>
    5.13 +        let
    5.14 +          val _ =
    5.15 +            Context_Position.report ctxt (Input.pos_of source)
    5.16 +              (Markup.language_outer (Input.is_delimited source));
    5.17 +
    5.18 +          val keywords = Thy_Header.get_keywords' ctxt;
    5.19 +          val toks =
    5.20 +            Source.of_list (Input.source_explode source)
    5.21 +            |> Token.source' true keywords
    5.22 +            |> Source.exhaust;
    5.23 +          val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
    5.24 +        in
    5.25 +          implode (map Latex.output_token toks)
    5.26 +          |> (if Config.get ctxt display then Latex.environment "isabelle" else enclose "\\isa{" "}")
    5.27 +        end));
    5.28 +
    5.29 +
    5.30  (* basic entities *)
    5.31  
    5.32  local