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