author | wenzelm |
Wed, 31 Mar 2021 17:15:54 +0200 | |
changeset 73519 | 8f485a199874 |
parent 73340 | 0ffcad1f6130 |
child 73987 | fc363a3b690a |
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._ |
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
66114
diff
changeset
|
11 |
import isabelle.jedit_base.Dockable |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
12 |
|
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53177
diff
changeset
|
13 |
import javax.swing.JComponent |
59286
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59245
diff
changeset
|
14 |
import java.awt.{Point, Font} |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
15 |
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
|
16 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
17 |
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
|
18 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
19 |
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
|
20 |
|
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 |
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
|
23 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56662
diff
changeset
|
24 |
/* implicit arguments -- owned by GUI thread */ |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
25 |
|
52972 | 26 |
private var implicit_snapshot = Document.Snapshot.init |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
27 |
|
59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59233
diff
changeset
|
28 |
private val no_graph: Exn.Result[Graph_Display.Graph] = Exn.Exn(ERROR("No graph")) |
50452
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 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
|
30 |
|
73340 | 31 |
private def set_implicit( |
32 |
snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph]): Unit = |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
33 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56662
diff
changeset
|
34 |
GUI_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
|
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 |
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
|
37 |
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
|
38 |
} |
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 |
private def reset_implicit(): Unit = |
52972 | 41 |
set_implicit(Document.Snapshot.init, no_graph) |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
42 |
|
71742
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
43 |
class Handler extends Active.Handler |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
44 |
{ |
71742
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
45 |
override def handle( |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
46 |
view: View, text: String, elem: XML.Elem, |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
47 |
doc_view: Document_View, snapshot: Document.Snapshot): Boolean = |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
48 |
{ |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
49 |
elem match { |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
50 |
case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) => |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
51 |
Isabelle_Thread.fork(name = "graphview") { |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
52 |
val graph = |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
53 |
Exn.capture { |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
54 |
Graph_Display.decode_graph(body).transitive_reduction_acyclic |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
55 |
} |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
56 |
GUI_Thread.later { |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
57 |
set_implicit(snapshot, graph) |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
58 |
view.getDockableWindowManager.floatDockableWindow("isabelle-graphview") |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
59 |
} |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
60 |
} |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
61 |
true |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
62 |
case _ => false |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
63 |
} |
de37910974da
avoid hard-wired stuff: configure via plugin services;
wenzelm
parents:
71525
diff
changeset
|
64 |
} |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
65 |
} |
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 |
|
49570 | 68 |
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
|
69 |
{ |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
70 |
private val snapshot = Graphview_Dockable.implicit_snapshot |
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
57612
diff
changeset
|
71 |
private val graph_result = 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
|
72 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
73 |
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
|
74 |
new WindowFocusListener { |
73340 | 75 |
def windowGainedFocus(e: WindowEvent): Unit = |
76 |
Graphview_Dockable.set_implicit(snapshot, graph_result) |
|
77 |
def windowLostFocus(e: WindowEvent): Unit = |
|
78 |
Graphview_Dockable.reset_implicit() |
|
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 |
} |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
80 |
|
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
81 |
val graphview = |
59228
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
57612
diff
changeset
|
82 |
graph_result match { |
56b34fc7a015
more dynamic visualizer -- re-use Isabelle/jEdit options;
wenzelm
parents:
57612
diff
changeset
|
83 |
case Exn.Res(graph) => |
59462 | 84 |
val graphview = new isabelle.graphview.Graphview(graph) { |
59395 | 85 |
def options: Options = PIDE.options.value |
86 |
||
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
87 |
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
|
88 |
{ |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52483
diff
changeset
|
89 |
Pretty_Tooltip.invoke(() => |
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52483
diff
changeset
|
90 |
{ |
66114 | 91 |
val model = File_Model.empty(PIDE.session) |
92 |
val rendering = JEdit_Rendering(snapshot, model, options) |
|
65131
5d35f4bccfa7
proper Text.Range.offside (NB: in Scala ~1 == -2);
wenzelm
parents:
64621
diff
changeset
|
93 |
val info = Text.Info(Text.Range.offside, body) |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53177
diff
changeset
|
94 |
Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info) |
52494
a1e09340c0f4
clarified tooltip timing of pending event and active state;
wenzelm
parents:
52483
diff
changeset
|
95 |
}) |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
96 |
null |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
97 |
} |
59395 | 98 |
|
99 |
override def make_font(): Font = |
|
69359 | 100 |
if (editor_style) GUI.imitate_font(Font_Info.main().font) |
61176 | 101 |
else |
102 |
GUI.imitate_font(Font_Info.main().font, |
|
69358
71ef6e6da3dc
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
wenzelm
parents:
66591
diff
changeset
|
103 |
family = options.string("graphview_font_family"), |
71ef6e6da3dc
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
wenzelm
parents:
66591
diff
changeset
|
104 |
scale = options.real("graphview_font_scale")) |
61176 | 105 |
|
106 |
override def foreground_color = |
|
107 |
if (editor_style) view.getTextArea.getPainter.getForeground |
|
108 |
else super.foreground_color |
|
59395 | 109 |
|
61176 | 110 |
override def background_color = |
111 |
if (editor_style) view.getTextArea.getPainter.getBackground |
|
112 |
else super.background_color |
|
113 |
||
114 |
override def selection_color = |
|
115 |
if (editor_style) view.getTextArea.getPainter.getSelectionColor |
|
116 |
else super.selection_color |
|
117 |
||
118 |
override def highlight_color = |
|
119 |
if (editor_style) view.getTextArea.getPainter.getLineHighlightColor |
|
120 |
else super.highlight_color |
|
121 |
||
59233 | 122 |
override def error_color = PIDE.options.color_value("error_color") |
61176 | 123 |
|
124 |
editor_style = true |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
125 |
} |
59459 | 126 |
new isabelle.graphview.Main_Panel(graphview) |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
127 |
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
|
128 |
} |
50452
bfb5964e3041
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm
parents:
50446
diff
changeset
|
129 |
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
|
130 |
|
59288 | 131 |
|
73340 | 132 |
override def focusOnDefaultComponent(): Unit = |
59396 | 133 |
{ |
134 |
graphview match { |
|
135 |
case main_panel: isabelle.graphview.Main_Panel => |
|
136 |
main_panel.tree_panel.tree.requestFocusInWindow |
|
137 |
case _ => |
|
138 |
} |
|
139 |
} |
|
140 |
||
141 |
||
59288 | 142 |
/* main */ |
143 |
||
144 |
private val main = |
|
145 |
Session.Consumer[Session.Global_Options](getClass.getName) { |
|
146 |
case _: Session.Global_Options => |
|
147 |
GUI_Thread.later { |
|
148 |
graphview match { |
|
149 |
case main_panel: isabelle.graphview.Main_Panel => |
|
59392 | 150 |
main_panel.update_layout() |
59288 | 151 |
case _ => |
152 |
} |
|
153 |
} |
|
154 |
} |
|
155 |
||
73340 | 156 |
override def init(): Unit = |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
157 |
{ |
60215 | 158 |
GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener)) |
59288 | 159 |
PIDE.session.global_options += main |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
160 |
} |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
161 |
|
73340 | 162 |
override def exit(): Unit = |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
163 |
{ |
60215 | 164 |
GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener)) |
59288 | 165 |
PIDE.session.global_options -= main |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49557
diff
changeset
|
166 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
167 |
} |