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