# HG changeset patch
# User wenzelm
# Date 1349618731 -7200
# Node ID 2074197dc274710792e731aebbfedd07df54f00b
# Parent f8eeff667076d000424fa549397283ad277bc02e
detach tooltip as dockable window;
diff -r f8eeff667076 -r 2074197dc274 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Oct 07 15:05:11 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Oct 07 16:05:31 2012 +0200
@@ -14,6 +14,7 @@
"src/graphview_dockable.scala"
"src/html_panel.scala"
"src/hyperlink.scala"
+ "src/info_dockable.scala"
"src/isabelle_encoding.scala"
"src/isabelle_logic.scala"
"src/isabelle_options.scala"
diff -r f8eeff667076 -r 2074197dc274 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Sun Oct 07 15:05:11 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Sun Oct 07 16:05:31 2012 +0200
@@ -52,6 +52,7 @@
#dockables
isabelle-session.title=Prover Session
isabelle-output.title=Output
+isabelle-info.title=Info
isabelle-graphview.title=Graphview
isabelle-raw-output.title=Raw Output
isabelle-protocol.title=Protocol
diff -r f8eeff667076 -r 2074197dc274 src/Tools/jEdit/src/dockables.xml
--- a/src/Tools/jEdit/src/dockables.xml Sun Oct 07 15:05:11 2012 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Sun Oct 07 16:05:31 2012 +0200
@@ -14,6 +14,9 @@
new isabelle.jedit.Output_Dockable(view, position);
+
+ new isabelle.jedit.Info_Dockable(view, position);
+
new isabelle.jedit.Graphview_Dockable(view, position);
diff -r f8eeff667076 -r 2074197dc274 src/Tools/jEdit/src/info_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/info_dockable.scala Sun Oct 07 16:05:31 2012 +0200
@@ -0,0 +1,119 @@
+/* Title: Tools/jEdit/src/info_dockable.scala
+ Author: Makarius
+
+Dockable window with info text.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+
+import scala.swing.{FlowPanel, Button, CheckBox}
+import scala.swing.event.ButtonClicked
+
+import java.lang.System
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import org.gjt.sp.jedit.View
+
+
+object Info_Dockable
+{
+ /* implicit arguments -- owned by Swing thread */
+
+ private var implicit_snapshot = Document.State.init.snapshot()
+ private var implicit_info: XML.Body = Nil
+
+ def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
+ {
+ Swing_Thread.require()
+
+ implicit_snapshot = snapshot
+ implicit_info = info
+
+ view.getDockableWindowManager.floatDockableWindow("isabelle-info")
+
+ implicit_snapshot = Document.State.init.snapshot()
+ implicit_info = Nil
+ }
+}
+
+
+class Info_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ Swing_Thread.require()
+
+
+ /* component state -- owned by Swing thread */
+
+ private var zoom_factor = 100
+
+
+ /* pretty text area */
+
+ private val pretty_text_area = new Pretty_Text_Area(view)
+ set_content(pretty_text_area)
+
+ pretty_text_area.update(Info_Dockable.implicit_snapshot, Info_Dockable.implicit_info)
+
+ private def handle_resize()
+ {
+ Swing_Thread.require()
+
+ pretty_text_area.resize(Isabelle.font_family(),
+ scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100))
+ }
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case Session.Global_Options =>
+ Swing_Thread.later { handle_resize() }
+ case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Swing_Thread.require()
+
+ Isabelle.session.global_options += main_actor
+ handle_resize()
+ }
+
+ override def exit()
+ {
+ Swing_Thread.require()
+
+ Isabelle.session.global_options -= main_actor
+ delay_resize.revoke()
+ }
+
+
+ /* resize */
+
+ private val delay_resize =
+ Swing_Thread.delay_first(
+ Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+
+ /* controls */
+
+ private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
+ zoom.tooltip = "Zoom factor for basic font size"
+
+ private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
+ add(controls.peer, BorderLayout.NORTH)
+}
diff -r f8eeff667076 -r 2074197dc274 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Sun Oct 07 15:05:11 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Sun Oct 07 16:05:31 2012 +0200
@@ -56,6 +56,7 @@
legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
error_pri -> load_icon("16x16/status/dialog-error.png"))
+ val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
diff -r f8eeff667076 -r 2074197dc274 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala Sun Oct 07 15:05:11 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Sun Oct 07 16:05:31 2012 +0200
@@ -37,7 +37,7 @@
private var current_tracing = 0
- /* pretty text panel */
+ /* pretty text area */
private val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
diff -r f8eeff667076 -r 2074197dc274 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sun Oct 07 15:05:11 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sun Oct 07 16:05:31 2012 +0200
@@ -76,6 +76,15 @@
/* controls */
+ private val detach = new Label {
+ icon = Isabelle_Rendering.tooltip_detach_icon
+ tooltip = "Detach tooltip window"
+ listenTo(mouse.clicks)
+ reactions += {
+ case _: MouseClicked => Info_Dockable(view, rendering.snapshot, body); window.dispose()
+ }
+ }
+
private val close = new Label {
icon = Isabelle_Rendering.tooltip_close_icon
tooltip = "Close tooltip window"
@@ -83,7 +92,7 @@
reactions += { case _: MouseClicked => window.dispose() }
}
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(close)
+ private val controls = new FlowPanel(FlowPanel.Alignment.Right)(detach, close)
window.add(controls.peer, BorderLayout.NORTH)