more general Document_Model.point_range;
authorwenzelm
Fri Sep 14 17:37:19 2012 +0200 (2012-09-14)
changeset 4935734ac36642a31
parent 49356 6e0c0ffb6ec7
child 49358 0fa351b1bd14
more general Document_Model.point_range;
more general Document_View.Active_Area;
eliminated dead popup material;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 14 13:52:16 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 14 17:37:19 2012 +0200
     1.3 @@ -92,6 +92,24 @@
     1.4    }
     1.5  
     1.6  
     1.7 +
     1.8 +  /* point range */
     1.9 +
    1.10 +  def point_range(offset: Text.Offset): Text.Range =
    1.11 +    Isabelle.buffer_lock(buffer) {
    1.12 +      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
    1.13 +      try {
    1.14 +        val c = text(offset)
    1.15 +        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
    1.16 +          Text.Range(offset, offset + 2)
    1.17 +        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
    1.18 +          Text.Range(offset - 1, offset + 1)
    1.19 +        else Text.Range(offset, offset + 1)
    1.20 +      }
    1.21 +      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
    1.22 +    }
    1.23 +
    1.24 +
    1.25    /* pending text edits */
    1.26  
    1.27    private object pending_edits  // owned by Swing thread
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Sep 14 13:52:16 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Sep 14 17:37:19 2012 +0200
     2.3 @@ -19,7 +19,6 @@
     2.4  import java.awt.{Color, Graphics2D, Point}
     2.5  import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
     2.6    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
     2.7 -import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
     2.8  import javax.swing.event.{CaretListener, CaretEvent}
     2.9  
    2.10  import org.gjt.sp.util.Log
    2.11 @@ -143,77 +142,56 @@
    2.12    }
    2.13  
    2.14  
    2.15 -  /* HTML popups */
    2.16 +  /* active areas within the text */
    2.17  
    2.18 -  private var html_popup: Option[Popup] = None
    2.19 +  private class Active_Area[A](
    2.20 +    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
    2.21 +  {
    2.22 +    private var the_info: Option[Text.Info[A]] = None
    2.23  
    2.24 -  private def exit_popup() { html_popup.map(_.hide) }
    2.25 +    def info: Option[Text.Info[A]] = the_info
    2.26  
    2.27 -  private val html_panel =
    2.28 -    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    2.29 -  html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
    2.30 +    def update(new_info: Option[Text.Info[A]])
    2.31 +    {
    2.32 +      val old_info = the_info
    2.33 +      if (new_info != old_info) {
    2.34 +        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
    2.35 +          invalidate_range(range)
    2.36 +        the_info = new_info
    2.37 +      }
    2.38 +    }
    2.39  
    2.40 -  private def html_panel_resize()
    2.41 -  {
    2.42 -    Swing_Thread.now {
    2.43 -      html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    2.44 -    }
    2.45 +    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
    2.46 +    { update(rendering(r)(range)) }
    2.47 +
    2.48 +    def reset { update(None) }
    2.49    }
    2.50  
    2.51 -  private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
    2.52 -  {
    2.53 -    exit_popup()
    2.54 -/* FIXME broken
    2.55 -    val offset = text_area.xyToOffset(x, y)
    2.56 -    val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
    2.57 -
    2.58 -    // FIXME snapshot.cumulate
    2.59 -    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.popup) match {
    2.60 -      case Text.Info(_, Some(msg)) #:: _ =>
    2.61 -        val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
    2.62 -        html_panel.render_sync(List(msg))
    2.63 -        Thread.sleep(10)  // FIXME !?
    2.64 -        popup.show
    2.65 -        html_popup = Some(popup)
    2.66 -      case _ =>
    2.67 -    }
    2.68 -*/
    2.69 -  }
    2.70 -
    2.71 -
    2.72 -  /* subexpression highlighting and hyperlinks */
    2.73 -
    2.74 -  @volatile private var _highlight_range: Option[Text.Info[Color]] = None
    2.75 -  def highlight_range(): Option[Text.Info[Color]] = _highlight_range
    2.76 -
    2.77 -  @volatile private var _hyperlink_range: Option[Text.Info[Hyperlink]] = None
    2.78 -  def hyperlink_range(): Option[Text.Info[Hyperlink]] = _hyperlink_range
    2.79 +  // owned by Swing thread
    2.80  
    2.81    private var control: Boolean = false
    2.82  
    2.83 -  private def exit_control()
    2.84 -  {
    2.85 -    exit_popup()
    2.86 -    _highlight_range = None
    2.87 -    _hyperlink_range = None
    2.88 -  }
    2.89 +  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.subexp _)
    2.90 +  def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
    2.91 +
    2.92 +  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
    2.93 +  def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info
    2.94 +
    2.95 +  private val active_areas = List(highlight_area, hyperlink_area)
    2.96 +  private def active_reset(): Unit = active_areas.foreach(_.reset)
    2.97  
    2.98    private val focus_listener = new FocusAdapter {
    2.99 -    override def focusLost(e: FocusEvent) {
   2.100 -      // FIXME exit_control !?
   2.101 -      _highlight_range = None
   2.102 -      _hyperlink_range = None
   2.103 -    }
   2.104 +    override def focusLost(e: FocusEvent) { active_reset() }
   2.105    }
   2.106  
   2.107    private val window_listener = new WindowAdapter {
   2.108 -    override def windowIconified(e: WindowEvent) { exit_control() }
   2.109 -    override def windowDeactivated(e: WindowEvent) { exit_control() }
   2.110 +    override def windowIconified(e: WindowEvent) { active_reset() }
   2.111 +    override def windowDeactivated(e: WindowEvent) { active_reset() }
   2.112    }
   2.113  
   2.114    private val mouse_listener = new MouseAdapter {
   2.115      override def mouseClicked(e: MouseEvent) {
   2.116 -      hyperlink_range match {
   2.117 +      hyperlink_area.info match {
   2.118          case Some(Text.Info(range, link)) => link.follow(text_area.getView)
   2.119          case None =>
   2.120        }
   2.121 @@ -222,37 +200,15 @@
   2.122  
   2.123    private val mouse_motion_listener = new MouseMotionAdapter {
   2.124      override def mouseMoved(e: MouseEvent) {
   2.125 -      Swing_Thread.assert()
   2.126 -
   2.127        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
   2.128 -      val x = e.getX()
   2.129 -      val y = e.getY()
   2.130 -
   2.131 -      if (!model.buffer.isLoaded) exit_control()
   2.132 -      else
   2.133 +      if (control && model.buffer.isLoaded) {
   2.134          Isabelle.buffer_lock(model.buffer) {
   2.135 -          val snapshot = model.snapshot()
   2.136 -          val rendering = Isabelle_Rendering(snapshot, Isabelle.options.value)
   2.137 -
   2.138 -          if (control) init_popup(snapshot, x, y)
   2.139 -
   2.140 -          def update_range[A](
   2.141 -            rendering: Text.Range => Option[Text.Info[A]],
   2.142 -            info: Option[Text.Info[A]]): Option[Text.Info[A]] =
   2.143 -          {
   2.144 -            for (Text.Info(range, _) <- info) invalidate_range(range)
   2.145 -            val new_info =
   2.146 -              if (control) {
   2.147 -                val offset = text_area.xyToOffset(x, y)
   2.148 -                rendering(Text.Range(offset, offset + 1))
   2.149 -              }
   2.150 -              else None
   2.151 -            for (Text.Info(range, _) <- info) invalidate_range(range)
   2.152 -            new_info
   2.153 -          }
   2.154 -          _highlight_range = update_range(rendering.subexp, _highlight_range)
   2.155 -          _hyperlink_range = update_range(rendering.hyperlink, _hyperlink_range)
   2.156 +          val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
   2.157 +          val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY()))
   2.158 +          active_areas.foreach(_.update_rendering(rendering, mouse_range))
   2.159          }
   2.160 +      }
   2.161 +      else active_reset()
   2.162      }
   2.163    }
   2.164  
   2.165 @@ -316,24 +272,6 @@
   2.166    }
   2.167  
   2.168  
   2.169 -  /* caret range */
   2.170 -
   2.171 -  def caret_range(): Text.Range =
   2.172 -    Isabelle.buffer_lock(model.buffer) {
   2.173 -      def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
   2.174 -      val caret = text_area.getCaretPosition
   2.175 -      try {
   2.176 -        val c = text(caret)
   2.177 -        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
   2.178 -          Text.Range(caret, caret + 2)
   2.179 -        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
   2.180 -          Text.Range(caret - 1, caret + 1)
   2.181 -        else Text.Range(caret, caret + 1)
   2.182 -      }
   2.183 -      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
   2.184 -    }
   2.185 -
   2.186 -
   2.187    /* caret handling */
   2.188  
   2.189    def selected_command(): Option[Command] =
   2.190 @@ -408,8 +346,6 @@
   2.191              }
   2.192            }
   2.193  
   2.194 -        case Session.Global_Settings => html_panel_resize()
   2.195 -
   2.196          case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
   2.197        }
   2.198      }
   2.199 @@ -452,6 +388,5 @@
   2.200      text_area_painter.deactivate()
   2.201      painter.removeExtension(tooltip_painter)
   2.202      painter.removeExtension(update_perspective)
   2.203 -    exit_popup()
   2.204    }
   2.205  }
     3.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 14 13:52:16 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 14 17:37:19 2012 +0200
     3.3 @@ -185,7 +185,7 @@
     3.4            else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
     3.5  
     3.6          val caret_range =
     3.7 -          if (text_area.isCaretVisible) doc_view.caret_range()
     3.8 +          if (text_area.isCaretVisible) model.point_range(text_area.getCaretPosition)
     3.9            else Text.Range(-1)
    3.10  
    3.11          val markup =
    3.12 @@ -296,9 +296,9 @@
    3.13                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    3.14              }
    3.15  
    3.16 -            // highlighted range -- potentially from other snapshot
    3.17 +            // highlight range -- potentially from other snapshot
    3.18              for {
    3.19 -              info <- doc_view.highlight_range()
    3.20 +              info <- doc_view.highlight_info()
    3.21                Text.Info(range, color) <- info.try_restrict(line_range)
    3.22                r <- gfx_range(range)
    3.23              } {
    3.24 @@ -308,7 +308,7 @@
    3.25  
    3.26              // hyperlink range -- potentially from other snapshot
    3.27              for {
    3.28 -              info <- doc_view.hyperlink_range()
    3.29 +              info <- doc_view.hyperlink_info()
    3.30                Text.Info(range, _) <- info.try_restrict(line_range)
    3.31                r <- gfx_range(range)
    3.32              } {