author | wenzelm |
Mon, 08 Oct 2012 12:40:35 +0200 | |
changeset 49730 | e0d98ff3c0db |
parent 49570 | 2265456f6131 |
child 49735 | 30e2f3f1c623 |
permissions | -rw-r--r-- |
49570 | 1 |
/* Title: Tools/jEdit/src/graphview_dockable.scala |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Markus Kaiser, TU Muenchen |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
3 |
Author: Makarius |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
5 |
Dockable window for graphview. |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
6 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
7 |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
8 |
package isabelle.jedit |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
9 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
10 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
11 |
import isabelle._ |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
12 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
13 |
import java.awt.BorderLayout |
49730 | 14 |
import javax.swing.{JPanel, JComponent} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
import scala.actors.Actor._ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
17 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
18 |
import org.gjt.sp.jedit.View |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
19 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
20 |
|
49570 | 21 |
class Graphview_Dockable(view: View, position: String) extends Dockable(view, position) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
22 |
{ |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
23 |
Swing_Thread.require() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
24 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
25 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
26 |
/* component state -- owned by Swing thread */ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
27 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
28 |
private val do_update = true // FIXME |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
29 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
30 |
private var current_snapshot = Document.State.init.snapshot() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
31 |
private var current_state = Command.empty.init_state |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
32 |
private var current_graph: XML.Body = Nil |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
33 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
34 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
35 |
/* GUI components */ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
36 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
37 |
private val graphview = new JPanel |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
38 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
39 |
// FIXME mutable GUI content |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
40 |
private def set_graphview(graph: XML.Body) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
41 |
{ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
42 |
graphview.removeAll() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
43 |
graphview.setLayout(new BorderLayout) |
49730 | 44 |
val panel = |
45 |
new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) { |
|
46 |
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
|
47 |
{ |
|
48 |
val rendering = Isabelle_Rendering(current_snapshot, Isabelle.options.value) |
|
49 |
new Pretty_Tooltip(view, parent, rendering, x, y, body) |
|
50 |
null |
|
51 |
} |
|
52 |
} |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
53 |
graphview.add(panel.peer, BorderLayout.CENTER) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
54 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
55 |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
56 |
set_graphview(current_graph) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
57 |
set_content(graphview) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
58 |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
59 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
60 |
private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
61 |
{ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
62 |
Swing_Thread.require() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
63 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
64 |
val (new_snapshot, new_state) = |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
65 |
Document_View(view.getTextArea) match { |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
66 |
case Some(doc_view) => |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
67 |
val snapshot = doc_view.model.snapshot() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
68 |
if (follow && !snapshot.is_outdated) { |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
69 |
snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
70 |
case Some(cmd) => |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
71 |
(snapshot, snapshot.state.command_state(snapshot.version, cmd)) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
72 |
case None => |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
73 |
(Document.State.init.snapshot(), Command.empty.init_state) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
74 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
75 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
76 |
else (current_snapshot, current_state) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
77 |
case None => (current_snapshot, current_state) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
78 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
79 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
80 |
val new_graph = |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
81 |
if (!restriction.isDefined || restriction.get.contains(new_state.command)) { |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
82 |
new_state.markup.cumulate[Option[XML.Body]]( |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
83 |
new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)), |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
84 |
{ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
85 |
case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) => |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
86 |
Some(graph) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
87 |
}).filter(_.info.isDefined) match { |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
88 |
case Text.Info(_, Some(graph)) #:: _ => graph |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
89 |
case _ => Nil |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
90 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
91 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
92 |
else current_graph |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
93 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
94 |
if (new_graph != current_graph) set_graphview(new_graph) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
95 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
96 |
current_snapshot = new_snapshot |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
97 |
current_state = new_state |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
98 |
current_graph = new_graph |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
99 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
100 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
101 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
102 |
/* main actor */ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
103 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
104 |
private val main_actor = actor { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
105 |
loop { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
106 |
react { |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
107 |
case Session.Global_Options => // FIXME |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
108 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
109 |
case changed: Session.Commands_Changed => |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
110 |
Swing_Thread.later { handle_update(do_update, Some(changed.commands)) } |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
111 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
112 |
case Session.Caret_Focus => |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
113 |
Swing_Thread.later { handle_update(do_update, None) } |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
114 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
115 |
case bad => |
49570 | 116 |
java.lang.System.err.println("Graphview_Dockable: ignoring bad message " + bad) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
117 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
118 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
119 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
120 |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
121 |
override def init() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
122 |
{ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
123 |
Swing_Thread.require() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
124 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
125 |
Isabelle.session.global_options += main_actor |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
126 |
Isabelle.session.commands_changed += main_actor |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
127 |
Isabelle.session.caret_focus += main_actor |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
128 |
handle_update(do_update, None) |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
129 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
130 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
131 |
override def exit() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
132 |
{ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
133 |
Swing_Thread.require() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
134 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
135 |
Isabelle.session.global_options -= main_actor |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
136 |
Isabelle.session.commands_changed -= main_actor |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
137 |
Isabelle.session.caret_focus -= main_actor |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
138 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
139 |
} |