# 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 =>