# HG changeset patch
# User wenzelm
# Date 1579441803 -3600
# Node ID 028edb1e5b99695d477e483e35c1166d889af190
# Parent  c1c61d0d8e7c95d95118e0703252e993f5b64e9c
clarified file names;

diff -r c1c61d0d8e7c -r 028edb1e5b99 Admin/polyml/settings
--- a/Admin/polyml/settings	Sun Jan 19 14:23:49 2020 +0100
+++ b/Admin/polyml/settings	Sun Jan 19 14:50:03 2020 +0100
@@ -16,4 +16,4 @@
 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
 ML_SOURCES="$POLYML_HOME/src"
 
-ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:$POLYML_HOME/src/ROOT.ML"
+ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT.ML"
diff -r c1c61d0d8e7c -r 028edb1e5b99 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sun Jan 19 14:23:49 2020 +0100
+++ b/src/Pure/Tools/doc.scala	Sun Jan 19 14:50:03 2020 +0100
@@ -33,20 +33,13 @@
   case class Doc(name: String, title: String, path: Path) extends Entry
   case class Text_File(name: String, path: Path) extends Entry
 
-  private val Variable_Path = new Regex("""^\$[^/]+/+(.+)$""")
-
   def text_file(path: Path): Option[Text_File] =
-  {
     if (path.is_file) {
-      val name =
-        path.implode match {
-          case Variable_Path(name) => name
-          case name => name
-        }
-      Some(Text_File(name, path))
+      val a = path.implode
+      val b = Library.try_unprefix("$ISABELLE_HOME/", a).getOrElse(a)
+      Some(Text_File(b, path))
     }
     else None
-  }
 
   private val Section_Entry = new Regex("""^(\S.*)\s*$""")
   private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")