author | wenzelm |
Mon, 05 Aug 2013 15:29:10 +0200 | |
changeset 52862 | 930ce8eacb87 |
parent 52858 | 863581a704a6 |
child 52863 | acbced24e5fc |
permissions | -rw-r--r-- |
52846 | 1 |
/* Title: Tools/jEdit/src/find_dockable.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Dockable window for "find" dialog. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import scala.actors.Actor._ |
|
13 |
||
14 |
import scala.swing.{FlowPanel, Button, Component} |
|
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 |
import org.gjt.sp.jedit.gui.HistoryTextArea |
|
22 |
||
23 |
||
24 |
class Find_Dockable(view: View, position: String) extends Dockable(view, position) |
|
25 |
{ |
|
26 |
Swing_Thread.require() |
|
27 |
||
28 |
||
29 |
/* component state -- owned by Swing thread */ |
|
30 |
||
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
31 |
private val FIND_THEOREMS = "find_theorems" |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
32 |
private val instance = Document_ID.make().toString |
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
33 |
|
52846 | 34 |
private var zoom_factor = 100 |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
35 |
private var current_location: Option[Command] = None |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
36 |
private var current_query: String = "" |
52846 | 37 |
private var current_snapshot = Document.State.init.snapshot() |
38 |
private var current_state = Command.empty.init_state |
|
39 |
private var current_output: List[XML.Tree] = Nil |
|
40 |
||
41 |
||
42 |
/* pretty text area */ |
|
43 |
||
44 |
val pretty_text_area = new Pretty_Text_Area(view) |
|
45 |
set_content(pretty_text_area) |
|
46 |
||
47 |
||
48 |
private def handle_resize() |
|
49 |
{ |
|
50 |
Swing_Thread.require() |
|
51 |
||
52 |
pretty_text_area.resize(Rendering.font_family(), |
|
53 |
(Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round) |
|
54 |
} |
|
55 |
||
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
56 |
private def handle_update() |
52846 | 57 |
{ |
58 |
Swing_Thread.require() |
|
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
59 |
|
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
60 |
val (new_snapshot, new_state) = |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
61 |
Document_View(view.getTextArea) match { |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
62 |
case Some(doc_view) => |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
63 |
val snapshot = doc_view.model.snapshot() |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
64 |
if (!snapshot.is_outdated) { |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
65 |
current_location match { |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
66 |
case Some(cmd) => |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
67 |
(snapshot, snapshot.state.command_state(snapshot.version, cmd)) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
68 |
case None => |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
69 |
(Document.State.init.snapshot(), Command.empty.init_state) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
70 |
} |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
71 |
} |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
72 |
else (current_snapshot, current_state) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
73 |
case None => (current_snapshot, current_state) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
74 |
} |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
75 |
|
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
76 |
val new_output = |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
77 |
(for { |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
78 |
(_, XML.Elem(Markup(Markup.RESULT, props), body)) <- new_state.results.entries |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
79 |
if props.contains((Markup.KIND, FIND_THEOREMS)) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
80 |
if props.contains((Markup.INSTANCE, instance)) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
81 |
} yield XML.Elem(Markup(Markup.WRITELN_MESSAGE, Nil), body)).toList |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
82 |
|
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
83 |
if (new_output != current_output) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
84 |
pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output)) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
85 |
|
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
86 |
current_snapshot = new_snapshot |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
87 |
current_state = new_state |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
88 |
current_output = new_output |
52846 | 89 |
} |
90 |
||
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
91 |
private def clear_overlay() |
52846 | 92 |
{ |
93 |
Swing_Thread.require() |
|
52848 | 94 |
|
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
95 |
for { |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
96 |
command <- current_location |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
97 |
buffer <- JEdit_Lib.jedit_buffer(command.node_name.node) |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
98 |
model <- PIDE.document_model(buffer) |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
99 |
} model.remove_overlay(command, FIND_THEOREMS, List(instance, current_query)) |
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
100 |
|
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
101 |
current_location = None |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
102 |
current_query = "" |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
103 |
} |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
104 |
|
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
105 |
private def apply_query(query: String) |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
106 |
{ |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
107 |
Swing_Thread.require() |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
108 |
|
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
109 |
clear_overlay() |
52848 | 110 |
Document_View(view.getTextArea) match { |
111 |
case Some(doc_view) => |
|
112 |
val snapshot = doc_view.model.snapshot() |
|
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
113 |
snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
114 |
case Some(command) => |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
115 |
current_location = Some(command) |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
116 |
current_query = query |
52862
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52858
diff
changeset
|
117 |
doc_view.model.insert_overlay(command, FIND_THEOREMS, List(instance, query)) |
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
118 |
case None => |
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52848
diff
changeset
|
119 |
} |
52848 | 120 |
case None => |
121 |
} |
|
52858
863581a704a6
avoid repeated PIDE.flush_buffers when manipulating overlays;
wenzelm
parents:
52854
diff
changeset
|
122 |
|
863581a704a6
avoid repeated PIDE.flush_buffers when manipulating overlays;
wenzelm
parents:
52854
diff
changeset
|
123 |
PIDE.flush_buffers() |
52846 | 124 |
} |
125 |
||
126 |
private def locate_query() |
|
127 |
{ |
|
128 |
Swing_Thread.require() |
|
52848 | 129 |
|
130 |
current_location match { |
|
131 |
case Some(command) => |
|
132 |
val snapshot = PIDE.session.snapshot(command.node_name) |
|
133 |
val commands = snapshot.node.commands |
|
134 |
if (commands.contains(command)) { |
|
135 |
val sources = commands.iterator.takeWhile(_ != command).map(_.source) |
|
136 |
val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) |
|
137 |
Hyperlink(command.node_name.node, line, column).follow(view) |
|
138 |
} |
|
139 |
case None => |
|
140 |
} |
|
52846 | 141 |
} |
142 |
||
143 |
||
144 |
/* main actor */ |
|
145 |
||
146 |
private val main_actor = actor { |
|
147 |
loop { |
|
148 |
react { |
|
149 |
case _: Session.Global_Options => |
|
150 |
Swing_Thread.later { handle_resize() } |
|
151 |
case changed: Session.Commands_Changed => |
|
152 |
current_location match { |
|
153 |
case Some(command) if changed.commands.contains(command) => |
|
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
154 |
Swing_Thread.later { handle_update() } |
52846 | 155 |
case _ => |
156 |
} |
|
157 |
case bad => |
|
158 |
java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad) |
|
159 |
} |
|
160 |
} |
|
161 |
} |
|
162 |
||
163 |
override def init() |
|
164 |
{ |
|
165 |
Swing_Thread.require() |
|
166 |
||
167 |
PIDE.session.global_options += main_actor |
|
168 |
PIDE.session.commands_changed += main_actor |
|
52848 | 169 |
handle_resize() |
52846 | 170 |
} |
171 |
||
172 |
override def exit() |
|
173 |
{ |
|
174 |
Swing_Thread.require() |
|
175 |
||
176 |
PIDE.session.global_options -= main_actor |
|
177 |
PIDE.session.commands_changed -= main_actor |
|
178 |
delay_resize.revoke() |
|
179 |
} |
|
180 |
||
181 |
||
182 |
/* resize */ |
|
183 |
||
184 |
private val delay_resize = |
|
185 |
Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
|
186 |
||
187 |
addComponentListener(new ComponentAdapter { |
|
188 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
|
189 |
}) |
|
190 |
||
191 |
||
192 |
/* controls */ |
|
193 |
||
194 |
private val query = new HistoryTextArea("isabelle-find-theorems") { |
|
195 |
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) } |
|
196 |
setColumns(25) |
|
197 |
setRows(1) |
|
198 |
} |
|
199 |
||
200 |
private val query_wrapped = Component.wrap(query) |
|
201 |
||
202 |
private val find = new Button("Find") { |
|
203 |
tooltip = "Find theorems meeting specified criteria" |
|
204 |
reactions += { case ButtonClicked(_) => apply_query(query.getText) } |
|
205 |
} |
|
206 |
||
207 |
private val locate = new Button("Locate") { |
|
208 |
tooltip = "Locate context of current query within source text" |
|
209 |
reactions += { case ButtonClicked(_) => locate_query() } |
|
210 |
} |
|
211 |
||
212 |
private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) { |
|
213 |
tooltip = "Zoom factor for output font size" |
|
214 |
} |
|
215 |
||
216 |
private val controls = |
|
217 |
new FlowPanel(FlowPanel.Alignment.Right)(query_wrapped, find, locate, zoom) |
|
218 |
add(controls.peer, BorderLayout.NORTH) |
|
219 |
} |