changeset 64813 | 7283f41d05ab |
parent 61867 | 95cce5313c83 |
child 65246 | 848965b5befc |
--- a/src/Tools/jEdit/src/state_dockable.scala Fri Jan 06 11:58:29 2017 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Fri Jan 06 13:27:18 2017 +0100 @@ -64,7 +64,7 @@ { GUI_Thread.require {} - PIDE.document_model(view.getBuffer).map(_.snapshot()) match { + Document_Model.get(view.getBuffer).map(_.snapshot()) 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 =>