# HG changeset patch
# User wenzelm
# Date 1541934804 -3600
# Node ID 39044da8bb5a9f98706f1144143e06f38c08826d
# Parent  94fa3376ba33a7768fefcb8183420c34390e33b6
clarified display name;

diff -r 94fa3376ba33 -r 39044da8bb5a etc/settings
--- a/etc/settings	Sat Nov 10 19:39:38 2018 +0100
+++ b/etc/settings	Sun Nov 11 12:13:24 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 94fa3376ba33 -r 39044da8bb5a src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sat Nov 10 19:39:38 2018 +0100
+++ b/src/Pure/Tools/doc.scala	Sun Nov 11 12:13:24 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
   }