diff -r bd5ee3148132 -r 042180540068 src/Pure/Tools/doc.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/doc.ML	Sat Nov 28 17:38:03 2020 +0100
@@ -0,0 +1,24 @@
+(*  Title:      Pure/Tools/doc.ML
+    Author:     Makarius
+
+Access to Isabelle documentation.
+*)
+
+signature DOC =
+sig
+  val check: Proof.context -> string * Position.T -> string
+end;
+
+structure Doc: DOC =
+struct
+
+fun check ctxt arg =
+  Completion.check_item "documentation" (Markup.doc o #1)
+    (\<^scala>\<open>doc_names\<close> "" |> split_lines |> map (rpair ())) ctxt arg;
+
+val _ =
+  Theory.setup
+   (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close>
+      (Scan.lift Parse.embedded_position) check);
+
+end;