author | wenzelm |
Mon, 10 Dec 2012 19:28:56 +0100 | |
changeset 50466 | 53d3930dae0c |
parent 50452 | bfb5964e3041 |
child 50498 | 6647ba2775c1 |
permissions | -rw-r--r-- |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/active.scala |
49492 | 2 |
Author: Makarius |
3 |
||
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
4 |
Active areas within the document. |
49492 | 5 |
*/ |
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
12 |
import org.gjt.sp.jedit.View |
49492 | 13 |
|
14 |
||
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
15 |
object Active |
49492 | 16 |
{ |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
17 |
def action(view: View, text: String, elem: XML.Elem) |
49492 | 18 |
{ |
19 |
Swing_Thread.require() |
|
20 |
||
21 |
Document_View(view.getTextArea) match { |
|
22 |
case Some(doc_view) => |
|
23 |
doc_view.rich_text_area.robust_body() { |
|
50215 | 24 |
val text_area = doc_view.text_area |
49492 | 25 |
val model = doc_view.model |
26 |
val buffer = model.buffer |
|
27 |
val snapshot = model.snapshot() |
|
49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset
|
28 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
29 |
def try_replace_command(exec_id: Document.ID, s: String) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
30 |
{ |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
31 |
snapshot.state.execs.get(exec_id).map(_.command) match { |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
32 |
case Some(command) => |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
33 |
snapshot.node.command_start(command) match { |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
34 |
case Some(start) => |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
35 |
JEdit_Lib.buffer_edit(buffer) { |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
36 |
buffer.remove(start, command.proper_range.length) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
37 |
buffer.insert(start, s) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
38 |
} |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
39 |
case None => |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
40 |
} |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
41 |
case None => |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
42 |
} |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
43 |
} |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
44 |
|
50164
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset
|
45 |
if (!snapshot.is_outdated) { |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
46 |
elem match { |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
47 |
case XML.Elem(Markup(Markup.SENDBACK, props), _) => |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
48 |
props match { |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
49 |
case Position.Id(exec_id) => |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
50 |
try_replace_command(exec_id, text) |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
51 |
case _ => |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
52 |
if (props.exists(_ == Markup.PADDING_LINE)) |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
53 |
Isabelle.insert_line_padding(text_area, text) |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
54 |
else text_area.setSelectedText(text) |
50164
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset
|
55 |
} |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
56 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
57 |
case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) => |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
58 |
default_thread_pool.submit(() => |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
59 |
{ |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
60 |
val graph = |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
61 |
Exn.capture { |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
62 |
isabelle.graphview.Model.decode_graph(body) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
63 |
.transitive_reduction_acyclic |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
64 |
} |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
65 |
Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) } |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50450
diff
changeset
|
66 |
}) |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
67 |
|
50215 | 68 |
case _ => |
50164
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset
|
69 |
} |
49492 | 70 |
} |
71 |
} |
|
72 |
case None => |
|
73 |
} |
|
74 |
} |
|
75 |
} |
|
76 |