--- 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
--- 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
}