# HG changeset patch # User wenzelm # Date 1373140295 -7200 # Node ID 97c950217d7f34e838174d7432e122a02ddc6a5b # Parent c1ddd91ba515abe6c7e7eab39a038f6c9a515ad0 quick access to release notes (imitating website/documentation.html); diff -r c1ddd91ba515 -r 97c950217d7f src/Pure/Tools/doc.scala --- 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 */ diff -r c1ddd91ba515 -r 97c950217d7f src/Tools/jEdit/src/documentation_dockable.scala --- 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.encode(name) + ": " + HTML.encode(title) + "" } + 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 _ =>