src/Pure/Tools/doc.ML
author wenzelm
Mon, 23 Sep 2024 11:36:03 +0200
changeset 80930 a9e2f4e845a0
parent 73761 ef1a18e20ace
child 82759 c7d2ae25d008
permissions -rw-r--r--
minor performance tuning: more concise tuples;

(*  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
   (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close>
      (Scan.lift Parse.embedded_position) check);

end;