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