src/Tools/jEdit/src/documentation_dockable.scala
author wenzelm
Mon Aug 10 13:54:12 2015 +0200 (2015-08-10)
changeset 60873 974d9acb2b87
parent 60849 6e49311ef842
child 60893 3c8b9b4b577c
permissions -rw-r--r--
tuned imports;
     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
    13 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
    14 import javax.swing.{JTree, JScrollPane}
    15 import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
    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   private val docs = Doc.contents()
    23 
    24   private case class Documentation(name: String, title: String, path: Path)
    25   {
    26     override def toString: String =
    27       "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
    28   }
    29 
    30   private case class Text_File(name: String, path: Path)
    31   {
    32     override def toString: String = name
    33   }
    34 
    35   private val root = new DefaultMutableTreeNode
    36   docs foreach {
    37     case Doc.Section(text, _) =>
    38       root.add(new DefaultMutableTreeNode(text))
    39     case Doc.Doc(name, title, path) =>
    40       root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    41         .add(new DefaultMutableTreeNode(Documentation(name, title, path)))
    42     case Doc.Text_File(name: String, path: Path) =>
    43       root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    44         .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
    45   }
    46 
    47   private val tree = new JTree(root)
    48   tree.setRowHeight(0)
    49   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
    50 
    51   override def focusOnDefaultComponent { tree.requestFocusInWindow }
    52 
    53   private def action(node: DefaultMutableTreeNode)
    54   {
    55     node.getUserObject match {
    56       case Text_File(_, path) =>
    57         PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    58       case Documentation(_, _, path) =>
    59         if (path.is_file)
    60           PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    61         else {
    62           Future.fork {
    63             try { Doc.view(path) }
    64             catch {
    65               case exn: Throwable =>
    66                 GUI.error_dialog(view,
    67                   "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    68             }
    69           }
    70         }
    71       case _ =>
    72     }
    73   }
    74 
    75   tree.addKeyListener(new KeyAdapter {
    76     override def keyPressed(e: KeyEvent)
    77     {
    78       if (e.getKeyCode == KeyEvent.VK_ENTER) {
    79         e.consume
    80         val path = tree.getSelectionPath
    81         if (path != null) {
    82           path.getLastPathComponent match {
    83             case node: DefaultMutableTreeNode => action(node)
    84             case _ =>
    85           }
    86         }
    87       }
    88     }
    89   })
    90   tree.addMouseListener(new MouseAdapter {
    91     override def mouseClicked(e: MouseEvent)
    92     {
    93       val click = tree.getPathForLocation(e.getX, e.getY)
    94       if (click != null && e.getClickCount == 1) {
    95         (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
    96           case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
    97             action(node)
    98           case _ =>
    99         }
   100       }
   101     }
   102   })
   103 
   104   {
   105     var expand = true
   106     var visible = 0
   107     def make_visible(row: Int) { visible += 1; tree.expandRow(row) }
   108     for ((entry, row) <- docs.zipWithIndex) {
   109       entry match {
   110         case Doc.Section(_, important) =>
   111           expand = important
   112           make_visible(row)
   113         case _ =>
   114           if (expand) make_visible(row)
   115       }
   116     }
   117     tree.setRootVisible(false)
   118     tree.setVisibleRowCount(visible)
   119   }
   120 
   121   private val tree_view = new JScrollPane(tree)
   122   tree_view.setMinimumSize(new Dimension(200, 50))
   123 
   124   set_content(tree_view)
   125 }