| author | wenzelm | 
| Thu, 21 Mar 2024 14:43:40 +0100 | |
| changeset 79954 | 475074795dca | 
| parent 73761 | ef1a18e20ace | 
| child 82759 | c7d2ae25d008 | 
| permissions | -rw-r--r-- | 
(* 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;