clarified display name;
authorwenzelm
Sun Nov 11 12:13:24 2018 +0100 (11 months ago ago)
changeset 6929039044da8bb5a
parent 69287 94fa3376ba33
child 69291 b9dd40e2c470
clarified display name;
etc/settings
src/Pure/Tools/doc.scala
     1.1 --- a/etc/settings	Sat Nov 10 19:39:38 2018 +0100
     1.2 +++ b/etc/settings	Sun Nov 11 12:13:24 2018 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4  ISABELLE_DOCS="$ISABELLE_HOME/doc"
     1.5  
     1.6  ISABELLE_DOCS_RELEASE_NOTES="ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:src/Tools/jEdit/README:README_REPOSITORY"
     1.7 -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"
     1.8 +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"
     1.9  
    1.10  # "open" within desktop environment (potentially asynchronous)
    1.11  case "$ISABELLE_PLATFORM_FAMILY" in
     2.1 --- a/src/Pure/Tools/doc.scala	Sat Nov 10 19:39:38 2018 +0100
     2.2 +++ b/src/Pure/Tools/doc.scala	Sun Nov 11 12:13:24 2018 +0100
     2.3 @@ -33,10 +33,18 @@
     2.4    case class Doc(name: String, title: String, path: Path) extends Entry
     2.5    case class Text_File(name: String, path: Path) extends Entry
     2.6  
     2.7 -  def text_file(name: Path): Option[Text_File] =
     2.8 +  private val Variable_Path = new Regex("""^\$[^/]+/+(.+)$""")
     2.9 +
    2.10 +  def text_file(path: Path): Option[Text_File] =
    2.11    {
    2.12 -    val path = Path.variable("ISABELLE_HOME") + name
    2.13 -    if (path.is_file) Some(Text_File(name.implode, path))
    2.14 +    if (path.is_file) {
    2.15 +      val name =
    2.16 +        path.implode match {
    2.17 +          case Variable_Path(name) => name
    2.18 +          case name => name
    2.19 +        }
    2.20 +      Some(Text_File(name, path))
    2.21 +    }
    2.22      else None
    2.23    }
    2.24