src/Pure/Tools/doc.scala
changeset 71397 028edb1e5b99
parent 69409 e7a5340128f0
child 71601 97ccf48c2f0c
--- 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*$""")