# HG changeset patch
# User wenzelm
# Date 1447178609 -3600
# Node ID 34978e1b234ff28343910a4e1473a0acecac7fd6
# Parent  e4194168a1eb3d8106c164d7e16f8fa1d0a07786
added document antiquotation @{theory_text};
tuned document;

diff -r e4194168a1eb -r 34978e1b234f NEWS
--- 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.
diff -r e4194168a1eb -r 34978e1b234f src/Doc/Isar_Ref/Document_Preparation.thy
--- 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>
 
 
diff -r e4194168a1eb -r 34978e1b234f src/Pure/Isar/token.ML
--- 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,
diff -r e4194168a1eb -r 34978e1b234f src/Pure/PIDE/markup.ML
--- 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 =
diff -r e4194168a1eb -r 34978e1b234f src/Pure/Thy/thy_output.ML
--- 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