--- a/src/Pure/Tools/doc.scala Sat Jul 06 21:50:14 2013 +0200
+++ b/src/Pure/Tools/doc.scala Sat Jul 06 21:51:35 2013 +0200
@@ -18,7 +18,7 @@
Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
if (dir.is_dir) dir
else error("Bad documentation directory: " + dir))
-
+
/* contents */
@@ -33,12 +33,21 @@
sealed abstract class Entry
case class Section(text: String) extends Entry
case class Doc(name: String, title: String) extends Entry
+ case class Text_File(path: Path) extends Entry
private val Section_Entry = new Regex("""^(\S.*)\s*$""")
private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
+ private val release_notes =
+ List(Section("Release notes"),
+ Text_File(Path.explode("~~/ANNOUNCE")),
+ Text_File(Path.explode("~~/README")),
+ Text_File(Path.explode("~~/NEWS")),
+ Text_File(Path.explode("~~/COPYRIGHT")),
+ Text_File(Path.explode("~~/CONTRIBUTORS")))
+
def contents(): List[Entry] =
- for {
+ (for {
line <- contents_lines()
entry <-
line match {
@@ -46,7 +55,7 @@
case Doc_Entry(name, title) => Some(Doc(name, title))
case _ => None
}
- } yield entry
+ } yield entry) ::: release_notes
/* view */
--- a/src/Tools/jEdit/src/documentation_dockable.scala Sat Jul 06 21:50:14 2013 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Jul 06 21:51:35 2013 +0200
@@ -29,6 +29,11 @@
"<html><b>" + HTML.encode(name) + "</b>: " + HTML.encode(title) + "</html>"
}
+ private case class Text_File(path: Path)
+ {
+ override def toString = path.base.implode
+ }
+
private val root = new DefaultMutableTreeNode
docs foreach {
case Doc.Section(text) =>
@@ -36,6 +41,13 @@
case Doc.Doc(name, title) =>
root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
.add(new DefaultMutableTreeNode(Documentation(name, title)))
+ case Doc.Text_File(path: Path) =>
+ root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
+ .add(new DefaultMutableTreeNode(Text_File(path.expand)))
+ }
+
+ private def documentation_error(exn: Throwable) {
+ GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn)))
}
private val tree = new JTree(root)
@@ -52,11 +64,10 @@
case Documentation(name, _) =>
default_thread_pool.submit(() =>
try { Doc.view(name) }
- catch {
- case exn: Throwable =>
- GUI.error_dialog(view,
- "Documentation error", GUI.scrollable_text(Exn.message(exn)))
- })
+ catch { case exn: Throwable => documentation_error(exn) })
+ case Text_File(path) =>
+ try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) }
+ catch { case exn: Throwable => documentation_error(exn) }
case _ =>
}
case _ =>