# HG changeset patch
# User wenzelm
# Date 1660301419 -7200
# Node ID 91f02f224b8090fe6e0726a965b13e56c1b76227
# Parent  4001a6ceb8029e40b704e5c8a1af8e8e26d83638
basic setup for document build panel;

diff -r 4001a6ceb802 -r 91f02f224b80 etc/build.props
--- 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 \
diff -r 4001a6ceb802 -r 91f02f224b80 src/Tools/jEdit/jedit_main/dockables.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)
 
diff -r 4001a6ceb802 -r 91f02f224b80 src/Tools/jEdit/jedit_main/dockables.xml
--- 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>
diff -r 4001a6ceb802 -r 91f02f224b80 src/Tools/jEdit/jedit_main/plugin.props
--- 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
diff -r 4001a6ceb802 -r 91f02f224b80 src/Tools/jEdit/src/document_dockable.scala
--- /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()
+  }
+}
+
diff -r 4001a6ceb802 -r 91f02f224b80 src/Tools/jEdit/src/isabelle.scala
--- 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)