tuned signature;
authorwenzelm
Sat Aug 24 15:30:50 2013 +0200 (2013-08-24)
changeset 53179336cd976698c
parent 53178 0a3a5f606b2a
child 53180 04590977dc3c
tuned signature;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Aug 24 14:58:36 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Aug 24 15:30:50 2013 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5    val rich_text_area =
     1.6      new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
     1.7 -      caret_visible = true, hovering = false)
     1.8 +      caret_visible = true, enable_hovering = false)
     1.9  
    1.10  
    1.11    /* perspective */
     2.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Aug 24 14:58:36 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Aug 24 15:30:50 2013 +0200
     2.3 @@ -72,7 +72,7 @@
     2.4  
     2.5    private val rich_text_area =
     2.6      new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
     2.7 -      caret_visible = false, hovering = true)
     2.8 +      caret_visible = false, enable_hovering = true)
     2.9  
    2.10    def get_background(): Option[Color] = None
    2.11  
     3.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Aug 24 14:58:36 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Aug 24 15:30:50 2013 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4    get_rendering: () => Rendering,
     3.5    close_action: () => Unit,
     3.6    caret_visible: Boolean,
     3.7 -  hovering: Boolean)
     3.8 +  enable_hovering: Boolean)
     3.9  {
    3.10    private val buffer = text_area.getBuffer
    3.11  
    3.12 @@ -175,7 +175,7 @@
    3.13        robust_body(()) {
    3.14          control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
    3.15  
    3.16 -        if ((control || hovering) && !buffer.isLoading) {
    3.17 +        if ((control || enable_hovering) && !buffer.isLoading) {
    3.18            JEdit_Lib.buffer_lock(buffer) {
    3.19              JEdit_Lib.pixel_range(text_area, e.getX, e.getY) match {
    3.20                case None => active_reset()