author | wenzelm |
Mon, 10 Dec 2012 15:17:47 +0100 | |
changeset 50452 | bfb5964e3041 |
parent 50446 | 8dc05db0bf69 |
child 50501 | 6f41f1646617 |
permissions | -rw-r--r-- |
49570 | 1 |
/* Title: Tools/jEdit/src/graphview_dockable.scala |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
2 |
Author: Makarius |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
3 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
4 |
Stateless 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
|
5 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
6 |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
7 |
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
|
8 |
|
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 |
import isabelle._ |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
11 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
12 |
import javax.swing.JComponent |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
13 |
import java.awt.event.{WindowFocusListener, WindowEvent} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
14 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
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
|
16 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
17 |
import scala.swing.TextArea |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
18 |
|
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
19 |
|
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
20 |
object Graphview_Dockable |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
21 |
{ |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
22 |
/* implicit arguments -- owned by Swing thread */ |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
23 |
|
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
24 |
private var implicit_snapshot = Document.State.init.snapshot() |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
25 |
|
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
26 |
private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph")) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
27 |
private var implicit_graph = no_graph |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
28 |
|
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
29 |
private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph]) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
30 |
{ |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
31 |
Swing_Thread.require() |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
32 |
|
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
33 |
implicit_snapshot = snapshot |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
34 |
implicit_graph = graph |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
35 |
} |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
36 |
|
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
37 |
private def reset_implicit(): Unit = |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
38 |
set_implicit(Document.State.init.snapshot(), no_graph) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
39 |
|
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
40 |
def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph]) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
41 |
{ |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
42 |
set_implicit(snapshot, graph) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
43 |
view.getDockableWindowManager.floatDockableWindow("isabelle-graphview") |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
44 |
} |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
45 |
} |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
46 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
47 |
|
49570 | 48 |
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
|
49 |
{ |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
50 |
Swing_Thread.require() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
51 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
52 |
private val snapshot = Graphview_Dockable.implicit_snapshot |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
53 |
private val graph = Graphview_Dockable.implicit_graph |
50446
8dc05db0bf69
always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
wenzelm
parents:
50205
diff
changeset
|
54 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
55 |
private val window_focus_listener = |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
56 |
new WindowFocusListener { |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
57 |
def windowGainedFocus(e: WindowEvent) { Graphview_Dockable.set_implicit(snapshot, graph) } |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
58 |
def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() } |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
59 |
} |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
60 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
61 |
val graphview = |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
62 |
graph match { |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
63 |
case Exn.Res(proper_graph) => |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
64 |
new isabelle.graphview.Main_Panel(proper_graph) { |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
65 |
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
66 |
{ |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
67 |
val rendering = Rendering(snapshot, PIDE.options.value) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
68 |
new Pretty_Tooltip(view, parent, rendering, x, y, body) |
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
69 |
null |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
70 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
71 |
} |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
72 |
case Exn.Exn(exn) => new TextArea(Exn.message(exn)) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
73 |
} |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
74 |
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
|
75 |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
76 |
override def init() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
77 |
{ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
78 |
Swing_Thread.require() |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
79 |
JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener)) |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
80 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
81 |
|
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
82 |
override def exit() |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
83 |
{ |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
84 |
Swing_Thread.require() |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
85 |
JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener)) |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
86 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
87 |
} |