# HG changeset patch
# User wenzelm
# Date 1447195190 -3600
# Node ID 18e3efa15e52166003162ff68f282d13326ed50b
# Parent  40859aa6d10c361c41653ffe5ac39d786091a431# Parent  b98b237969c0cfabe82f847cfab6c1f0436ba85b
merged

diff -r 40859aa6d10c -r 18e3efa15e52 NEWS
--- a/NEWS	Tue Nov 10 17:49:54 2015 +0100
+++ b/NEWS	Tue Nov 10 23:39:50 2015 +0100
@@ -91,6 +91,12 @@
 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 @{command}, @{method}, @{attribute} print checked
+entities of the Isar language.
+
 * 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 40859aa6d10c -r 18e3efa15e52 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Nov 10 23:39:50 2015 +0100
@@ -4,18 +4,20 @@
 
 chapter \<open>Document preparation \label{ch:document-prep}\<close>
 
-text \<open>Isabelle/Isar provides a simple document preparation system
-  based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks
-  within that format.  This allows to produce papers, books, theses
-  etc.\ from Isabelle theory sources.
+text \<open>
+  Isabelle/Isar provides a simple document preparation system based on
+  {PDF-\LaTeX}, with support for hyperlinks and bookmarks within that format.
+  This allows to produce papers, books, theses etc.\ from Isabelle theory
+  sources.
 
-  {\LaTeX} output is generated while processing a \<^emph>\<open>session\<close> in
-  batch mode, as explained in the \<^emph>\<open>The Isabelle System Manual\<close>
-  @{cite "isabelle-system"}.  The main Isabelle tools to get started with
-  document preparation are @{tool_ref mkroot} and @{tool_ref build}.
+  {\LaTeX} output is generated while processing a \<^emph>\<open>session\<close> in batch mode, as
+  explained in the \<^emph>\<open>The Isabelle System Manual\<close> @{cite "isabelle-system"}.
+  The main Isabelle tools to get started with document preparation are
+  @{tool_ref mkroot} and @{tool_ref build}.
 
-  The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also
-  explains some aspects of theory presentation.\<close>
+  The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also explains
+  some aspects of theory presentation.
+\<close>
 
 
 section \<open>Markup commands \label{sec:markup}\<close>
@@ -33,16 +35,15 @@
     @{command_def "text_raw"} & : & \<open>any \<rightarrow> any\<close> \\
   \end{matharray}
 
-  Markup commands provide a structured way to insert text into the
-  document generated from a theory.  Each markup command takes a
-  single @{syntax text} argument, which is passed as argument to a
-  corresponding {\LaTeX} macro.  The default macros provided by
-  @{file "~~/lib/texinputs/isabelle.sty"} can be redefined according
-  to the needs of the underlying document and {\LaTeX} styles.
+  Markup commands provide a structured way to insert text into the document
+  generated from a theory. Each markup command takes a single @{syntax text}
+  argument, which is passed as argument to a corresponding {\LaTeX} macro. The
+  default macros provided by @{file "~~/lib/texinputs/isabelle.sty"} can be
+  redefined according to the needs of the underlying document and {\LaTeX}
+  styles.
 
-  Note that formal comments (\secref{sec:comments}) are similar to
-  markup commands, but have a different status within Isabelle/Isar
-  syntax.
+  Note that formal comments (\secref{sec:comments}) are similar to markup
+  commands, but have a different status within Isabelle/Isar syntax.
 
   @{rail \<open>
     (@@{command chapter} | @@{command section} | @@{command subsection} |
@@ -50,28 +51,27 @@
       @@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
   \<close>}
 
-  \<^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.\
+    \<^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.\
 
-  \<^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.
+    \<^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.
 
-  \<^descr> @{command text_raw} is similar to @{command text}, but without
-  any surrounding markup environment. This allows to inject arbitrary
-  {\LaTeX} source into the generated document.
-
+    \<^descr> @{command text_raw} is similar to @{command text}, but without any
+    surrounding markup environment. This allows to inject arbitrary {\LaTeX}
+    source into the generated document.
 
   All text passed to any of the above markup commands may refer to formal
-  entities via \<^emph>\<open>document antiquotations\<close>, see also \secref{sec:antiq}.
-  These are interpreted in the present theory or proof context.
+  entities via \<^emph>\<open>document antiquotations\<close>, see also \secref{sec:antiq}. These
+  are interpreted in the present theory or proof context.
 
   \<^medskip>
-  The proof markup commands closely resemble those for theory
-  specifications, but have a different formal status and produce
-  different {\LaTeX} macros.
+  The proof markup commands closely resemble those for theory specifications,
+  but have a different formal status and produce different {\LaTeX} macros.
 \<close>
 
 
@@ -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}? |
@@ -179,7 +175,9 @@
       @@{antiquotation abbrev} options @{syntax term} |
       @@{antiquotation typ} options @{syntax type} |
       @@{antiquotation type} options @{syntax name} |
-      @@{antiquotation class} options @{syntax name}
+      @@{antiquotation class} options @{syntax name} |
+      (@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
+        options @{syntax name}
     ;
     @{syntax antiquotation}:
       @@{antiquotation goals} options |
@@ -206,229 +204,215 @@
     @@{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>@{command name}\<close>, \<open>@{method name}\<close>, \<open>@{attribute name}\<close> print checked
+  entities of the Isar language.
 
-  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>@{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.
   
-  \<^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>@{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>@{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>
 
 
 subsection \<open>Styled antiquotations\<close>
 
-text \<open>The antiquotations \<open>thm\<close>, \<open>prop\<close> and \<open>term\<close> admit an extra \<^emph>\<open>style\<close> specification to modify the
-  printed result.  A style is specified by a name with a possibly
-  empty number of arguments;  multiple styles can be sequenced with
-  commas.  The following standard styles are available:
+text \<open>
+  The antiquotations \<open>thm\<close>, \<open>prop\<close> and \<open>term\<close> admit an extra \<^emph>\<open>style\<close>
+  specification to modify the printed result. A style is specified by a name
+  with a possibly empty number of arguments; multiple styles can be sequenced
+  with commas. The following standard styles are available:
 
-  \<^descr> \<open>lhs\<close> extracts the first argument of any application
-  form with at least two arguments --- typically meta-level or
-  object-level equality, or any other binary relation.
+  \<^descr> \<open>lhs\<close> extracts the first argument of any application form with at least
+  two arguments --- typically meta-level or object-level equality, or any
+  other binary relation.
   
-  \<^descr> \<open>rhs\<close> is like \<open>lhs\<close>, but extracts the second
-  argument.
+  \<^descr> \<open>rhs\<close> is like \<open>lhs\<close>, but extracts the second argument.
   
-  \<^descr> \<open>concl\<close> extracts the conclusion \<open>C\<close> from a rule
-  in Horn-clause normal form \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close>.
+  \<^descr> \<open>concl\<close> extracts the conclusion \<open>C\<close> from a rule in Horn-clause normal form
+  \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close>.
   
-  \<^descr> \<open>prem\<close> \<open>n\<close> extract premise number
-  \<open>n\<close> from from a rule in Horn-clause
-  normal form \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close>
+  \<^descr> \<open>prem\<close> \<open>n\<close> extract premise number \<open>n\<close> from from a rule in Horn-clause
+  normal form \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close>.
 \<close>
 
 
 subsection \<open>General options\<close>
 
-text \<open>The following options are available to tune the printed output
-  of antiquotations.  Note that many of these coincide with system and
+text \<open>
+  The following options are available to tune the printed output of
+  antiquotations. Note that many of these coincide with system and
   configuration options of the same names.
 
-  \<^descr> @{antiquotation_option_def show_types}~\<open>= bool\<close> and
-  @{antiquotation_option_def show_sorts}~\<open>= bool\<close> control
-  printing of explicit type and sort constraints.
+    \<^descr> @{antiquotation_option_def show_types}~\<open>= bool\<close> and
+    @{antiquotation_option_def show_sorts}~\<open>= bool\<close> control printing of
+    explicit type and sort constraints.
 
-  \<^descr> @{antiquotation_option_def show_structs}~\<open>= bool\<close>
-  controls printing of implicit structures.
+    \<^descr> @{antiquotation_option_def show_structs}~\<open>= bool\<close> controls printing of
+    implicit structures.
 
-  \<^descr> @{antiquotation_option_def show_abbrevs}~\<open>= bool\<close>
-  controls folding of abbreviations.
+    \<^descr> @{antiquotation_option_def show_abbrevs}~\<open>= bool\<close> controls folding of
+    abbreviations.
 
-  \<^descr> @{antiquotation_option_def names_long}~\<open>= bool\<close> forces
-  names of types and constants etc.\ to be printed in their fully
-  qualified internal form.
+    \<^descr> @{antiquotation_option_def names_long}~\<open>= bool\<close> forces names of types
+    and constants etc.\ to be printed in their fully qualified internal form.
 
-  \<^descr> @{antiquotation_option_def names_short}~\<open>= bool\<close>
-  forces names of types and constants etc.\ to be printed unqualified.
-  Note that internalizing the output again in the current context may
-  well yield a different result.
+    \<^descr> @{antiquotation_option_def names_short}~\<open>= bool\<close> forces names of types
+    and constants etc.\ to be printed unqualified. Note that internalizing the
+    output again in the current context may well yield a different result.
 
-  \<^descr> @{antiquotation_option_def names_unique}~\<open>= bool\<close>
-  determines whether the printed version of qualified names should be
-  made sufficiently long to avoid overlap with names declared further
-  back.  Set to \<open>false\<close> for more concise output.
+    \<^descr> @{antiquotation_option_def names_unique}~\<open>= bool\<close> determines whether the
+    printed version of qualified names should be made sufficiently long to
+    avoid overlap with names declared further back. Set to \<open>false\<close> for more
+    concise output.
 
-  \<^descr> @{antiquotation_option_def eta_contract}~\<open>= bool\<close>
-  prints terms in \<open>\<eta>\<close>-contracted form.
+    \<^descr> @{antiquotation_option_def eta_contract}~\<open>= bool\<close> prints terms in
+    \<open>\<eta>\<close>-contracted form.
 
-  \<^descr> @{antiquotation_option_def display}~\<open>= bool\<close> indicates
-  if the text is to be output as multi-line ``display material'',
-  rather than a small piece of text without line breaks (which is the
-  default).
+    \<^descr> @{antiquotation_option_def display}~\<open>= bool\<close> indicates if the text is to
+    be output as multi-line ``display material'', rather than a small piece of
+    text without line breaks (which is the default).
 
-  In this mode the embedded entities are printed in the same style as
-  the main theory text.
+    In this mode the embedded entities are printed in the same style as the
+    main theory text.
 
-  \<^descr> @{antiquotation_option_def break}~\<open>= bool\<close> controls
-  line breaks in non-display material.
+    \<^descr> @{antiquotation_option_def break}~\<open>= bool\<close> controls line breaks in
+    non-display material.
 
-  \<^descr> @{antiquotation_option_def quotes}~\<open>= bool\<close> indicates
-  if the output should be enclosed in double quotes.
-
-  \<^descr> @{antiquotation_option_def mode}~\<open>= name\<close> adds \<open>name\<close> to the print mode to be used for presentation.  Note that the
-  standard setup for {\LaTeX} output is already present by default,
-  including the modes \<open>latex\<close> and \<open>xsymbols\<close>.
+    \<^descr> @{antiquotation_option_def quotes}~\<open>= bool\<close> indicates if the output
+    should be enclosed in double quotes.
 
-  \<^descr> @{antiquotation_option_def margin}~\<open>= nat\<close> and
-  @{antiquotation_option_def indent}~\<open>= nat\<close> change the margin
-  or indentation for pretty printing of display material.
+    \<^descr> @{antiquotation_option_def mode}~\<open>= name\<close> adds \<open>name\<close> to the print mode
+    to be used for presentation. Note that the standard setup for {\LaTeX}
+    output is already present by default, including the modes \<open>latex\<close> and
+    \<open>xsymbols\<close>.
 
-  \<^descr> @{antiquotation_option_def goals_limit}~\<open>= nat\<close>
-  determines the maximum number of subgoals to be printed (for goal-based
-  antiquotation).
+    \<^descr> @{antiquotation_option_def margin}~\<open>= nat\<close> and
+    @{antiquotation_option_def indent}~\<open>= nat\<close> change the margin or
+    indentation for pretty printing of display material.
+
+    \<^descr> @{antiquotation_option_def goals_limit}~\<open>= nat\<close> determines the maximum
+    number of subgoals to be printed (for goal-based antiquotation).
 
-  \<^descr> @{antiquotation_option_def source}~\<open>= bool\<close> prints the
-  original source text of the antiquotation arguments, rather than its
-  internal representation.  Note that formal checking of
-  @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still
-  enabled; use the @{antiquotation "text"} antiquotation for unchecked
-  output.
+    \<^descr> @{antiquotation_option_def source}~\<open>= bool\<close> prints the original source
+    text of the antiquotation arguments, rather than its internal
+    representation. Note that formal checking of @{antiquotation "thm"},
+    @{antiquotation "term"}, etc. is still enabled; use the @{antiquotation
+    "text"} antiquotation for unchecked output.
 
-  Regular \<open>term\<close> and \<open>typ\<close> antiquotations with \<open>source = false\<close> involve a full round-trip from the original source
-  to an internalized logical entity back to a source form, according
-  to the syntax of the current context.  Thus the printed output is
-  not under direct control of the author, it may even fluctuate a bit
-  as the underlying theory is changed later on.
+    Regular \<open>term\<close> and \<open>typ\<close> antiquotations with \<open>source = false\<close> involve a
+    full round-trip from the original source to an internalized logical entity
+    back to a source form, according to the syntax of the current context.
+    Thus the printed output is not under direct control of the author, it may
+    even fluctuate a bit as the underlying theory is changed later on.
 
-  In contrast, @{antiquotation_option source}~\<open>= true\<close>
-  admits direct printing of the given source text, with the desirable
-  well-formedness check in the background, but without modification of
-  the printed text.
+    In contrast, @{antiquotation_option source}~\<open>= true\<close> admits direct
+    printing of the given source text, with the desirable well-formedness
+    check in the background, but without modification of the printed text.
 
-
-  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>\<open>ROOT\<close> file.
+  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>\<open>ROOT\<close> file.
 \<close>
 
 
 section \<open>Markup via command tags \label{sec:tags}\<close>
 
-text \<open>Each Isabelle/Isar command may be decorated by additional
-  presentation tags, to indicate some modification in the way it is
-  printed in the document.
+text \<open>
+  Each Isabelle/Isar command may be decorated by additional presentation tags,
+  to indicate some modification in the way it is printed in the document.
 
   @{rail \<open>
     @{syntax_def tags}: ( tag * )
@@ -436,8 +420,8 @@
     tag: '%' (@{syntax ident} | @{syntax string})
   \<close>}
 
-  Some tags are pre-declared for certain classes of commands, serving
-  as default markup if no tags are given in the text:
+  Some tags are pre-declared for certain classes of commands, serving as
+  default markup if no tags are given in the text:
 
   \<^medskip>
   \begin{tabular}{ll}
@@ -447,34 +431,29 @@
   \end{tabular}
   \<^medskip>
 
-  The Isabelle document preparation system
-  @{cite "isabelle-system"} allows tagged command regions to be presented
-  specifically, e.g.\ to fold proof texts, or drop parts of the text
-  completely.
+  The Isabelle document preparation system @{cite "isabelle-system"} allows
+  tagged command regions to be presented specifically, e.g.\ to fold proof
+  texts, or drop parts of the text completely.
 
-  For example ``@{command "by"}~\<open>%invisible auto\<close>'' causes
-  that piece of proof to be treated as \<open>invisible\<close> instead of
-  \<open>proof\<close> (the default), which may be shown or hidden
-  depending on the document setup.  In contrast, ``@{command
-  "by"}~\<open>%visible auto\<close>'' forces this text to be shown
-  invariably.
+  For example ``@{command "by"}~\<open>%invisible auto\<close>'' causes that piece of proof
+  to be treated as \<open>invisible\<close> instead of \<open>proof\<close> (the default), which may be
+  shown or hidden depending on the document setup. In contrast, ``@{command
+  "by"}~\<open>%visible auto\<close>'' forces this text to be shown invariably.
 
-  Explicit tag specifications within a proof apply to all subsequent
-  commands of the same level of nesting.  For example, ``@{command
-  "proof"}~\<open>%visible \<dots>\<close>~@{command "qed"}'' forces the whole
-  sub-proof to be typeset as \<open>visible\<close> (unless some of its parts
-  are tagged differently).
+  Explicit tag specifications within a proof apply to all subsequent commands
+  of the same level of nesting. For example, ``@{command "proof"}~\<open>%visible
+  \<dots>\<close>~@{command "qed"}'' forces the whole sub-proof to be typeset as \<open>visible\<close>
+  (unless some of its parts are tagged differently).
 
   \<^medskip>
-  Command tags merely produce certain markup environments for
-  type-setting.  The meaning of these is determined by {\LaTeX}
-  macros, as defined in @{file "~~/lib/texinputs/isabelle.sty"} or
-  by the document author.  The Isabelle document preparation tools
-  also provide some high-level options to specify the meaning of
-  arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
-  parts of the text.  Logic sessions may also specify ``document
-  versions'', where given tags are interpreted in some particular way.
-  Again see @{cite "isabelle-system"} for further details.
+  Command tags merely produce certain markup environments for type-setting.
+  The meaning of these is determined by {\LaTeX} macros, as defined in @{file
+  "~~/lib/texinputs/isabelle.sty"} or by the document author. The Isabelle
+  document preparation tools also provide some high-level options to specify
+  the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the
+  corresponding parts of the text. Logic sessions may also specify ``document
+  versions'', where given tags are interpreted in some particular way. Again
+  see @{cite "isabelle-system"} for further details.
 \<close>
 
 
@@ -489,14 +468,13 @@
     'rail' @{syntax text}
   \<close>}
 
-  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
+  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>\<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
-  below.
+  The rail specification language is quoted here as Isabelle @{syntax string}
+  or text @{syntax "cartouche"}; it has its own grammar given below.
 
   \begingroup
   \def\isasymnewline{\isatt{\isacharbackslash\isacharless newline\isachargreater}}
@@ -515,15 +493,14 @@
   \<close>}
   \endgroup
 
-  The lexical syntax of \<open>identifier\<close> coincides with that of
-  @{syntax ident} in regular Isabelle syntax, but \<open>string\<close> uses
-  single quotes instead of double quotes of the standard @{syntax
-  string} category.
+  The lexical syntax of \<open>identifier\<close> coincides with that of @{syntax ident} in
+  regular Isabelle syntax, but \<open>string\<close> uses single quotes instead of double
+  quotes of the standard @{syntax string} category.
 
-  Each \<open>rule\<close> defines a formal language (with optional name),
-  using a notation that is similar to EBNF or regular expressions with
-  recursion.  The meaning and visual appearance of these rail language
-  elements is illustrated by the following representative examples.
+  Each \<open>rule\<close> defines a formal language (with optional name), using a notation
+  that is similar to EBNF or regular expressions with recursion. The meaning
+  and visual appearance of these rail language elements is illustrated by the
+  following representative examples.
 
   \<^item> Empty \<^verbatim>\<open>()\<close>
 
@@ -594,10 +571,9 @@
     @@{command display_drafts} (@{syntax name} +)
   \<close>}
 
-  \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a
-  given list of raw source files. Only those symbols that do not require
-  additional {\LaTeX} packages are displayed properly, everything else is left
-  verbatim.
+  \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
+  of raw source files. Only those symbols that do not require additional
+  {\LaTeX} packages are displayed properly, everything else is left verbatim.
 \<close>
 
 end
diff -r 40859aa6d10c -r 18e3efa15e52 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Nov 10 23:39:50 2015 +0100
@@ -141,77 +141,15 @@
             #> enclose "\\isa{" "}")));
 
 
-(* theory file *)
-
-val _ =
-  Theory.setup (Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
-    (fn {context = ctxt, ...} =>
-      fn name => (Resources.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])));
-
-
-(* Isabelle/jEdit elements *)
-
-local
-
-fun parse_named a (XML.Elem ((b, props), _)) =
-      (case Properties.get props "NAME" of
-        SOME name => if a = b then [name] else []
-      | NONE => [])
-  | parse_named _ _ = [];
-
-val isabelle_jedit_actions =
-  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
-    XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
-  | _ => []);
-
-val isabelle_jedit_dockables =
-  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
-    XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
-  | _ => []);
-
-val jedit_actions =
-  Lazy.lazy (fn () =>
-    (case Isabelle_System.bash_output
-      "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
-      (txt, 0) =>
-        (case XML.parse txt of
-          XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
-        | _ => [])
-    | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
-
-in
-
-fun is_action a =
-  member (op =) isabelle_jedit_actions a orelse
-  member (op =) isabelle_jedit_dockables a orelse
-  member (op =) (Lazy.force jedit_actions) a;
-
-end;
-
-
 (* Isabelle/Isar entities (with index) *)
 
 local
 
-fun no_check _ _ = true;
-
-fun is_keyword ctxt (name, _) =
-  Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name;
+fun no_check (_: Proof.context) (name, _: Position.T) = name;
 
-fun check_command ctxt (name, pos) =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val keywords = Thy_Header.get_keywords thy;
-  in
-    Keyword.is_command keywords name andalso
-      let
-        val markup =
-          Token.explode keywords Position.none name
-          |> maps (Outer_Syntax.command_reports thy)
-          |> map (snd o fst);
-        val _ = Context_Position.reports ctxt (map (pair pos) markup);
-      in true end
-  end;
+fun check_keyword ctxt (name, pos) =
+  if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name
+  else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos);
 
 fun check_system_option ctxt (name, pos) =
   (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
@@ -248,16 +186,12 @@
             NONE => ""
           | SOME is_def =>
               "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
+        val _ = check ctxt (name, pos);
       in
-        if check ctxt (name, pos) then
-          idx ^
-          (Output.output name
-            |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
-            |> (if Config.get ctxt Thy_Output.quotes then quote else I)
-            |> (if Config.get ctxt Thy_Output.display
-                then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
-                else hyper o enclose "\\mbox{\\isa{" "}}"))
-        else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos)
+        idx ^
+        (Output.output name
+          |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
+          |> hyper o enclose "\\mbox{\\isa{" "}}")
       end);
 
 fun entity_antiqs check markup kind =
@@ -270,23 +204,23 @@
 val _ =
   Theory.setup
    (entity_antiqs no_check "" @{binding syntax} #>
-    entity_antiqs check_command "isacommand" @{binding command} #>
-    entity_antiqs is_keyword "isakeyword" @{binding keyword} #>
-    entity_antiqs is_keyword "isakeyword" @{binding element} #>
-    entity_antiqs (can o Method.check_name) "" @{binding method} #>
-    entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #>
+    entity_antiqs Outer_Syntax.check_command "isacommand" @{binding command} #>
+    entity_antiqs check_keyword "isakeyword" @{binding keyword} #>
+    entity_antiqs check_keyword "isakeyword" @{binding element} #>
+    entity_antiqs Method.check_name "" @{binding method} #>
+    entity_antiqs Attrib.check_name "" @{binding attribute} #>
     entity_antiqs no_check "" @{binding fact} #>
     entity_antiqs no_check "" @{binding variable} #>
     entity_antiqs no_check "" @{binding case} #>
-    entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
-    entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
+    entity_antiqs Thy_Output.check_command "" @{binding antiquotation} #>
+    entity_antiqs Thy_Output.check_option "" @{binding antiquotation_option} #>
     entity_antiqs no_check "isasystem" @{binding setting} #>
     entity_antiqs check_system_option "isasystem" @{binding system_option} #>
     entity_antiqs no_check "" @{binding inference} #>
     entity_antiqs no_check "isasystem" @{binding executable} #>
     entity_antiqs check_tool "isatool" @{binding tool} #>
-    entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
-    entity_antiqs (K (is_action o #1)) "isasystem" @{binding action});
+    entity_antiqs ML_Context.check_antiquotation "" @{binding ML_antiquotation} #>
+    entity_antiqs (K JEdit.check_action) "isasystem" @{binding action});
 
 end;
 
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/General/completion.scala	Tue Nov 10 23:39:50 2015 +0100
@@ -205,8 +205,15 @@
              (Long_Name.qualify(kind, name),
               Word.implode(Word.explode('_', kind)) +
               (if (xname == name) "" else " " + quote(decode(name))))
-          description = List(xname1, "(" + descr_name + ")")
-        } yield Item(range, original, full_name, description, xname1, 0, true)
+        } yield {
+          val description = List(xname1, "(" + descr_name + ")")
+          val replacement =
+            Token.explode(Keyword.Keywords.empty, xname1) match {
+              case List(tok) if tok.is_name => xname1
+              case _ => quote(xname1)
+            }
+          Item(range, original, full_name, description, replacement, 0, true)
+        }
 
       if (items.isEmpty) None
       else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
@@ -246,7 +253,7 @@
   {
     override val whiteSpace = "".r
 
-    private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>)""".r
+    private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r
     def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches
 
     private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/Isar/keyword.ML	Tue Nov 10 23:39:50 2015 +0100
@@ -43,6 +43,7 @@
   val is_keyword: keywords -> string -> bool
   val is_command: keywords -> string -> bool
   val is_literal: keywords -> string -> bool
+  val dest_commands: keywords -> string list
   val command_markup: keywords -> string -> Markup.T option
   val command_kind: keywords -> string -> string option
   val command_files: keywords -> string -> Path.T -> Path.T list
@@ -187,6 +188,8 @@
 fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
 fun is_literal keywords = is_keyword keywords orf is_command keywords;
 
+fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands;
+
 
 (* command keywords *)
 
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Nov 10 23:39:50 2015 +0100
@@ -25,6 +25,7 @@
   val parse_spans: Token.T list -> Command_Span.span list
   val side_comments: Token.T list -> Token.T list
   val command_reports: theory -> Token.T -> Position.report_text list
+  val check_command: Proof.context -> string * Position.T -> string
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -268,7 +269,7 @@
 val side_comments = filter Token.is_proper #> cmts;
 
 
-(* read commands *)
+(* check commands *)
 
 fun command_reports thy tok =
   if Token.is_command tok then
@@ -279,4 +280,30 @@
     end
   else [];
 
+fun check_command ctxt (name, pos) =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val keywords = Thy_Header.get_keywords thy;
+  in
+    if Keyword.is_command keywords name then
+      let
+        val markup =
+          Token.explode keywords Position.none name
+          |> maps (command_reports thy)
+          |> map (#2 o #1);
+        val _ = Context_Position.reports ctxt (map (pair pos) markup);
+      in name end
+    else
+      let
+        val completion =
+          Completion.make (name, pos)
+            (fn completed =>
+              Keyword.dest_commands keywords
+              |> filter completed
+              |> sort_strings
+              |> map (fn a => (a, (Markup.commandN, a))));
+        val report = Markup.markup_report (Completion.reported_text completion);
+      in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end
+  end;
+
 end;
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/Isar/token.ML	Tue Nov 10 23:39:50 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 40859aa6d10c -r 18e3efa15e52 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Nov 10 23:39:50 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 40859aa6d10c -r 18e3efa15e52 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/Pure.thy	Tue Nov 10 23:39:50 2015 +0100
@@ -109,6 +109,7 @@
 ML_file "Tools/simplifier_trace.ML"
 ML_file "Tools/debugger.ML"
 ML_file "Tools/named_theorems.ML"
+ML_file "Tools/jedit.ML"
 
 
 section \<open>Basic attributes\<close>
@@ -298,4 +299,3 @@
 qed
 
 end
-
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/ROOT	Tue Nov 10 23:39:50 2015 +0100
@@ -227,6 +227,7 @@
     "System/message_channel.ML"
     "System/options.ML"
     "System/system_channel.ML"
+    "Thy/document_antiquotations.ML"
     "Thy/html.ML"
     "Thy/latex.ML"
     "Thy/markdown.ML"
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/ROOT.ML	Tue Nov 10 23:39:50 2015 +0100
@@ -303,6 +303,7 @@
 use "Thy/term_style.ML";
 use "Isar/outer_syntax.ML";
 use "Thy/thy_output.ML";
+use "Thy/document_antiquotations.ML";
 use "General/graph_display.ML";
 use "Thy/present.ML";
 use "pure_syn.ML";
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/Thy/document_antiquotations.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Nov 10 23:39:50 2015 +0100
@@ -0,0 +1,189 @@
+(*  Title:      Pure/ML/document_antiquotations.ML
+    Author:     Makarius
+
+Miscellaneous document antiquotations.
+*)
+
+structure Document_Antiquotations: sig end =
+struct
+
+(* control spacing *)
+
+val _ =
+  Theory.setup
+   (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #>
+    Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #>
+    Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #>
+    Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip"));
+
+
+(* control style *)
+
+local
+
+fun control_antiquotation name s1 s2 =
+  Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
+    (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
+
+in
+
+val _ =
+  Theory.setup
+   (control_antiquotation @{binding footnote} "\\footnote{" "}" #>
+    control_antiquotation @{binding emph} "\\emph{" "}" #>
+    control_antiquotation @{binding bold} "\\textbf{" "}");
+
+end;
+
+
+(* quasi-formal text (unchecked) *)
+
+local
+
+fun text_antiquotation name =
+  Thy_Output.antiquotation name (Scan.lift Args.text_input)
+    (fn {context = ctxt, ...} => fn source =>
+     (Context_Position.report ctxt (Input.pos_of source)
+        (Markup.language_text (Input.is_delimited source));
+      Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)]));
+
+in
+
+val _ =
+  Theory.setup
+   (text_antiquotation @{binding text} #>
+    text_antiquotation @{binding cartouche});
+
+end;
+
+
+(* theory text with tokens (unchecked) *)
+
+val _ =
+  Theory.setup
+    (Thy_Output.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 Thy_Output.display
+            then Latex.environment "isabelle"
+            else enclose "\\isa{" "}")
+        end));
+
+
+(* goal state *)
+
+local
+
+fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
+  (fn {state, context = ctxt, ...} => fn () =>
+    Thy_Output.output ctxt
+      [Goal_Display.pretty_goal
+        (Config.put Goal_Display.show_main_goal main ctxt)
+        (#goal (Proof.goal (Toplevel.proof_of state)))]);
+
+in
+
+val _ = Theory.setup
+ (goal_state @{binding goals} true #>
+  goal_state @{binding subgoals} false);
+
+end;
+
+
+(* embedded lemma *)
+
+val _ = Theory.setup
+  (Thy_Output.antiquotation @{binding lemma}
+    (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
+      Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
+    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
+      let
+        val prop_src = Token.src (Token.name_of_src source) [prop_token];
+
+        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
+        val _ = Context_Position.reports ctxt reports;
+
+        (* FIXME check proof!? *)
+        val _ = ctxt
+          |> Proof.theorem NONE (K I) [[(prop, [])]]
+          |> Proof.global_terminal_proof (m1, m2);
+      in
+        Thy_Output.output ctxt
+          (Thy_Output.maybe_pretty_source Thy_Output.pretty_term ctxt prop_src [prop])
+      end));
+
+
+(* verbatim text *)
+
+val _ =
+  Theory.setup
+    (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text)
+      (Thy_Output.verbatim_text o #context));
+
+
+(* ML text *)
+
+local
+
+fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input)
+  (fn {context = ctxt, ...} => fn source =>
+   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
+    Thy_Output.verbatim_text ctxt (Input.source_content source)));
+
+fun ml_enclose bg en source =
+  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
+
+in
+
+val _ = Theory.setup
+ (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
+  ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
+  ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
+  ml_text @{binding ML_structure}
+    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
+
+  ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
+    (fn source =>
+      ML_Lex.read ("ML_Env.check_functor " ^
+        ML_Syntax.print_string (Input.source_content source))) #>
+
+  ml_text @{binding ML_text} (K []));
+
+end;
+
+
+(* URLs *)
+
+val _ = Theory.setup
+  (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
+    (fn {context = ctxt, ...} => fn (name, pos) =>
+      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
+       enclose "\\url{" "}" name)));
+
+
+(* formal entities *)
+
+fun entity_antiquotation name check output =
+  Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name))
+    (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
+
+val _ =
+  Theory.setup
+   (entity_antiquotation @{binding command} Outer_Syntax.check_command
+     (enclose "\\isacommand{" "}" o Output.output) #>
+    entity_antiquotation @{binding method} Method.check_name Output.output #>
+    entity_antiquotation @{binding attribute} Attrib.check_name Output.output);
+
+end;
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Nov 10 17:49:54 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Nov 10 23:39:50 2015 +0100
@@ -597,60 +597,18 @@
         #> enclose "\\isa{" "}");
 
 
-
-(** concrete antiquotations **)
-
-(* control spacing *)
+(* verbatim text *)
 
-val _ =
-  Theory.setup
-   (antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #>
-    antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #>
-    antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #>
-    antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip"));
+fun verbatim_text ctxt =
+  if Config.get ctxt display then
+    Latex.output_ascii #> Latex.environment "isabellett"
+  else
+    split_lines #>
+    map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
+    space_implode "\\isasep\\isanewline%\n";
 
 
-(* control style *)
-
-local
-
-fun control_antiquotation name s1 s2 =
-  antiquotation name (Scan.lift Args.cartouche_input)
-    (fn {state, ...} => enclose s1 s2 o output_text state {markdown = false});
-
-in
-
-val _ =
-  Theory.setup
-   (control_antiquotation @{binding footnote} "\\footnote{" "}" #>
-    control_antiquotation @{binding emph} "\\emph{" "}" #>
-    control_antiquotation @{binding bold} "\\textbf{" "}");
-
-end;
-
-
-(* quasi-formal text (unchecked) *)
-
-local
-
-fun text_antiquotation name =
-  antiquotation name (Scan.lift Args.text_input)
-    (fn {context = ctxt, ...} => fn source =>
-     (Context_Position.report ctxt (Input.pos_of source)
-        (Markup.language_text (Input.is_delimited source));
-      output ctxt [pretty_text ctxt (Input.source_content source)]));
-
-in
-
-val _ =
-  Theory.setup
-   (text_antiquotation @{binding text} #>
-    text_antiquotation @{binding cartouche});
-
-end;
-
-
-(* basic entities *)
+(* antiquotations for basic entities *)
 
 local
 
@@ -685,101 +643,6 @@
 end;
 
 
-(* goal state *)
-
-local
-
-fun goal_state name main = antiquotation name (Scan.succeed ())
-  (fn {state, context = ctxt, ...} => fn () =>
-    output ctxt
-      [Goal_Display.pretty_goal
-        (Config.put Goal_Display.show_main_goal main ctxt)
-        (#goal (Proof.goal (Toplevel.proof_of state)))]);
-
-in
-
-val _ = Theory.setup
- (goal_state @{binding goals} true #>
-  goal_state @{binding subgoals} false);
-
-end;
-
-
-(* embedded lemma *)
-
-val _ = Theory.setup
-  (antiquotation @{binding lemma}
-    (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
-      Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
-    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
-      let
-        val prop_src = Token.src (Token.name_of_src source) [prop_token];
-
-        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
-        val _ = Context_Position.reports ctxt reports;
-
-        (* FIXME check proof!? *)
-        val _ = ctxt
-          |> Proof.theorem NONE (K I) [[(prop, [])]]
-          |> Proof.global_terminal_proof (m1, m2);
-      in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end));
-
-
-(* verbatim text *)
-
-fun verbatim_text ctxt =
-  if Config.get ctxt display then
-    Latex.output_ascii #> Latex.environment "isabellett"
-  else
-    split_lines #>
-    map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
-    space_implode "\\isasep\\isanewline%\n";
-
-val _ =
-  Theory.setup
-    (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context));
-
-
-(* ML text *)
-
-local
-
-fun ml_text name ml = antiquotation name (Scan.lift Args.text_input)
-  (fn {context = ctxt, ...} => fn source =>
-   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
-    verbatim_text ctxt (Input.source_content source)));
-
-fun ml_enclose bg en source =
-  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
-
-in
-
-val _ = Theory.setup
- (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
-  ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
-  ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
-  ml_text @{binding ML_structure}
-    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
-
-  ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
-    (fn source =>
-      ML_Lex.read ("ML_Env.check_functor " ^
-        ML_Syntax.print_string (Input.source_content source))) #>
-
-  ml_text @{binding ML_text} (K []));
-
-end;
-
-
-(* URLs *)
-
-val _ = Theory.setup
-  (antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
-    (fn {context = ctxt, ...} => fn (name, pos) =>
-      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
-       enclose "\\url{" "}" name)));
-
-
 
 (** document commands **)
 
diff -r 40859aa6d10c -r 18e3efa15e52 src/Pure/Tools/jedit.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/jedit.ML	Tue Nov 10 23:39:50 2015 +0100
@@ -0,0 +1,71 @@
+(*  Title:      Pure/Tools/jedit.ML
+    Author:     Makarius
+
+jEdit support.
+*)
+
+signature JEDIT =
+sig
+  val check_action: string * Position.T -> string
+end;
+
+structure JEdit: JEDIT =
+struct
+
+(* jEdit actions *)
+
+local
+
+fun parse_named a (XML.Elem ((b, props), _)) =
+      (case Properties.get props "NAME" of
+        SOME name => if a = b then [name] else []
+      | NONE => [])
+  | parse_named _ _ = [];
+
+val isabelle_jedit_actions =
+  Lazy.lazy (fn () =>
+    (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
+      XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
+    | _ => []));
+
+val isabelle_jedit_dockables =
+  Lazy.lazy (fn () =>
+    (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
+      XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
+    | _ => []));
+
+val jedit_actions =
+  Lazy.lazy (fn () =>
+    (case Isabelle_System.bash_output
+      "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of
+      (txt, 0) =>
+        (case XML.parse txt of
+          XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
+        | _ => [])
+    | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
+
+val all_actions =
+  Lazy.lazy (fn () =>
+    Lazy.force isabelle_jedit_actions @
+    Lazy.force isabelle_jedit_dockables @
+    Lazy.force jedit_actions);
+
+in
+
+fun check_action (name, pos) =
+  if member (op =) (Lazy.force all_actions) name then name
+  else
+    let
+      val completion =
+        Completion.make (name, pos)
+          (fn completed =>
+            Lazy.force all_actions
+            |> filter completed
+            |> sort_strings
+            |> map (fn a => (a, ("action", a))));
+      val report = Markup.markup_report (Completion.reported_text completion);
+    in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end
+
+end;
+
+end;