1 /* Title: Tools/jEdit/src/jedit/output_dockable.scala |
|
2 Author: Makarius |
|
3 |
|
4 Dockable window with result message output. |
|
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.awt.BorderLayout |
|
18 import java.awt.event.{ComponentEvent, ComponentAdapter} |
|
19 |
|
20 import org.gjt.sp.jedit.View |
|
21 |
|
22 |
|
23 class Output_Dockable(view: View, position: String) extends Dockable(view, position) |
|
24 { |
|
25 Swing_Thread.require() |
|
26 |
|
27 private val html_panel = |
|
28 new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size())) |
|
29 { |
|
30 override val handler: PartialFunction[HTML_Panel.Event, Unit] = { |
|
31 case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" => |
|
32 val text = elem.getFirstChild().getNodeValue() |
|
33 |
|
34 Document_View(view.getTextArea) match { |
|
35 case Some(doc_view) => |
|
36 val cmd = current_command.get |
|
37 val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get |
|
38 val buffer = view.getBuffer |
|
39 buffer.beginCompoundEdit() |
|
40 buffer.remove(start_ofs, cmd.length) |
|
41 buffer.insert(start_ofs, text) |
|
42 buffer.endCompoundEdit() |
|
43 case None => |
|
44 } |
|
45 } |
|
46 } |
|
47 |
|
48 set_content(html_panel) |
|
49 |
|
50 |
|
51 /* component state -- owned by Swing thread */ |
|
52 |
|
53 private var zoom_factor = 100 |
|
54 private var show_tracing = false |
|
55 private var follow_caret = true |
|
56 private var current_command: Option[Command] = None |
|
57 |
|
58 |
|
59 private def handle_resize() |
|
60 { |
|
61 Swing_Thread.now { |
|
62 html_panel.resize(Isabelle.font_family(), |
|
63 scala.math.round(Isabelle.font_size() * zoom_factor / 100)) |
|
64 } |
|
65 } |
|
66 |
|
67 private def handle_perspective(): Boolean = |
|
68 Swing_Thread.now { |
|
69 Document_View(view.getTextArea) match { |
|
70 case Some(doc_view) => |
|
71 val cmd = doc_view.selected_command() |
|
72 if (current_command == cmd) false |
|
73 else { current_command = cmd; true } |
|
74 case None => false |
|
75 } |
|
76 } |
|
77 |
|
78 private def handle_update(restriction: Option[Set[Command]] = None) |
|
79 { |
|
80 Swing_Thread.now { |
|
81 if (follow_caret) handle_perspective() |
|
82 Document_View(view.getTextArea) match { |
|
83 case Some(doc_view) => |
|
84 current_command match { |
|
85 case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
|
86 val snapshot = doc_view.model.snapshot() |
|
87 val filtered_results = |
|
88 snapshot.state(cmd).results.iterator.map(_._2) filter { |
|
89 case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable |
|
90 case _ => true |
|
91 } |
|
92 html_panel.render(filtered_results.toList) |
|
93 case _ => |
|
94 } |
|
95 case None => |
|
96 } |
|
97 } |
|
98 } |
|
99 |
|
100 |
|
101 /* main actor */ |
|
102 |
|
103 private val main_actor = actor { |
|
104 loop { |
|
105 react { |
|
106 case Session.Global_Settings => handle_resize() |
|
107 case Session.Commands_Changed(changed) => handle_update(Some(changed)) |
|
108 case Session.Perspective => if (follow_caret && handle_perspective()) handle_update() |
|
109 case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) |
|
110 } |
|
111 } |
|
112 } |
|
113 |
|
114 override def init() |
|
115 { |
|
116 Isabelle.session.global_settings += main_actor |
|
117 Isabelle.session.commands_changed += main_actor |
|
118 Isabelle.session.perspective += main_actor |
|
119 } |
|
120 |
|
121 override def exit() |
|
122 { |
|
123 Isabelle.session.global_settings -= main_actor |
|
124 Isabelle.session.commands_changed -= main_actor |
|
125 Isabelle.session.perspective -= main_actor |
|
126 } |
|
127 |
|
128 |
|
129 /* resize */ |
|
130 |
|
131 addComponentListener(new ComponentAdapter { |
|
132 val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() } |
|
133 override def componentResized(e: ComponentEvent) { delay() } |
|
134 }) |
|
135 |
|
136 |
|
137 /* controls */ |
|
138 |
|
139 private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
|
140 zoom.tooltip = "Zoom factor for basic font size" |
|
141 |
|
142 private val tracing = new CheckBox("Tracing") { |
|
143 reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
|
144 } |
|
145 tracing.selected = show_tracing |
|
146 tracing.tooltip = "Indicate output of tracing messages" |
|
147 |
|
148 private val auto_update = new CheckBox("Auto update") { |
|
149 reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } |
|
150 } |
|
151 auto_update.selected = follow_caret |
|
152 auto_update.tooltip = "Indicate automatic update following cursor movement" |
|
153 |
|
154 private val update = new Button("Update") { |
|
155 reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() } |
|
156 } |
|
157 update.tooltip = "Update display according to the command at cursor position" |
|
158 |
|
159 private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) |
|
160 add(controls.peer, BorderLayout.NORTH) |
|
161 |
|
162 handle_update() |
|
163 } |
|