src/Tools/jEdit/src/state_dockable.scala
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 =>