22 { |
22 { |
23 /* implicit arguments -- owned by GUI thread */ |
23 /* implicit arguments -- owned by GUI thread */ |
24 |
24 |
25 private var implicit_snapshot = Document.Snapshot.init |
25 private var implicit_snapshot = Document.Snapshot.init |
26 |
26 |
27 private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph")) |
27 private val no_graph: Exn.Result[Graph_Display.Graph] = Exn.Exn(ERROR("No graph")) |
28 private var implicit_graph = no_graph |
28 private var implicit_graph = no_graph |
29 |
29 |
30 private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph]) |
30 private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph]) |
31 { |
31 { |
32 GUI_Thread.require {} |
32 GUI_Thread.require {} |
33 |
33 |
34 implicit_snapshot = snapshot |
34 implicit_snapshot = snapshot |
35 implicit_graph = graph |
35 implicit_graph = graph |
36 } |
36 } |
37 |
37 |
38 private def reset_implicit(): Unit = |
38 private def reset_implicit(): Unit = |
39 set_implicit(Document.Snapshot.init, no_graph) |
39 set_implicit(Document.Snapshot.init, no_graph) |
40 |
40 |
41 def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph]) |
41 def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph]) |
42 { |
42 { |
43 set_implicit(snapshot, graph) |
43 set_implicit(snapshot, graph) |
44 view.getDockableWindowManager.floatDockableWindow("isabelle-graphview") |
44 view.getDockableWindowManager.floatDockableWindow("isabelle-graphview") |
45 } |
45 } |
46 } |
46 } |