--- a/src/Pure/Thy/document_antiquotations.ML Fri Nov 13 17:48:33 2015 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Nov 13 19:59:28 2015 +0100
@@ -173,6 +173,15 @@
enclose "\\url{" "}" name)));
+(* doc entries *)
+
+val _ = Theory.setup
+ (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.name))
+ (fn {context = ctxt, ...} => fn (name, pos) =>
+ (Context_Position.report ctxt pos (Markup.doc name);
+ Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
+
+
(* formal entities *)
fun entity_antiquotation name check output =