src/Tools/jEdit/src/info_dockable.scala
author wenzelm
Tue, 16 Oct 2012 22:13:46 +0200
changeset 49870 2b82358694e6
parent 49726 2074197dc274
child 50117 32755e357a51
permissions -rw-r--r--
retain info dockable state via educated guess on window focus;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/info_dockable.scala
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     3
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     4
Dockable window with info text.
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     5
*/
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     6
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     8
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
     9
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    10
import isabelle._
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    11
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    12
import scala.actors.Actor._
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    13
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    14
import scala.swing.{FlowPanel, Button, CheckBox}
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    15
import scala.swing.event.ButtonClicked
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    16
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    17
import java.lang.System
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    18
import java.awt.BorderLayout
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    19
import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    20
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    21
import org.gjt.sp.jedit.View
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    22
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    23
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    24
object Info_Dockable
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    25
{
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    26
  /* implicit arguments -- owned by Swing thread */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    27
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    28
  private var implicit_snapshot = Document.State.init.snapshot()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    29
  private var implicit_info: XML.Body = Nil
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    30
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    31
  private def set_implicit(snapshot: Document.Snapshot, info: XML.Body)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    32
  {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    33
    Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    34
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    35
    implicit_snapshot = snapshot
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    36
    implicit_info = info
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    37
  }
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    38
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    39
  private def reset_implicit(): Unit = set_implicit(Document.State.init.snapshot(), Nil)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    40
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    41
  def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    42
  {
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    43
    set_implicit(snapshot, info)
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    44
    view.getDockableWindowManager.floatDockableWindow("isabelle-info")
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    45
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    46
}
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    47
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    48
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    49
class Info_Dockable(view: View, position: String) extends Dockable(view, position)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    50
{
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    51
  Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    52
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    53
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    54
  /* component state -- owned by Swing thread */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    55
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    56
  private var zoom_factor = 100
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    57
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    58
  private val snapshot = Info_Dockable.implicit_snapshot
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    59
  private val info = Info_Dockable.implicit_info
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    60
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    61
  private val window_focus_listener =
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    62
    new WindowFocusListener {
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    63
      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, info) }
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    64
      def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    65
    }
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    66
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    67
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    68
  /* pretty text area */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    69
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    70
  private val pretty_text_area = new Pretty_Text_Area(view)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    71
  set_content(pretty_text_area)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    72
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    73
  pretty_text_area.update(snapshot, info)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    74
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    75
  private def handle_resize()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    76
  {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    77
    Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    78
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    79
    pretty_text_area.resize(Isabelle.font_family(),
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    80
      scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100))
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    81
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    82
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    83
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    84
  /* main actor */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    85
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    86
  private val main_actor = actor {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    87
    loop {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    88
      react {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    89
        case Session.Global_Options =>
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    90
          Swing_Thread.later { handle_resize() }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    91
        case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    92
      }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    93
    }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    94
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    95
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    96
  override def init()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    97
  {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    98
    Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    99
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
   100
    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   101
    Isabelle.session.global_options += main_actor
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   102
    handle_resize()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   103
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   104
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   105
  override def exit()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   106
  {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   107
    Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   108
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
   109
    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   110
    Isabelle.session.global_options -= main_actor
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   111
    delay_resize.revoke()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   112
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   113
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   114
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   115
  /* resize */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   116
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   117
  private val delay_resize =
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   118
    Swing_Thread.delay_first(
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   119
      Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   120
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   121
  addComponentListener(new ComponentAdapter {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   122
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   123
  })
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   124
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   125
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   126
  /* controls */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   127
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   128
  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   129
  zoom.tooltip = "Zoom factor for basic font size"
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   130
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   131
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   132
  add(controls.peer, BorderLayout.NORTH)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   133
}