src/Pure/Tools/doc.ML
changeset 82767 3b045cc57f0c
parent 82759 c7d2ae25d008
--- 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