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;
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@52445
    27
      "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(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@57920
    57
        PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
wenzelm@57920
    58
      case Documentation(_, _, path) =>
wenzelm@57920
    59
        if (path.is_file)
wenzelm@57920
    60
          PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
wenzelm@57920
    61
        else {
wenzelm@57920
    62
          Future.fork {
wenzelm@57920
    63
            try { Doc.view(path) }
wenzelm@57920
    64
            catch {
wenzelm@57920
    65
              case exn: Throwable =>
wenzelm@57920
    66
                GUI.error_dialog(view,
wenzelm@57920
    67
                  "Documentation error", GUI.scrollable_text(Exn.message(exn)))
wenzelm@57920
    68
            }
wenzelm@57920
    69
          }
wenzelm@57920
    70
        }
wenzelm@57920
    71
      case _ =>
wenzelm@57920
    72
    }
wenzelm@57920
    73
  }
wenzelm@57920
    74
wenzelm@57920
    75
  tree.addKeyListener(new KeyAdapter {
wenzelm@57920
    76
    override def keyPressed(e: KeyEvent)
wenzelm@57920
    77
    {
wenzelm@57920
    78
      if (e.getKeyCode == KeyEvent.VK_ENTER) {
wenzelm@57920
    79
        e.consume
wenzelm@57920
    80
        val path = tree.getSelectionPath
wenzelm@57920
    81
        if (path != null) {
wenzelm@57920
    82
          path.getLastPathComponent match {
wenzelm@57920
    83
            case node: DefaultMutableTreeNode => action(node)
wenzelm@57920
    84
            case _ =>
wenzelm@57920
    85
          }
wenzelm@57920
    86
        }
wenzelm@57920
    87
      }
wenzelm@57920
    88
    }
wenzelm@57920
    89
  })
wenzelm@54686
    90
  tree.addMouseListener(new MouseAdapter {
wenzelm@57920
    91
    override def mouseClicked(e: MouseEvent)
wenzelm@57920
    92
    {
wenzelm@54686
    93
      val click = tree.getPathForLocation(e.getX, e.getY)
wenzelm@54686
    94
      if (click != null && e.getClickCount == 1) {
wenzelm@54686
    95
        (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
wenzelm@54686
    96
          case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
wenzelm@57920
    97
            action(node)
wenzelm@52445
    98
          case _ =>
wenzelm@52445
    99
        }
wenzelm@52445
   100
      }
wenzelm@54686
   101
    }
wenzelm@54686
   102
  })
wenzelm@56423
   103
wenzelm@56423
   104
  {
wenzelm@56423
   105
    var expand = true
wenzelm@56423
   106
    var visible = 0
wenzelm@56423
   107
    def make_visible(row: Int) { visible += 1; tree.expandRow(row) }
wenzelm@56423
   108
    for ((entry, row) <- docs.zipWithIndex) {
wenzelm@56423
   109
      entry match {
wenzelm@56423
   110
        case Doc.Section(_, important) =>
wenzelm@56423
   111
          expand = important
wenzelm@56423
   112
          make_visible(row)
wenzelm@56423
   113
        case _ =>
wenzelm@56423
   114
          if (expand) make_visible(row)
wenzelm@56423
   115
      }
wenzelm@56423
   116
    }
wenzelm@56423
   117
    tree.setRootVisible(false)
wenzelm@56423
   118
    tree.setVisibleRowCount(visible)
wenzelm@56423
   119
  }
wenzelm@52445
   120
wenzelm@52445
   121
  private val tree_view = new JScrollPane(tree)
wenzelm@60849
   122
  tree_view.setMinimumSize(new Dimension(200, 50))
wenzelm@52445
   123
wenzelm@52445
   124
  set_content(tree_view)
wenzelm@52445
   125
}