# HG changeset patch
# User wenzelm
# Date 1497432898 -7200
# Node ID 0a91f2d976c1fea13c75ed0393c11b175658aff2
# Parent  5e1c1b366ac3aa16023114419cbb2e0b2e03146e
tuned;

diff -r 5e1c1b366ac3 -r 0a91f2d976c1 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Wed Jun 14 11:32:47 2017 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Wed Jun 14 11:34:58 2017 +0200
@@ -64,7 +64,7 @@
   {
     GUI_Thread.require {}
 
-    Document_Model.get(view.getBuffer).map(_.snapshot()) match {
+    PIDE.editor.current_node_snapshot(view) match {
       case Some(snapshot) =>
         (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
           case (Some(command1), Some(command2)) if command1.id == command2.id =>