# HG changeset patch
# User wenzelm
# Date 1372172110 -7200
# Node ID 18a720984855b7138933d59185c91f69b26acac1
# Parent  2cfe6656d6d6becf8275a703a40bb8bbd26fe624
dockable window for Isabelle documentation;

diff -r 2cfe6656d6d6 -r 18a720984855 NEWS
--- a/NEWS	Tue Jun 25 12:17:19 2013 +0200
+++ b/NEWS	Tue Jun 25 16:55:10 2013 +0200
@@ -39,6 +39,9 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
+* Dockable window "Documentation" provides access to Isabelle
+documentation.
+
 * Dockable window "Timing" provides an overview of relevant command
 timing information.
 
diff -r 2cfe6656d6d6 -r 18a720984855 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Jun 25 12:17:19 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Jun 25 16:55:10 2013 +0200
@@ -12,6 +12,7 @@
   "src/dockable.scala"
   "src/document_model.scala"
   "src/document_view.scala"
+  "src/documentation_dockable.scala"
   "src/fold_handling.scala"
   "src/graphview_dockable.scala"
   "src/html_panel.scala"
diff -r 2cfe6656d6d6 -r 18a720984855 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Tue Jun 25 12:17:19 2013 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Tue Jun 25 16:55:10 2013 +0200
@@ -30,6 +30,7 @@
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
 plugin.isabelle.jedit.Plugin.menu= \
+  isabelle.documentation-panel \
   isabelle.monitor-panel \
   isabelle.output-panel \
   isabelle.protocol-panel \
@@ -39,6 +40,7 @@
   isabelle.syslog-panel \
   isabelle.theories-panel \
   isabelle.timing-panel
+isabelle.documentation-panel.label=Documentation panel
 isabelle.monitor-panel.label=Monitor panel
 isabelle.output-panel.label=Output panel
 isabelle.protocol-panel.label=Protocol panel
@@ -56,6 +58,7 @@
 isabelle-output.title=Output
 isabelle-protocol.title=Protocol
 isabelle-raw-output.title=Raw Output
+isabelle-documentation.title=Documentation
 isabelle-readme.title=README
 isabelle-symbols.title=Symbols
 isabelle-syslog.title=Syslog
diff -r 2cfe6656d6d6 -r 18a720984855 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Tue Jun 25 12:17:19 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Tue Jun 25 16:55:10 2013 +0200
@@ -17,6 +17,11 @@
 			wm.addDockableWindow("isabelle-syslog");
 		</CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.documentation-panel">
+		<CODE>
+			wm.addDockableWindow("isabelle-documentation");
+		</CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.readme-panel">
 		<CODE>
 			wm.addDockableWindow("isabelle-readme");
diff -r 2cfe6656d6d6 -r 18a720984855 src/Tools/jEdit/src/dockables.xml
--- a/src/Tools/jEdit/src/dockables.xml	Tue Jun 25 12:17:19 2013 +0200
+++ b/src/Tools/jEdit/src/dockables.xml	Tue Jun 25 16:55:10 2013 +0200
@@ -11,6 +11,9 @@
 	<DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
 		new isabelle.jedit.Syslog_Dockable(view, position);
 	</DOCKABLE>
+	<DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
+		new isabelle.jedit.Documentation_Dockable(view, position);
+	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-readme" MOVABLE="TRUE">
 		new isabelle.jedit.README_Dockable(view, position);
 	</DOCKABLE>
diff -r 2cfe6656d6d6 -r 18a720984855 src/Tools/jEdit/src/documentation_dockable.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Jun 25 16:55:10 2013 +0200
@@ -0,0 +1,67 @@
+/*  Title:      Tools/jEdit/src/documentation_dockable.scala
+    Author:     Makarius
+
+Dockable window for Isabelle documentation.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.{Dimension, GridLayout}
+import javax.swing.{JTree, JScrollPane}
+import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
+import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
+
+import org.gjt.sp.jedit.{View, OperatingSystem}
+
+
+class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+  Swing_Thread.require()
+
+  private val docs = Doc.contents()
+
+  private case class Documentation(name: String, title: String)
+  {
+    override def toString =
+      "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
+  }
+
+  private val root = new DefaultMutableTreeNode
+  docs foreach {
+    case Doc.Section(text) =>
+      root.add(new DefaultMutableTreeNode(text))
+    case Doc.Doc(name, title) =>
+      root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
+        .add(new DefaultMutableTreeNode(Documentation(name, title)))
+  }
+
+  private val tree = new JTree(root)
+  if (!OperatingSystem.isMacOSLF)
+    tree.putClientProperty("JTree.lineStyle", "Angled")
+  tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
+  tree.addTreeSelectionListener(
+    new TreeSelectionListener {
+      override def valueChanged(e: TreeSelectionEvent)
+      {
+        tree.getLastSelectedPathComponent match {
+          case node: DefaultMutableTreeNode =>
+            node.getUserObject match {
+              case Documentation(name, _) => Doc.view(name)
+              case _ =>
+            }
+          case _ =>
+        }
+      }
+    })
+  tree.setRootVisible(false)
+  tree.setVisibleRowCount(docs.length)
+  (0 until docs.length).foreach(tree.expandRow)
+
+  private val tree_view = new JScrollPane(tree)
+  tree_view.setMinimumSize(new Dimension(100, 50))
+
+  set_content(tree_view)
+}
diff -r 2cfe6656d6d6 -r 18a720984855 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Tue Jun 25 12:17:19 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Tue Jun 25 16:55:10 2013 +0200
@@ -181,6 +181,7 @@
 isabelle-output.dock-position=bottom
 isabelle-output.height=174
 isabelle-output.width=412
+isabelle-documentation.dock-position=right
 isabelle-readme.dock-position=bottom
 isabelle-symbols.dock-position=bottom
 isabelle-theories.dock-position=right