# HG changeset patch
# User wenzelm
# Date 1750846092 -7200
# Node ID c7d2ae25d008d58d171c6663e1471d4763de0ec1
# Parent  414ebfd5389b163a7a7463ecfefee814a30ab23d
clarified signature: more accurate ML_Settings;

diff -r 414ebfd5389b -r c7d2ae25d008 src/Pure/Tools/doc.ML
--- a/src/Pure/Tools/doc.ML	Wed Jun 25 11:51:13 2025 +0200
+++ b/src/Pure/Tools/doc.ML	Wed Jun 25 12:08:12 2025 +0200
@@ -14,7 +14,7 @@
 
 fun check ctxt arg =
   Completion.check_item "documentation" (Markup.doc o #1)
-    (\<^scala>\<open>doc_names\<close> "" |> split_lines |> map (rpair ())) ctxt arg;
+    (\<^scala>\<open>doc_names\<close> ML_System.platform |> split_lines |> map (rpair ())) ctxt arg;
 
 val _ =
   Theory.setup
diff -r 414ebfd5389b -r c7d2ae25d008 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Wed Jun 25 11:51:13 2025 +0200
+++ b/src/Pure/Tools/doc.scala	Wed Jun 25 12:08:12 2025 +0200
@@ -67,8 +67,7 @@
       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES"))
         .flatMap(plain_file(_)))
 
-  def examples(): Contents = {
-    val ml_settings = ML_Settings.system(Options.init())
+  def examples(ml_settings: ML_Settings): Contents = {
     val env = Isabelle_System.Settings(putenv = List(ml_settings.ml_sources_root))
     Contents.section("Examples", true,
       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
@@ -116,15 +115,16 @@
     Contents(result.toList)
   }
 
-  def contents(): Contents = {
-    examples() ++ release_notes() ++ main_contents()
+  def contents(ml_settings: ML_Settings): Contents = {
+    examples(ml_settings) ++ release_notes() ++ main_contents()
   }
 
   object Doc_Names extends Scala.Fun_String("doc_names") {
     val here = Scala_Project.here
-    def apply(arg: String): String =
-      if (arg.nonEmpty) error("Bad argument: " + quote(arg))
-      else cat_lines((for (entry <- contents().entries(pdf = true)) yield entry.name).sorted)
+    def apply(arg: String): String = {
+      val ml_settings = ML_Settings.system(Options.init() + ("ML_platform=" + arg))
+      cat_lines((for (entry <- contents(ml_settings).entries(pdf = true)) yield entry.name).sorted)
+    }
   }
 
 
@@ -149,10 +149,12 @@
 """)
       val docs = getopts(args)
 
+      val ml_settings = ML_Settings.system(Options.init())
+
       if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
       else {
         docs.foreach(name =>
-          contents().entries(name = docs.contains).headOption match {
+          contents(ml_settings).entries(name = docs.contains).headOption match {
             case Some(entry) => entry.view()
             case None => error("No Isabelle documentation entry: " + quote(name))
           }
diff -r 414ebfd5389b -r c7d2ae25d008 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Wed Jun 25 11:51:13 2025 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Wed Jun 25 12:08:12 2025 +0200
@@ -17,7 +17,7 @@
 
 
 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) {
-  private val doc_contents = Doc.contents()
+  private val doc_contents = Doc.contents(PIDE.ml_settings)
 
   private val tree = new Tree_View(single_selection_mode = true)
 
diff -r 414ebfd5389b -r c7d2ae25d008 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jun 25 11:51:13 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jun 25 12:08:12 2025 +0200
@@ -175,7 +175,7 @@
   /* hyperlinks */
 
   def hyperlink_doc(name: String): Option[Hyperlink] =
-    Doc.contents().entries(name = _ == name).headOption.map(entry =>
+    Doc.contents(PIDE.ml_settings).entries(name = _ == name).headOption.map(entry =>
       new Hyperlink {
         override val external: Boolean = !entry.path.is_file
         def follow(view: View): Unit = goto_doc(view, entry.path)