equal
deleted
inserted
replaced
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] = |