--- 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.
--- 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"
--- 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
--- 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");
--- 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>
--- /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)
+}
--- 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