quick access to release notes (imitating website/documentation.html);
authorwenzelm
Sat Jul 06 21:51:35 2013 +0200 (2013-07-06)
changeset 5254197c950217d7f
parent 52540 c1ddd91ba515
child 52542 19d674acb764
quick access to release notes (imitating website/documentation.html);
src/Pure/Tools/doc.scala
src/Tools/jEdit/src/documentation_dockable.scala
     1.1 --- a/src/Pure/Tools/doc.scala	Sat Jul 06 21:50:14 2013 +0200
     1.2 +++ b/src/Pure/Tools/doc.scala	Sat Jul 06 21:51:35 2013 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4      Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
     1.5        if (dir.is_dir) dir
     1.6        else error("Bad documentation directory: " + dir))
     1.7 -
     1.8 +    
     1.9  
    1.10    /* contents */
    1.11  
    1.12 @@ -33,12 +33,21 @@
    1.13    sealed abstract class Entry
    1.14    case class Section(text: String) extends Entry
    1.15    case class Doc(name: String, title: String) extends Entry
    1.16 +  case class Text_File(path: Path) extends Entry
    1.17  
    1.18    private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    1.19    private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    1.20  
    1.21 +  private val release_notes =
    1.22 +    List(Section("Release notes"),
    1.23 +      Text_File(Path.explode("~~/ANNOUNCE")),
    1.24 +      Text_File(Path.explode("~~/README")),
    1.25 +      Text_File(Path.explode("~~/NEWS")),
    1.26 +      Text_File(Path.explode("~~/COPYRIGHT")),
    1.27 +      Text_File(Path.explode("~~/CONTRIBUTORS")))
    1.28 +
    1.29    def contents(): List[Entry] =
    1.30 -    for {
    1.31 +    (for {
    1.32        line <- contents_lines()
    1.33        entry <-
    1.34          line match {
    1.35 @@ -46,7 +55,7 @@
    1.36            case Doc_Entry(name, title) => Some(Doc(name, title))
    1.37            case _ => None
    1.38          }
    1.39 -    } yield entry
    1.40 +    } yield entry) ::: release_notes
    1.41  
    1.42  
    1.43    /* view */
     2.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Jul 06 21:50:14 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Jul 06 21:51:35 2013 +0200
     2.3 @@ -29,6 +29,11 @@
     2.4        "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
     2.5    }
     2.6  
     2.7 +  private case class Text_File(path: Path)
     2.8 +  {
     2.9 +    override def toString = path.base.implode
    2.10 +  }
    2.11 +
    2.12    private val root = new DefaultMutableTreeNode
    2.13    docs foreach {
    2.14      case Doc.Section(text) =>
    2.15 @@ -36,6 +41,13 @@
    2.16      case Doc.Doc(name, title) =>
    2.17        root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    2.18          .add(new DefaultMutableTreeNode(Documentation(name, title)))
    2.19 +    case Doc.Text_File(path: Path) =>
    2.20 +      root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    2.21 +        .add(new DefaultMutableTreeNode(Text_File(path.expand)))
    2.22 +  }
    2.23 +
    2.24 +  private def documentation_error(exn: Throwable) {
    2.25 +    GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    2.26    }
    2.27  
    2.28    private val tree = new JTree(root)
    2.29 @@ -52,11 +64,10 @@
    2.30                case Documentation(name, _) =>
    2.31                  default_thread_pool.submit(() =>
    2.32                    try { Doc.view(name) }
    2.33 -                  catch {
    2.34 -                    case exn: Throwable =>
    2.35 -                      GUI.error_dialog(view,
    2.36 -                        "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    2.37 -                  })
    2.38 +                  catch { case exn: Throwable => documentation_error(exn) })
    2.39 +              case Text_File(path) =>
    2.40 +                  try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) }
    2.41 +                  catch { case exn: Throwable => documentation_error(exn) }
    2.42                case _ =>
    2.43              }
    2.44            case _ =>