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