# HG changeset patch
# User wenzelm
# Date 1750851148 -7200
# Node ID 3b045cc57f0c56fd73de7131759f8b0f6b0515cb
# Parent  632a893c0db5f147ad308f89e0e8b757f5ec0673
more operations (e.g. for testing);

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>\<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