# HG changeset patch
# User wenzelm
# Date 1447194062 -3600
# Node ID 2f89f0b13e0890853e2f1fe87eb7f1e646b63fb3
# Parent  8bb7848b3d4749751f5d1f3acbeb9e5f0f428b9f
added @{command}, @{method}, @{attribute};

diff -r 8bb7848b3d47 -r 2f89f0b13e08 NEWS
--- a/NEWS	Tue Nov 10 22:27:48 2015 +0100
+++ b/NEWS	Tue Nov 10 23:21:02 2015 +0100
@@ -94,6 +94,9 @@
 * 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 8bb7848b3d47 -r 2f89f0b13e08 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Nov 10 22:27:48 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Nov 10 23:21:02 2015 +0100
@@ -175,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 |
@@ -244,6 +246,9 @@
 
   \<^descr> \<open>@{class c}\<close> prints a class \<open>c\<close>.
 
+  \<^descr> \<open>@{command name}\<close>, \<open>@{method name}\<close>, \<open>@{attribute name}\<close> print checked
+  entities of the Isar language.
+
   \<^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!
diff -r 8bb7848b3d47 -r 2f89f0b13e08 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Tue Nov 10 22:27:48 2015 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Nov 10 23:21:02 2015 +0100
@@ -172,4 +172,18 @@
       (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;