src/Tools/jEdit/src/info_dockable.scala
author wenzelm
Thu, 13 Dec 2012 17:29:23 +0100
changeset 50501 6f41f1646617
parent 50451 2af559170d07
child 50507 9605b0d93d1e
permissions -rw-r--r--
more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
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()
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    29
  private var implicit_results = Command.empty_results
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    30
  private var implicit_info: XML.Body = Nil
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    31
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    32
  private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    33
  {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    34
    Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    35
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    36
    implicit_snapshot = snapshot
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    37
    implicit_results = results
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    38
    implicit_info = info
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    39
  }
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    40
50451
wenzelm
parents: 50207
diff changeset
    41
  private def reset_implicit(): Unit =
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    42
    set_implicit(Document.State.init.snapshot(), Command.empty_results, Nil)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    43
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    44
  def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    45
  {
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    46
    set_implicit(snapshot, results, info)
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    47
    view.getDockableWindowManager.floatDockableWindow("isabelle-info")
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    48
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    49
}
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    50
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    51
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    52
class Info_Dockable(view: View, position: String) extends Dockable(view, position)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    53
{
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    54
  Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    55
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    56
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    57
  /* component state -- owned by Swing thread */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    58
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    59
  private var zoom_factor = 100
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    60
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    61
  private val snapshot = Info_Dockable.implicit_snapshot
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    62
  private val results = Info_Dockable.implicit_results
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    63
  private val info = Info_Dockable.implicit_info
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    64
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    65
  private val window_focus_listener =
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    66
    new WindowFocusListener {
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    67
      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) }
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    68
      def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    69
    }
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    70
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    71
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    72
  /* pretty text area */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    73
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    74
  private val pretty_text_area = new Pretty_Text_Area(view)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    75
  set_content(pretty_text_area)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    76
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    77
  pretty_text_area.update(snapshot, results, info)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    78
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    79
  private def handle_resize()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    80
  {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    81
    Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    82
50206
6626bc5ed053 tuned signature;
wenzelm
parents: 50205
diff changeset
    83
    pretty_text_area.resize(Rendering.font_family(),
6626bc5ed053 tuned signature;
wenzelm
parents: 50205
diff changeset
    84
      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    85
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    86
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    87
50451
wenzelm
parents: 50207
diff changeset
    88
  /* resize */
wenzelm
parents: 50207
diff changeset
    89
wenzelm
parents: 50207
diff changeset
    90
  private val delay_resize =
wenzelm
parents: 50207
diff changeset
    91
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm
parents: 50207
diff changeset
    92
wenzelm
parents: 50207
diff changeset
    93
  addComponentListener(new ComponentAdapter {
wenzelm
parents: 50207
diff changeset
    94
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm
parents: 50207
diff changeset
    95
  })
wenzelm
parents: 50207
diff changeset
    96
wenzelm
parents: 50207
diff changeset
    97
  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
wenzelm
parents: 50207
diff changeset
    98
  zoom.tooltip = "Zoom factor for basic font size"
wenzelm
parents: 50207
diff changeset
    99
wenzelm
parents: 50207
diff changeset
   100
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
wenzelm
parents: 50207
diff changeset
   101
  add(controls.peer, BorderLayout.NORTH)
wenzelm
parents: 50207
diff changeset
   102
wenzelm
parents: 50207
diff changeset
   103
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   104
  /* main actor */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   105
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   106
  private val main_actor = actor {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   107
    loop {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   108
      react {
50117
32755e357a51 update options via protocol;
wenzelm
parents: 49870
diff changeset
   109
        case _: Session.Global_Options =>
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   110
          Swing_Thread.later { handle_resize() }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   111
        case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
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
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   116
  override def init()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   117
  {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   118
    Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   119
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
   120
    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50146
diff changeset
   121
    PIDE.session.global_options += main_actor
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   122
    handle_resize()
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
  override def exit()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   126
  {
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   127
    Swing_Thread.require()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   128
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
   129
    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50146
diff changeset
   130
    PIDE.session.global_options -= main_actor
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   131
    delay_resize.revoke()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   132
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   133
}