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