author | wenzelm |
Mon, 25 Mar 2019 17:21:26 +0100 | |
changeset 69981 | 3dced198b9ec |
parent 66591 | 6efa351190d0 |
child 71704 | b9a5eb0f3b43 |
permissions | -rw-r--r-- |
49726 | 1 |
/* Title: Tools/jEdit/src/info_dockable.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Dockable window with info text. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
66206
diff
changeset
|
11 |
import isabelle.jedit_base.Dockable |
49726 | 12 |
|
13 |
import java.awt.BorderLayout |
|
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
14 |
import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent} |
49726 | 15 |
|
16 |
import org.gjt.sp.jedit.View |
|
17 |
||
18 |
||
19 |
object Info_Dockable |
|
20 |
{ |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
21 |
/* implicit arguments -- owned by GUI thread */ |
49726 | 22 |
|
52972 | 23 |
private var implicit_snapshot = Document.Snapshot.init |
50507 | 24 |
private var implicit_results = Command.Results.empty |
49726 | 25 |
private var implicit_info: XML.Body = Nil |
26 |
||
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50451
diff
changeset
|
27 |
private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body) |
49726 | 28 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
29 |
GUI_Thread.require {} |
49726 | 30 |
|
31 |
implicit_snapshot = snapshot |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50451
diff
changeset
|
32 |
implicit_results = results |
49726 | 33 |
implicit_info = info |
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
34 |
} |
49726 | 35 |
|
50451 | 36 |
private def reset_implicit(): Unit = |
52972 | 37 |
set_implicit(Document.Snapshot.init, Command.Results.empty, Nil) |
49726 | 38 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50451
diff
changeset
|
39 |
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
|
40 |
{ |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50451
diff
changeset
|
41 |
set_implicit(snapshot, results, info) |
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
42 |
view.getDockableWindowManager.floatDockableWindow("isabelle-info") |
49726 | 43 |
} |
44 |
} |
|
45 |
||
46 |
||
47 |
class Info_Dockable(view: View, position: String) extends Dockable(view, position) |
|
48 |
{ |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
49 |
/* component state -- owned by GUI thread */ |
49726 | 50 |
|
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
51 |
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
|
52 |
private val results = Info_Dockable.implicit_results |
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
53 |
private val info = Info_Dockable.implicit_info |
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
54 |
|
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
55 |
private val window_focus_listener = |
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
56 |
new WindowFocusListener { |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50451
diff
changeset
|
57 |
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
|
58 |
def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() } |
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
59 |
} |
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
60 |
|
49726 | 61 |
|
62 |
/* pretty text area */ |
|
63 |
||
64 |
private val pretty_text_area = new Pretty_Text_Area(view) |
|
65 |
set_content(pretty_text_area) |
|
66 |
||
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50451
diff
changeset
|
67 |
pretty_text_area.update(snapshot, results, info) |
49726 | 68 |
|
57044 | 69 |
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } |
70 |
||
49726 | 71 |
private def handle_resize() |
72 |
{ |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
73 |
GUI_Thread.require {} |
49726 | 74 |
|
55825 | 75 |
pretty_text_area.resize( |
57044 | 76 |
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) |
49726 | 77 |
} |
78 |
||
79 |
||
50451 | 80 |
/* resize */ |
81 |
||
82 |
private val delay_resize = |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
83 |
GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
50451 | 84 |
|
85 |
addComponentListener(new ComponentAdapter { |
|
86 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
|
60750 | 87 |
override def componentShown(e: ComponentEvent) { delay_resize.invoke() } |
50451 | 88 |
}) |
89 |
||
66205 | 90 |
private val controls = |
66206 | 91 |
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |
66205 | 92 |
|
50451 | 93 |
add(controls.peer, BorderLayout.NORTH) |
94 |
||
95 |
||
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
96 |
/* main */ |
49726 | 97 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
98 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
99 |
Session.Consumer[Session.Global_Options](getClass.getName) { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
100 |
case _: Session.Global_Options => GUI_Thread.later { handle_resize() } |
49726 | 101 |
} |
102 |
||
103 |
override def init() |
|
104 |
{ |
|
53712 | 105 |
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
|
106 |
PIDE.session.global_options += main |
49726 | 107 |
handle_resize() |
108 |
} |
|
109 |
||
110 |
override def exit() |
|
111 |
{ |
|
53712 | 112 |
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
|
113 |
PIDE.session.global_options -= main |
49726 | 114 |
delay_resize.revoke() |
115 |
} |
|
116 |
} |