author | wenzelm |
Thu, 01 Sep 2016 15:18:14 +0200 | |
changeset 63748 | ebcc70c120a9 |
parent 63681 | d2448471ffba |
child 64664 | 951507563033 |
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 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57594
diff
changeset
|
19 |
GUI_Thread.require {} |
49492 | 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 |
|
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
|
29 |
if (!snapshot.is_outdated) { |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50500
diff
changeset
|
30 |
// FIXME avoid hard-wired stuff |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
31 |
elem match { |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50500
diff
changeset
|
32 |
case XML.Elem(Markup(Markup.BROWSER, _), body) => |
61557 | 33 |
Standard_Thread.fork("browser") { |
56729 | 34 |
val graph_file = Isabelle_System.tmp_file("graph") |
35 |
File.write(graph_file, XML.content(body)) |
|
62609 | 36 |
Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &") |
56729 | 37 |
} |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50500
diff
changeset
|
38 |
|
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50500
diff
changeset
|
39 |
case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) => |
61557 | 40 |
Standard_Thread.fork("graphview") { |
56729 | 41 |
val graph = |
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
58525
diff
changeset
|
42 |
Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic } |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57594
diff
changeset
|
43 |
GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) } |
56729 | 44 |
} |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset
|
45 |
|
63681 | 46 |
case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) => |
47 |
GUI_Thread.later { |
|
48 |
view.getInputHandler.invokeAction(XML.content(body)) |
|
49 |
} |
|
50 |
||
57878
51a2f9140175
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
wenzelm
parents:
57612
diff
changeset
|
51 |
case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) => |
51a2f9140175
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
wenzelm
parents:
57612
diff
changeset
|
52 |
val link = |
51a2f9140175
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
wenzelm
parents:
57612
diff
changeset
|
53 |
props match { |
60893 | 54 |
case Position.Id(id) => PIDE.editor.hyperlink_command_id(true, snapshot, id) |
57878
51a2f9140175
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
wenzelm
parents:
57612
diff
changeset
|
55 |
case _ => None |
51a2f9140175
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
wenzelm
parents:
57612
diff
changeset
|
56 |
} |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57594
diff
changeset
|
57 |
GUI_Thread.later { |
57878
51a2f9140175
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
wenzelm
parents:
57612
diff
changeset
|
58 |
link.foreach(_.follow(view)) |
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57593
diff
changeset
|
59 |
view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace") |
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57593
diff
changeset
|
60 |
} |
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57593
diff
changeset
|
61 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
62 |
case XML.Elem(Markup(Markup.SENDBACK, props), _) => |
58525 | 63 |
if (buffer.isEditable) { |
64 |
props match { |
|
65 |
case Position.Id(id) => |
|
63508 | 66 |
Isabelle.edit_command(snapshot, text_area, |
60215 | 67 |
props.contains(Markup.PADDING_COMMAND), id, text) |
58525 | 68 |
case _ => |
60215 | 69 |
if (props.contains(Markup.PADDING_LINE)) |
58525 | 70 |
Isabelle.insert_line_padding(text_area, text) |
71 |
else text_area.setSelectedText(text) |
|
72 |
} |
|
73 |
text_area.requestFocus |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
74 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
75 |
|
52081
29566b6810f7
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents:
50715
diff
changeset
|
76 |
case Protocol.Dialog(id, serial, result) => |
29566b6810f7
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents:
50715
diff
changeset
|
77 |
model.session.dialog_result(id, serial, result) |
29566b6810f7
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents:
50715
diff
changeset
|
78 |
|
50215 | 79 |
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
|
80 |
} |
49492 | 81 |
} |
82 |
} |
|
83 |
case None => |
|
84 |
} |
|
85 |
} |
|
86 |
} |