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