# HG changeset patch
# User nipkow
# Date 1541943242 -3600
# Node ID b9dd40e2c47084bded0b2cdd35c2a694da1536cc
# Parent  39044da8bb5a9f98706f1144143e06f38c08826d# Parent  3273692de24a411be04cdd918e8f3b5017f84380
merged

diff -r 3273692de24a -r b9dd40e2c470 etc/settings
--- a/etc/settings	Sun Nov 11 13:05:15 2018 +0100
+++ b/etc/settings	Sun Nov 11 14:34:02 2018 +0100
@@ -111,7 +111,7 @@
 ISABELLE_DOCS="$ISABELLE_HOME/doc"
 
 ISABELLE_DOCS_RELEASE_NOTES="ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:src/Tools/jEdit/README:README_REPOSITORY"
-ISABELLE_DOCS_EXAMPLES="src/HOL/ex/Seq.thy:src/HOL/ex/ML.thy:src/HOL/Unix/Unix.thy:src/HOL/Isar_Examples/Drinker.thy:src/Tools/SML/Examples.thy:src/Pure/ROOT.ML"
+ISABELLE_DOCS_EXAMPLES="~~/src/HOL/ex/Seq.thy:~~/src/HOL/ex/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/HOL/Isar_Examples/Drinker.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML"
 
 # "open" within desktop environment (potentially asynchronous)
 case "$ISABELLE_PLATFORM_FAMILY" in
diff -r 3273692de24a -r b9dd40e2c470 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sun Nov 11 13:05:15 2018 +0100
+++ b/src/Pure/Tools/doc.scala	Sun Nov 11 14:34:02 2018 +0100
@@ -33,10 +33,18 @@
   case class Doc(name: String, title: String, path: Path) extends Entry
   case class Text_File(name: String, path: Path) extends Entry
 
-  def text_file(name: Path): Option[Text_File] =
+  private val Variable_Path = new Regex("""^\$[^/]+/+(.+)$""")
+
+  def text_file(path: Path): Option[Text_File] =
   {
-    val path = Path.variable("ISABELLE_HOME") + name
-    if (path.is_file) Some(Text_File(name.implode, path))
+    if (path.is_file) {
+      val name =
+        path.implode match {
+          case Variable_Path(name) => name
+          case name => name
+        }
+      Some(Text_File(name, path))
+    }
     else None
   }