merged
authorwenzelm
Sat Mar 29 21:26:11 2014 +0100 (2014-03-29 ago)
changeset 56324f9de5e5b56e6
parent 56320 e84c12d4a886
parent 56323 e925118b1875
child 56325 ffbfc92e6508
merged
     1.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Mar 28 18:21:07 2014 -0700
     1.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 29 21:26:11 2014 +0100
     1.3 @@ -166,7 +166,8 @@
     1.4        {
     1.5          evt.getKeyCode match {
     1.6            case KeyEvent.VK_C
     1.7 -          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
     1.8 +          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
     1.9 +              text_area.getSelectionCount != 0 =>
    1.10              Registers.copy(text_area, '$')
    1.11              evt.consume
    1.12  
     2.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 28 18:21:07 2014 -0700
     2.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 29 21:26:11 2014 +0100
     2.3 @@ -10,10 +10,11 @@
     2.4  
     2.5  import isabelle._
     2.6  
     2.7 -import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor}
     2.8 +import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo}
     2.9  import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
    2.10    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    2.11  import java.awt.font.TextAttribute
    2.12 +import javax.swing.SwingUtilities
    2.13  import java.text.AttributedString
    2.14  import java.util.ArrayList
    2.15  
    2.16 @@ -180,7 +181,23 @@
    2.17      }
    2.18    }
    2.19  
    2.20 +  private def mouse_inside_painter(): Boolean =
    2.21 +    MouseInfo.getPointerInfo match {
    2.22 +      case null => false
    2.23 +      case info =>
    2.24 +        val point = info.getLocation
    2.25 +        val painter = text_area.getPainter
    2.26 +        SwingUtilities.convertPointFromScreen(point, painter)
    2.27 +        painter.contains(point)
    2.28 +    }
    2.29 +
    2.30    private val mouse_motion_listener = new MouseMotionAdapter {
    2.31 +    override def mouseDragged(evt: MouseEvent) {
    2.32 +      robust_body(()) {
    2.33 +        PIDE.dismissed_popups(view)
    2.34 +      }
    2.35 +    }
    2.36 +
    2.37      override def mouseMoved(evt: MouseEvent) {
    2.38        robust_body(()) {
    2.39          val x = evt.getX
    2.40 @@ -207,23 +224,25 @@
    2.41          if (evt.getSource == text_area.getPainter) {
    2.42            Pretty_Tooltip.invoke(() =>
    2.43              robust_body(()) {
    2.44 -              val rendering = get_rendering()
    2.45 -              val snapshot = rendering.snapshot
    2.46 -              if (!snapshot.is_outdated) {
    2.47 -                JEdit_Lib.pixel_range(text_area, x, y) match {
    2.48 -                  case None =>
    2.49 -                  case Some(range) =>
    2.50 -                    val result =
    2.51 -                      if (control) rendering.tooltip(range)
    2.52 -                      else rendering.tooltip_message(range)
    2.53 -                    result match {
    2.54 -                      case None =>
    2.55 -                      case Some(tip) =>
    2.56 -                        val painter = text_area.getPainter
    2.57 -                        val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
    2.58 -                        val results = rendering.command_results(range)
    2.59 -                        Pretty_Tooltip(view, painter, loc, rendering, results, tip)
    2.60 -                    }
    2.61 +              if (mouse_inside_painter()) {
    2.62 +                val rendering = get_rendering()
    2.63 +                val snapshot = rendering.snapshot
    2.64 +                if (!snapshot.is_outdated) {
    2.65 +                  JEdit_Lib.pixel_range(text_area, x, y) match {
    2.66 +                    case None =>
    2.67 +                    case Some(range) =>
    2.68 +                      val result =
    2.69 +                        if (control) rendering.tooltip(range)
    2.70 +                        else rendering.tooltip_message(range)
    2.71 +                      result match {
    2.72 +                        case None =>
    2.73 +                        case Some(tip) =>
    2.74 +                          val painter = text_area.getPainter
    2.75 +                          val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
    2.76 +                          val results = rendering.command_results(range)
    2.77 +                          Pretty_Tooltip(view, painter, loc, rendering, results, tip)
    2.78 +                      }
    2.79 +                  }
    2.80                  }
    2.81                }
    2.82            })