# HG changeset patch
# User wenzelm
# Date 1285710465 -7200
# Node ID 62b91eb2d39aea89837b43dcf09f7acd7b74d505
# Parent  0294948ba9622209e1812d38991a54f9406fb5d6
CONTROL-mouse management: handle windowIconified;
html_panel: tuned border;

diff -r 0294948ba962 -r 62b91eb2d39a src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 28 23:02:05 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 28 23:47:45 2010 +0200
@@ -13,8 +13,9 @@
 import scala.actors.Actor._
 
 import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
-import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
-import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities}
+import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
+  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
+import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
 import javax.swing.event.{CaretListener, CaretEvent}
 
 import org.gjt.sp.jedit.{jEdit, OperatingSystem}
@@ -30,7 +31,7 @@
 
   private val key = new Object
 
-  def init(model: Document_Model, text_area: TextArea): Document_View =
+  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
   {
     Swing_Thread.require()
     val doc_view = new Document_View(model, text_area)
@@ -39,7 +40,7 @@
     doc_view
   }
 
-  def apply(text_area: TextArea): Option[Document_View] =
+  def apply(text_area: JEditTextArea): Option[Document_View] =
   {
     Swing_Thread.require()
     text_area.getClientProperty(key) match {
@@ -48,7 +49,7 @@
     }
   }
 
-  def exit(text_area: TextArea)
+  def exit(text_area: JEditTextArea)
   {
     Swing_Thread.require()
     apply(text_area) match {
@@ -61,7 +62,7 @@
 }
 
 
-class Document_View(val model: Document_Model, text_area: TextArea)
+class Document_View(val model: Document_Model, text_area: JEditTextArea)
 {
   private val session = model.session
 
@@ -116,8 +117,8 @@
   private def exit_popup() { html_popup.map(_.hide) }
 
   private val html_panel =
-    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size())) {
-    }
+    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+  html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
 
   private def html_panel_resize()
   {
@@ -171,6 +172,10 @@
     override def focusLost(e: FocusEvent) { exit_control() }
   }
 
+  private val window_listener = new WindowAdapter {
+    override def windowIconified(e: WindowEvent) { exit_control() }
+  }
+
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseMoved(e: MouseEvent) {
       val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
@@ -460,6 +465,7 @@
       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
     text_area.getGutter.addExtension(gutter_extension)
     text_area.addFocusListener(focus_listener)
+    text_area.getView.addWindowListener(window_listener)
     text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
     text_area.addCaretListener(caret_listener)
     text_area.addLeftOfScrollBar(overview)
@@ -472,6 +478,7 @@
     session.commands_changed -= main_actor
     session.global_settings -= main_actor
     text_area.removeFocusListener(focus_listener)
+    text_area.getView.removeWindowListener(window_listener)
     text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
     text_area.removeCaretListener(caret_listener)
     text_area.removeLeftOfScrollBar(overview)
diff -r 0294948ba962 -r 62b91eb2d39a src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Sep 28 23:02:05 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Sep 28 23:47:45 2010 +0200
@@ -255,8 +255,8 @@
 
   private case class Init_Model(buffer: Buffer)
   private case class Exit_Model(buffer: Buffer)
-  private case class Init_View(buffer: Buffer, text_area: TextArea)
-  private case class Exit_View(buffer: Buffer, text_area: TextArea)
+  private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
+  private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
 
   private val session_manager = actor {
     var ready = false