src/Pure/Tools/doc.scala
changeset 71397 028edb1e5b99
parent 69409 e7a5340128f0
child 71601 97ccf48c2f0c
equal deleted inserted replaced
71396:c1c61d0d8e7c 71397:028edb1e5b99
    31   sealed abstract class Entry
    31   sealed abstract class Entry
    32   case class Section(text: String, important: Boolean) extends Entry
    32   case class Section(text: String, important: Boolean) extends Entry
    33   case class Doc(name: String, title: String, path: Path) extends Entry
    33   case class Doc(name: String, title: String, path: Path) extends Entry
    34   case class Text_File(name: String, path: Path) extends Entry
    34   case class Text_File(name: String, path: Path) extends Entry
    35 
    35 
    36   private val Variable_Path = new Regex("""^\$[^/]+/+(.+)$""")
       
    37 
       
    38   def text_file(path: Path): Option[Text_File] =
    36   def text_file(path: Path): Option[Text_File] =
    39   {
       
    40     if (path.is_file) {
    37     if (path.is_file) {
    41       val name =
    38       val a = path.implode
    42         path.implode match {
    39       val b = Library.try_unprefix("$ISABELLE_HOME/", a).getOrElse(a)
    43           case Variable_Path(name) => name
    40       Some(Text_File(b, path))
    44           case name => name
       
    45         }
       
    46       Some(Text_File(name, path))
       
    47     }
    41     }
    48     else None
    42     else None
    49   }
       
    50 
    43 
    51   private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    44   private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    52   private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    45   private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    53 
    46 
    54   private def release_notes(): List[Entry] =
    47   private def release_notes(): List[Entry] =