src/Tools/jEdit/src/info_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56883 38c6b70e5e53
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
wenzelm@49726
     1
/*  Title:      Tools/jEdit/src/info_dockable.scala
wenzelm@49726
     2
    Author:     Makarius
wenzelm@49726
     3
wenzelm@49726
     4
Dockable window with info text.
wenzelm@49726
     5
*/
wenzelm@49726
     6
wenzelm@49726
     7
package isabelle.jedit
wenzelm@49726
     8
wenzelm@49726
     9
wenzelm@49726
    10
import isabelle._
wenzelm@49726
    11
wenzelm@53711
    12
import scala.swing.Button
wenzelm@49726
    13
import scala.swing.event.ButtonClicked
wenzelm@49726
    14
wenzelm@49726
    15
import java.awt.BorderLayout
wenzelm@49870
    16
import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
wenzelm@49726
    17
wenzelm@49726
    18
import org.gjt.sp.jedit.View
wenzelm@49726
    19
wenzelm@49726
    20
wenzelm@49726
    21
object Info_Dockable
wenzelm@49726
    22
{
wenzelm@49726
    23
  /* implicit arguments -- owned by Swing thread */
wenzelm@49726
    24
wenzelm@52972
    25
  private var implicit_snapshot = Document.Snapshot.init
wenzelm@50507
    26
  private var implicit_results = Command.Results.empty
wenzelm@49726
    27
  private var implicit_info: XML.Body = Nil
wenzelm@49726
    28
wenzelm@50501
    29
  private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
wenzelm@49726
    30
  {
wenzelm@56662
    31
    Swing_Thread.require {}
wenzelm@49726
    32
wenzelm@49726
    33
    implicit_snapshot = snapshot
wenzelm@50501
    34
    implicit_results = results
wenzelm@49726
    35
    implicit_info = info
wenzelm@49870
    36
  }
wenzelm@49726
    37
wenzelm@50451
    38
  private def reset_implicit(): Unit =
wenzelm@52972
    39
    set_implicit(Document.Snapshot.init, Command.Results.empty, Nil)
wenzelm@49726
    40
wenzelm@50501
    41
  def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
wenzelm@49870
    42
  {
wenzelm@50501
    43
    set_implicit(snapshot, results, info)
wenzelm@49870
    44
    view.getDockableWindowManager.floatDockableWindow("isabelle-info")
wenzelm@49726
    45
  }
wenzelm@49726
    46
}
wenzelm@49726
    47
wenzelm@49726
    48
wenzelm@49726
    49
class Info_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@49726
    50
{
wenzelm@49726
    51
  /* component state -- owned by Swing thread */
wenzelm@49726
    52
wenzelm@49726
    53
  private var zoom_factor = 100
wenzelm@49726
    54
wenzelm@49870
    55
  private val snapshot = Info_Dockable.implicit_snapshot
wenzelm@50501
    56
  private val results = Info_Dockable.implicit_results
wenzelm@49870
    57
  private val info = Info_Dockable.implicit_info
wenzelm@49870
    58
wenzelm@49870
    59
  private val window_focus_listener =
wenzelm@49870
    60
    new WindowFocusListener {
wenzelm@50501
    61
      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) }
wenzelm@49870
    62
      def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
wenzelm@49870
    63
    }
wenzelm@49870
    64
wenzelm@49726
    65
wenzelm@49726
    66
  /* pretty text area */
wenzelm@49726
    67
wenzelm@49726
    68
  private val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@49726
    69
  set_content(pretty_text_area)
wenzelm@49726
    70
wenzelm@50501
    71
  pretty_text_area.update(snapshot, results, info)
wenzelm@49726
    72
wenzelm@49726
    73
  private def handle_resize()
wenzelm@49726
    74
  {
wenzelm@56662
    75
    Swing_Thread.require {}
wenzelm@49726
    76
wenzelm@55825
    77
    pretty_text_area.resize(
wenzelm@55825
    78
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
wenzelm@49726
    79
  }
wenzelm@49726
    80
wenzelm@49726
    81
wenzelm@50451
    82
  /* resize */
wenzelm@50451
    83
wenzelm@50451
    84
  private val delay_resize =
wenzelm@50451
    85
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@50451
    86
wenzelm@50451
    87
  addComponentListener(new ComponentAdapter {
wenzelm@50451
    88
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@50451
    89
  })
wenzelm@50451
    90
wenzelm@51616
    91
  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
wenzelm@50451
    92
  zoom.tooltip = "Zoom factor for basic font size"
wenzelm@50451
    93
wenzelm@53711
    94
  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
wenzelm@50451
    95
  add(controls.peer, BorderLayout.NORTH)
wenzelm@50451
    96
wenzelm@50451
    97
wenzelm@56715
    98
  /* main */
wenzelm@49726
    99
wenzelm@56715
   100
  private val main =
wenzelm@56715
   101
    Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@56715
   102
      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
wenzelm@49726
   103
    }
wenzelm@49726
   104
wenzelm@49726
   105
  override def init()
wenzelm@49726
   106
  {
wenzelm@53712
   107
    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
wenzelm@56715
   108
    PIDE.session.global_options += main
wenzelm@49726
   109
    handle_resize()
wenzelm@49726
   110
  }
wenzelm@49726
   111
wenzelm@49726
   112
  override def exit()
wenzelm@49726
   113
  {
wenzelm@53712
   114
    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
wenzelm@56715
   115
    PIDE.session.global_options -= main
wenzelm@49726
   116
    delay_resize.revoke()
wenzelm@49726
   117
  }
wenzelm@49726
   118
}