src/Tools/jEdit/src/documentation_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 62113 16de2a9b5b3d
child 65246 848965b5befc
permissions -rw-r--r--
tuned signature;
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@60847
    12
import java.awt.Dimension
wenzelm@57920
    13
import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
wenzelm@60847
    14
import javax.swing.{JTree, JScrollPane}
wenzelm@52445
    15
import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
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
  private val docs = Doc.contents()
wenzelm@52445
    23
wenzelm@56422
    24
  private case class Documentation(name: String, title: String, path: Path)
wenzelm@52445
    25
  {
wenzelm@57912
    26
    override def toString: String =
wenzelm@62113
    27
      "<html><b>" + HTML.output(name) + "</b>:  " + HTML.output(title) + "</html>"
wenzelm@52445
    28
  }
wenzelm@52445
    29
wenzelm@52542
    30
  private case class Text_File(name: String, path: Path)
wenzelm@52541
    31
  {
wenzelm@57912
    32
    override def toString: String = name
wenzelm@52541
    33
  }
wenzelm@52541
    34
wenzelm@52445
    35
  private val root = new DefaultMutableTreeNode
wenzelm@52445
    36
  docs foreach {
wenzelm@56423
    37
    case Doc.Section(text, _) =>
wenzelm@52445
    38
      root.add(new DefaultMutableTreeNode(text))
wenzelm@56422
    39
    case Doc.Doc(name, title, path) =>
wenzelm@52445
    40
      root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
wenzelm@56422
    41
        .add(new DefaultMutableTreeNode(Documentation(name, title, path)))
wenzelm@52542
    42
    case Doc.Text_File(name: String, path: Path) =>
wenzelm@52541
    43
      root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
wenzelm@52542
    44
        .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
wenzelm@52541
    45
  }
wenzelm@52541
    46
wenzelm@52445
    47
  private val tree = new JTree(root)
wenzelm@60292
    48
  tree.setRowHeight(0)
wenzelm@60847
    49
  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
wenzelm@54687
    50
wenzelm@57920
    51
  override def focusOnDefaultComponent { tree.requestFocusInWindow }
wenzelm@54687
    52
wenzelm@57920
    53
  private def action(node: DefaultMutableTreeNode)
wenzelm@57920
    54
  {
wenzelm@57920
    55
    node.getUserObject match {
wenzelm@57920
    56
      case Text_File(_, path) =>
wenzelm@60988
    57
        PIDE.editor.goto_file(true, view, File.platform_path(path))
wenzelm@57920
    58
      case Documentation(_, _, path) =>
wenzelm@61660
    59
        PIDE.editor.goto_doc(view, path)
wenzelm@57920
    60
      case _ =>
wenzelm@57920
    61
    }
wenzelm@57920
    62
  }
wenzelm@57920
    63
wenzelm@57920
    64
  tree.addKeyListener(new KeyAdapter {
wenzelm@57920
    65
    override def keyPressed(e: KeyEvent)
wenzelm@57920
    66
    {
wenzelm@57920
    67
      if (e.getKeyCode == KeyEvent.VK_ENTER) {
wenzelm@57920
    68
        e.consume
wenzelm@57920
    69
        val path = tree.getSelectionPath
wenzelm@57920
    70
        if (path != null) {
wenzelm@57920
    71
          path.getLastPathComponent match {
wenzelm@57920
    72
            case node: DefaultMutableTreeNode => action(node)
wenzelm@57920
    73
            case _ =>
wenzelm@57920
    74
          }
wenzelm@57920
    75
        }
wenzelm@57920
    76
      }
wenzelm@57920
    77
    }
wenzelm@57920
    78
  })
wenzelm@54686
    79
  tree.addMouseListener(new MouseAdapter {
wenzelm@57920
    80
    override def mouseClicked(e: MouseEvent)
wenzelm@57920
    81
    {
wenzelm@54686
    82
      val click = tree.getPathForLocation(e.getX, e.getY)
wenzelm@54686
    83
      if (click != null && e.getClickCount == 1) {
wenzelm@54686
    84
        (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
wenzelm@54686
    85
          case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
wenzelm@57920
    86
            action(node)
wenzelm@52445
    87
          case _ =>
wenzelm@52445
    88
        }
wenzelm@52445
    89
      }
wenzelm@54686
    90
    }
wenzelm@54686
    91
  })
wenzelm@56423
    92
wenzelm@56423
    93
  {
wenzelm@56423
    94
    var expand = true
wenzelm@56423
    95
    var visible = 0
wenzelm@56423
    96
    def make_visible(row: Int) { visible += 1; tree.expandRow(row) }
wenzelm@56423
    97
    for ((entry, row) <- docs.zipWithIndex) {
wenzelm@56423
    98
      entry match {
wenzelm@56423
    99
        case Doc.Section(_, important) =>
wenzelm@56423
   100
          expand = important
wenzelm@56423
   101
          make_visible(row)
wenzelm@56423
   102
        case _ =>
wenzelm@56423
   103
          if (expand) make_visible(row)
wenzelm@56423
   104
      }
wenzelm@56423
   105
    }
wenzelm@56423
   106
    tree.setRootVisible(false)
wenzelm@56423
   107
    tree.setVisibleRowCount(visible)
wenzelm@56423
   108
  }
wenzelm@52445
   109
wenzelm@52445
   110
  private val tree_view = new JScrollPane(tree)
wenzelm@60849
   111
  tree_view.setMinimumSize(new Dimension(200, 50))
wenzelm@52445
   112
wenzelm@52445
   113
  set_content(tree_view)
wenzelm@52445
   114
}