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