tuned;
authorwenzelm
Wed, 14 Jun 2017 11:34:58 +0200
changeset 66091 0a91f2d976c1
parent 66090 5e1c1b366ac3
child 66092 f5595bef6545
tuned;
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 =>