author | wenzelm |
Sat, 24 Aug 2013 13:32:51 +0200 | |
changeset 53177 | dcac8d837b9c |
parent 52972 | 8fd8e1c14988 |
child 53711 | 8ce7795256e1 |
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 scala.actors.Actor._ |
|
13 |
||
52907 | 14 |
import scala.swing.{FlowPanel, Button} |
49726 | 15 |
import scala.swing.event.ButtonClicked |
16 |
||
17 |
import java.lang.System |
|
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 | 20 |
|
21 |
import org.gjt.sp.jedit.View |
|
22 |
||
23 |
||
24 |
object Info_Dockable |
|
25 |
{ |
|
26 |
/* implicit arguments -- owned by Swing thread */ |
|
27 |
||
52972 | 28 |
private var implicit_snapshot = Document.Snapshot.init |
50507 | 29 |
private var implicit_results = Command.Results.empty |
49726 | 30 |
private var implicit_info: XML.Body = Nil |
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 | 33 |
{ |
34 |
Swing_Thread.require() |
|
35 |
||
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 | 38 |
implicit_info = info |
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
39 |
} |
49726 | 40 |
|
50451 | 41 |
private def reset_implicit(): Unit = |
52972 | 42 |
set_implicit(Document.Snapshot.init, Command.Results.empty, Nil) |
49726 | 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 | 48 |
} |
49 |
} |
|
50 |
||
51 |
||
52 |
class Info_Dockable(view: View, position: String) extends Dockable(view, position) |
|
53 |
{ |
|
54 |
/* component state -- owned by Swing thread */ |
|
55 |
||
56 |
private var zoom_factor = 100 |
|
57 |
||
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
58 |
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
|
59 |
private val results = Info_Dockable.implicit_results |
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
60 |
private val info = Info_Dockable.implicit_info |
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
61 |
|
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
62 |
private val window_focus_listener = |
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
63 |
new WindowFocusListener { |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50451
diff
changeset
|
64 |
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
|
65 |
def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() } |
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
66 |
} |
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
67 |
|
49726 | 68 |
|
69 |
/* pretty text area */ |
|
70 |
||
71 |
private val pretty_text_area = new Pretty_Text_Area(view) |
|
72 |
set_content(pretty_text_area) |
|
73 |
||
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50451
diff
changeset
|
74 |
pretty_text_area.update(snapshot, results, info) |
49726 | 75 |
|
76 |
private def handle_resize() |
|
77 |
{ |
|
78 |
Swing_Thread.require() |
|
79 |
||
50206 | 80 |
pretty_text_area.resize(Rendering.font_family(), |
81 |
(Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round) |
|
49726 | 82 |
} |
83 |
||
84 |
||
50451 | 85 |
/* resize */ |
86 |
||
87 |
private val delay_resize = |
|
88 |
Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
|
89 |
||
90 |
addComponentListener(new ComponentAdapter { |
|
91 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
|
92 |
}) |
|
93 |
||
51616 | 94 |
private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
50451 | 95 |
zoom.tooltip = "Zoom factor for basic font size" |
96 |
||
97 |
private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom) |
|
98 |
add(controls.peer, BorderLayout.NORTH) |
|
99 |
||
100 |
||
49726 | 101 |
/* main actor */ |
102 |
||
103 |
private val main_actor = actor { |
|
104 |
loop { |
|
105 |
react { |
|
50117 | 106 |
case _: Session.Global_Options => |
49726 | 107 |
Swing_Thread.later { handle_resize() } |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52972
diff
changeset
|
108 |
|
49726 | 109 |
case bad => System.err.println("Info_Dockable: ignoring bad message " + bad) |
110 |
} |
|
111 |
} |
|
112 |
} |
|
113 |
||
114 |
override def init() |
|
115 |
{ |
|
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
116 |
JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener)) |
50205 | 117 |
PIDE.session.global_options += main_actor |
49726 | 118 |
handle_resize() |
119 |
} |
|
120 |
||
121 |
override def exit() |
|
122 |
{ |
|
49870
2b82358694e6
retain info dockable state via educated guess on window focus;
wenzelm
parents:
49726
diff
changeset
|
123 |
JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener)) |
50205 | 124 |
PIDE.session.global_options -= main_actor |
49726 | 125 |
delay_resize.revoke() |
126 |
} |
|
127 |
} |