--- 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.
--- 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!
--- 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;