diff -r 632a893c0db5 -r 3b045cc57f0c src/Pure/Tools/doc.ML --- a/src/Pure/Tools/doc.ML Wed Jun 25 13:29:06 2025 +0200 +++ b/src/Pure/Tools/doc.ML Wed Jun 25 13:32:28 2025 +0200 @@ -6,15 +6,18 @@ signature DOC = sig + val names: unit -> string list val check: Proof.context -> string * Position.T -> string end; structure Doc: DOC = struct +fun names () = split_lines (\<^scala>\doc_names\ ML_System.platform); + fun check ctxt arg = Completion.check_item "documentation" (Markup.doc o #1) - (\<^scala>\doc_names\ ML_System.platform |> split_lines |> map (rpair ())) ctxt arg; + (map (rpair ()) (names ())) ctxt arg; val _ = Theory.setup