equal
deleted
inserted
replaced
16 case class Section(title: String, important: Boolean, entries: List[Entry]) |
16 case class Section(title: String, important: Boolean, entries: List[Entry]) |
17 case class Entry(name: String, path: Path, title: String = "") { |
17 case class Entry(name: String, path: Path, title: String = "") { |
18 def view(): Unit = Doc.view(path) |
18 def view(): Unit = Doc.view(path) |
19 override def toString: String = // GUI label |
19 override def toString: String = // GUI label |
20 if (title.nonEmpty) { |
20 if (title.nonEmpty) { |
21 "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>" |
21 "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>" |
22 } |
22 } |
23 else name |
23 else name |
24 } |
24 } |
25 |
25 |
26 def plain_file(path: Path): Option[Entry] = |
26 def plain_file(path: Path): Option[Entry] = |