src/Tools/jEdit/src/documentation_dockable.scala
author wenzelm
Sat Jul 06 21:51:35 2013 +0200 (2013-07-06)
changeset 52541 97c950217d7f
parent 52447 9a74000426e2
child 52542 19d674acb764
permissions -rw-r--r--
quick access to release notes (imitating website/documentation.html);
     1 /*  Title:      Tools/jEdit/src/documentation_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for Isabelle documentation.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{Dimension, GridLayout}
    13 import javax.swing.{JTree, JScrollPane}
    14 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
    15 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
    16 
    17 import org.gjt.sp.jedit.{View, OperatingSystem}
    18 
    19 
    20 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
    21 {
    22   Swing_Thread.require()
    23 
    24   private val docs = Doc.contents()
    25 
    26   private case class Documentation(name: String, title: String)
    27   {
    28     override def toString =
    29       "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
    30   }
    31 
    32   private case class Text_File(path: Path)
    33   {
    34     override def toString = path.base.implode
    35   }
    36 
    37   private val root = new DefaultMutableTreeNode
    38   docs foreach {
    39     case Doc.Section(text) =>
    40       root.add(new DefaultMutableTreeNode(text))
    41     case Doc.Doc(name, title) =>
    42       root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    43         .add(new DefaultMutableTreeNode(Documentation(name, title)))
    44     case Doc.Text_File(path: Path) =>
    45       root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    46         .add(new DefaultMutableTreeNode(Text_File(path.expand)))
    47   }
    48 
    49   private def documentation_error(exn: Throwable) {
    50     GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    51   }
    52 
    53   private val tree = new JTree(root)
    54   if (!OperatingSystem.isMacOSLF)
    55     tree.putClientProperty("JTree.lineStyle", "Angled")
    56   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
    57   tree.addTreeSelectionListener(
    58     new TreeSelectionListener {
    59       override def valueChanged(e: TreeSelectionEvent)
    60       {
    61         tree.getLastSelectedPathComponent match {
    62           case node: DefaultMutableTreeNode =>
    63             node.getUserObject match {
    64               case Documentation(name, _) =>
    65                 default_thread_pool.submit(() =>
    66                   try { Doc.view(name) }
    67                   catch { case exn: Throwable => documentation_error(exn) })
    68               case Text_File(path) =>
    69                   try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) }
    70                   catch { case exn: Throwable => documentation_error(exn) }
    71               case _ =>
    72             }
    73           case _ =>
    74         }
    75       }
    76     })
    77   tree.setRootVisible(false)
    78   tree.setVisibleRowCount(docs.length)
    79   (0 until docs.length).foreach(tree.expandRow)
    80 
    81   private val tree_view = new JScrollPane(tree)
    82   tree_view.setMinimumSize(new Dimension(100, 50))
    83 
    84   set_content(tree_view)
    85 }