--- a/etc/build.props Fri Aug 12 12:19:23 2022 +0200
+++ b/etc/build.props Fri Aug 12 12:50:19 2022 +0200
@@ -236,6 +236,7 @@
src/Tools/jEdit/src/context_menu.scala \
src/Tools/jEdit/src/debugger_dockable.scala \
src/Tools/jEdit/src/dockable.scala \
+ src/Tools/jEdit/src/document_dockable.scala \
src/Tools/jEdit/src/document_model.scala \
src/Tools/jEdit/src/document_view.scala \
src/Tools/jEdit/src/documentation_dockable.scala \
--- a/src/Tools/jEdit/jedit_main/dockables.scala Fri Aug 12 12:19:23 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/dockables.scala Fri Aug 12 12:50:19 2022 +0200
@@ -13,6 +13,9 @@
class Debugger_Dockable(view: View, position: String)
extends isabelle.jedit.Debugger_Dockable(view, position)
+class Document_Dockable(view: View, position: String)
+ extends isabelle.jedit.Document_Dockable(view, position)
+
class Documentation_Dockable(view: View, position: String)
extends isabelle.jedit.Documentation_Dockable(view, position)
--- a/src/Tools/jEdit/jedit_main/dockables.xml Fri Aug 12 12:19:23 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/dockables.xml Fri Aug 12 12:50:19 2022 +0200
@@ -5,6 +5,9 @@
<DOCKABLE NAME="isabelle-debugger" MOVABLE="TRUE">
new isabelle.jedit_main.Debugger_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-document" MOVABLE="TRUE">
+ new isabelle.jedit_main.Document_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
new isabelle.jedit_main.Documentation_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/jedit_main/plugin.props Fri Aug 12 12:19:23 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/plugin.props Fri Aug 12 12:50:19 2022 +0200
@@ -37,6 +37,7 @@
isabelle.java-monitor \
- \
isabelle-debugger \
+ isabelle-document \
isabelle-documentation \
isabelle-monitor \
isabelle-output \
@@ -52,6 +53,8 @@
isabelle-timing
isabelle-debugger.label=Debugger panel
isabelle-debugger.title=Debugger
+isabelle-document.label=Document panel
+isabelle-document.title=Document
isabelle-documentation.label=Documentation panel
isabelle-documentation.title=Documentation
isabelle-graphview.label=Graphview panel
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/document_dockable.scala Fri Aug 12 12:50:19 2022 +0200
@@ -0,0 +1,92 @@
+/* Title: Tools/jEdit/src/document_dockable.scala
+ Author: Makarius
+
+Dockable window for document build support.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import scala.swing.Button
+import scala.swing.event.ButtonClicked
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
+ GUI_Thread.require {}
+
+
+ /* text area */
+
+ val pretty_text_area = new Pretty_Text_Area(view)
+ set_content(pretty_text_area)
+
+ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
+
+
+ /* document build process */
+
+ private val process_indicator = new Process_Indicator
+
+
+ /* resize */
+
+ private val delay_resize =
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
+ })
+
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
+
+
+ /* controls */
+
+ private val build_button = new Button("<html><b>Build</b></html>") {
+ tooltip = "Build document"
+ reactions += { case ButtonClicked(_) =>
+ pretty_text_area.update(
+ Document.Snapshot.init, Command.Results.empty,
+ List(XML.Text(Date.now().toString))) // FIXME
+ }
+ }
+
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+
+ private val controls =
+ Wrap_Panel(List(process_indicator.component, build_button,
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+
+ add(controls.peer, BorderLayout.NORTH)
+
+ override def focusOnDefaultComponent(): Unit = build_button.requestFocus()
+
+
+ /* main */
+
+ private val main =
+ Session.Consumer[Session.Global_Options](getClass.getName) {
+ case _: Session.Global_Options =>
+ GUI_Thread.later { handle_resize() }
+ }
+
+ override def init(): Unit = {
+ PIDE.session.global_options += main
+ handle_resize()
+ }
+
+ override def exit(): Unit = {
+ PIDE.session.global_options -= main
+ delay_resize.revoke()
+ }
+}
+
--- a/src/Tools/jEdit/src/isabelle.scala Fri Aug 12 12:19:23 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Aug 12 12:50:19 2022 +0200
@@ -108,6 +108,12 @@
case _ => None
}
+ def document_dockable(view: View): Option[Document_Dockable] =
+ wm(view).getDockableWindow("isabelle-document") match {
+ case dockable: Document_Dockable => Some(dockable)
+ case _ => None
+ }
+
def documentation_dockable(view: View): Option[Documentation_Dockable] =
wm(view).getDockableWindow("isabelle-documentation") match {
case dockable: Documentation_Dockable => Some(dockable)