--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Aug 12 11:39:29 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Aug 12 11:49:58 2013 +0200
@@ -22,7 +22,7 @@
{
/* implicit arguments -- owned by Swing thread */
- private var implicit_snapshot = Document.State.init.snapshot()
+ private var implicit_snapshot = Document.Snapshot.init
private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph"))
private var implicit_graph = no_graph
@@ -36,7 +36,7 @@
}
private def reset_implicit(): Unit =
- set_implicit(Document.State.init.snapshot(), no_graph)
+ set_implicit(Document.Snapshot.init, no_graph)
def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
{