src/Tools/jEdit/src/info_dockable.scala
author wenzelm
Fri, 25 Apr 2014 12:51:08 +0200
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;
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
53711
8ce7795256e1 improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents: 53177
diff changeset
    12
import scala.swing.Button
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    13
import scala.swing.event.ButtonClicked
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    14
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    15
import java.awt.BorderLayout
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    16
import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    17
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    18
import org.gjt.sp.jedit.View
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    19
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    20
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    21
object Info_Dockable
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    22
{
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    23
  /* implicit arguments -- owned by Swing thread */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    24
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52907
diff changeset
    25
  private var implicit_snapshot = Document.Snapshot.init
50507
9605b0d93d1e more formal class Command.Results;
wenzelm
parents: 50501
diff changeset
    26
  private var implicit_results = Command.Results.empty
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    27
  private var implicit_info: XML.Body = Nil
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    28
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    29
  private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    30
  {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 55825
diff changeset
    31
    Swing_Thread.require {}
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    32
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    33
    implicit_snapshot = snapshot
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    34
    implicit_results = results
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    35
    implicit_info = info
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    36
  }
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    37
50451
wenzelm
parents: 50207
diff changeset
    38
  private def reset_implicit(): Unit =
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52907
diff changeset
    39
    set_implicit(Document.Snapshot.init, Command.Results.empty, Nil)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    40
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    41
  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
    42
  {
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    43
    set_implicit(snapshot, results, info)
49870
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
  /* component state -- owned by Swing thread */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    52
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    53
  private var zoom_factor = 100
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    54
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    55
  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
    56
  private val results = Info_Dockable.implicit_results
49870
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    57
  private val info = Info_Dockable.implicit_info
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    58
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    59
  private val window_focus_listener =
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    60
    new WindowFocusListener {
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    61
      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
    62
      def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    63
    }
2b82358694e6 retain info dockable state via educated guess on window focus;
wenzelm
parents: 49726
diff changeset
    64
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    65
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    66
  /* pretty text area */
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    67
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    68
  private val pretty_text_area = new Pretty_Text_Area(view)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    69
  set_content(pretty_text_area)
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    70
50501
6f41f1646617 more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents: 50451
diff changeset
    71
  pretty_text_area.update(snapshot, results, info)
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    72
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    73
  private def handle_resize()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    74
  {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 55825
diff changeset
    75
    Swing_Thread.require {}
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    76
55825
694833e3e4a0 tuned signature -- separate module Font_Info;
wenzelm
parents: 55618
diff changeset
    77
    pretty_text_area.resize(
694833e3e4a0 tuned signature -- separate module Font_Info;
wenzelm
parents: 55618
diff changeset
    78
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    79
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    80
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    81
50451
wenzelm
parents: 50207
diff changeset
    82
  /* resize */
wenzelm
parents: 50207
diff changeset
    83
wenzelm
parents: 50207
diff changeset
    84
  private val delay_resize =
wenzelm
parents: 50207
diff changeset
    85
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm
parents: 50207
diff changeset
    86
wenzelm
parents: 50207
diff changeset
    87
  addComponentListener(new ComponentAdapter {
wenzelm
parents: 50207
diff changeset
    88
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm
parents: 50207
diff changeset
    89
  })
wenzelm
parents: 50207
diff changeset
    90
51616
949e2cf02a3d tuned signature -- concentrate GUI tools;
wenzelm
parents: 50507
diff changeset
    91
  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
50451
wenzelm
parents: 50207
diff changeset
    92
  zoom.tooltip = "Zoom factor for basic font size"
wenzelm
parents: 50207
diff changeset
    93
53711
8ce7795256e1 improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents: 53177
diff changeset
    94
  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
50451
wenzelm
parents: 50207
diff changeset
    95
  add(controls.peer, BorderLayout.NORTH)
wenzelm
parents: 50207
diff changeset
    96
wenzelm
parents: 50207
diff changeset
    97
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    98
  /* main */
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
    99
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   100
  private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   101
    Session.Consumer[Session.Global_Options](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   102
      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
49726
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 init()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   106
  {
53712
ea51046be71b tuned signature;
wenzelm
parents: 53711
diff changeset
   107
    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   108
    PIDE.session.global_options += main
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   109
    handle_resize()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   110
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   111
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   112
  override def exit()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   113
  {
53712
ea51046be71b tuned signature;
wenzelm
parents: 53711
diff changeset
   114
    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   115
    PIDE.session.global_options -= main
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   116
    delay_resize.revoke()
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   117
  }
2074197dc274 detach tooltip as dockable window;
wenzelm
parents:
diff changeset
   118
}