|
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 |
|
14 import scala.swing.{FlowPanel, Button, CheckBox} |
|
15 import scala.swing.event.ButtonClicked |
|
16 |
|
17 import java.lang.System |
|
18 import java.awt.BorderLayout |
|
19 import java.awt.event.{ComponentEvent, ComponentAdapter} |
|
20 |
|
21 import org.gjt.sp.jedit.View |
|
22 |
|
23 |
|
24 object Info_Dockable |
|
25 { |
|
26 /* implicit arguments -- owned by Swing thread */ |
|
27 |
|
28 private var implicit_snapshot = Document.State.init.snapshot() |
|
29 private var implicit_info: XML.Body = Nil |
|
30 |
|
31 def apply(view: View, snapshot: Document.Snapshot, info: XML.Body) |
|
32 { |
|
33 Swing_Thread.require() |
|
34 |
|
35 implicit_snapshot = snapshot |
|
36 implicit_info = info |
|
37 |
|
38 view.getDockableWindowManager.floatDockableWindow("isabelle-info") |
|
39 |
|
40 implicit_snapshot = Document.State.init.snapshot() |
|
41 implicit_info = Nil |
|
42 } |
|
43 } |
|
44 |
|
45 |
|
46 class Info_Dockable(view: View, position: String) extends Dockable(view, position) |
|
47 { |
|
48 Swing_Thread.require() |
|
49 |
|
50 |
|
51 /* component state -- owned by Swing thread */ |
|
52 |
|
53 private var zoom_factor = 100 |
|
54 |
|
55 |
|
56 /* pretty text area */ |
|
57 |
|
58 private val pretty_text_area = new Pretty_Text_Area(view) |
|
59 set_content(pretty_text_area) |
|
60 |
|
61 pretty_text_area.update(Info_Dockable.implicit_snapshot, Info_Dockable.implicit_info) |
|
62 |
|
63 private def handle_resize() |
|
64 { |
|
65 Swing_Thread.require() |
|
66 |
|
67 pretty_text_area.resize(Isabelle.font_family(), |
|
68 scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100)) |
|
69 } |
|
70 |
|
71 |
|
72 /* main actor */ |
|
73 |
|
74 private val main_actor = actor { |
|
75 loop { |
|
76 react { |
|
77 case Session.Global_Options => |
|
78 Swing_Thread.later { handle_resize() } |
|
79 case bad => System.err.println("Info_Dockable: ignoring bad message " + bad) |
|
80 } |
|
81 } |
|
82 } |
|
83 |
|
84 override def init() |
|
85 { |
|
86 Swing_Thread.require() |
|
87 |
|
88 Isabelle.session.global_options += main_actor |
|
89 handle_resize() |
|
90 } |
|
91 |
|
92 override def exit() |
|
93 { |
|
94 Swing_Thread.require() |
|
95 |
|
96 Isabelle.session.global_options -= main_actor |
|
97 delay_resize.revoke() |
|
98 } |
|
99 |
|
100 |
|
101 /* resize */ |
|
102 |
|
103 private val delay_resize = |
|
104 Swing_Thread.delay_first( |
|
105 Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() } |
|
106 |
|
107 addComponentListener(new ComponentAdapter { |
|
108 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
|
109 }) |
|
110 |
|
111 |
|
112 /* controls */ |
|
113 |
|
114 private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
|
115 zoom.tooltip = "Zoom factor for basic font size" |
|
116 |
|
117 private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom) |
|
118 add(controls.peer, BorderLayout.NORTH) |
|
119 } |