--- 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>\<open>doc_names\<close> ML_System.platform);
+
fun check ctxt arg =
Completion.check_item "documentation" (Markup.doc o #1)
- (\<^scala>\<open>doc_names\<close> ML_System.platform |> split_lines |> map (rpair ())) ctxt arg;
+ (map (rpair ()) (names ())) ctxt arg;
val _ =
Theory.setup