# HG changeset patch
# User wenzelm
# Date 1376302008 -7200
# Node ID 908e8a36e97567b8e128da74242bd971acb2b36f
# Parent  d5f7fa1498b787b0506d0318f2e476a0a609ded9
tuned signature;

diff -r d5f7fa1498b7 -r 908e8a36e975 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Aug 12 11:56:12 2013 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Aug 12 12:06:48 2013 +0200
@@ -10,9 +10,11 @@
 abstract class Editor[Context]
 {
   def session: Session
+  def flush(): Unit
   def current_context: Context
   def current_node(context: Context): Option[Document.Node.Name]
   def current_snapshot(context: Context): Option[Document.Snapshot]
+  def node_snapshot(name: Document.Node.Name): Document.Snapshot
   def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]
 }
 
diff -r d5f7fa1498b7 -r 908e8a36e975 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 11:56:12 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 12:06:48 2013 +0200
@@ -99,7 +99,7 @@
     if (_node_required != b) {
       _node_required = b
       PIDE.options_changed()
-      PIDE.flush_buffers()
+      PIDE.editor.flush()
     }
   }
 
diff -r d5f7fa1498b7 -r 908e8a36e975 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Aug 12 11:56:12 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Aug 12 12:06:48 2013 +0200
@@ -70,7 +70,7 @@
     if (continuous_checking != b) {
       PIDE.options.bool(CONTINUOUS_CHECKING) = b
       PIDE.options_changed()
-      PIDE.flush_buffers()
+      PIDE.editor.flush()
     }
   }
 
diff -r d5f7fa1498b7 -r 908e8a36e975 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:56:12 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 12:06:48 2013 +0200
@@ -17,6 +17,23 @@
 {
   def session: Session = PIDE.session
 
+  def flush()
+  {
+    Swing_Thread.require()
+
+    session.update(
+      (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
+        case (edits, buffer) =>
+          JEdit_Lib.buffer_lock(buffer) {
+            PIDE.document_model(buffer) match {
+              case Some(model) => model.flushed_edits() ::: edits
+              case None => edits
+            }
+          }
+      }
+    )
+  }
+
   def current_context: View =
     Swing_Thread.require { jEdit.getActiveView() }
 
@@ -26,6 +43,20 @@
   def current_snapshot(view: View): Option[Document.Snapshot] =
     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
 
+  def node_snapshot(name: Document.Node.Name): Document.Snapshot =
+  {
+    Swing_Thread.require()
+
+    JEdit_Lib.jedit_buffer(name.node) match {
+      case Some(buffer) =>
+        PIDE.document_model(buffer) match {
+          case Some(model) => model.snapshot
+          case None => session.snapshot(name)
+        }
+      case None => session.snapshot(name)
+    }
+  }
+
   def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
   {
     Swing_Thread.require()
diff -r d5f7fa1498b7 -r 908e8a36e975 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 12 11:56:12 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 12 12:06:48 2013 +0200
@@ -52,20 +52,6 @@
 
   /* document model and view */
 
-  def document_snapshot(name: Document.Node.Name): Document.Snapshot =
-  {
-    Swing_Thread.require()
-
-    JEdit_Lib.jedit_buffer(name.node) match {
-      case Some(buffer) =>
-        document_model(buffer) match {
-          case Some(model) => model.snapshot
-          case None => session.snapshot(name)
-        }
-      case None => session.snapshot(name)
-    }
-  }
-
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
 
@@ -133,23 +119,6 @@
       Document_View.exit(text_area)
     }
   }
-
-  def flush_buffers()
-  {
-    Swing_Thread.require()
-
-    session.update(
-      (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
-        case (edits, buffer) =>
-          JEdit_Lib.buffer_lock(buffer) {
-            document_model(buffer) match {
-              case Some(model) => model.flushed_edits() ::: edits
-              case None => edits
-            }
-          }
-      }
-    )
-  }
 }
 
 
diff -r d5f7fa1498b7 -r 908e8a36e975 src/Tools/jEdit/src/query_operation.scala
--- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 11:56:12 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 12:06:48 2013 +0200
@@ -78,7 +78,7 @@
     val (snapshot, state, removed) =
       current_location match {
         case Some(cmd) =>
-          val snapshot = PIDE.document_snapshot(cmd.node_name)
+          val snapshot = editor.node_snapshot(cmd.node_name)
           val state = snapshot.state.command_state(snapshot.version, cmd)
           val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
           (snapshot, state, removed)
@@ -139,7 +139,7 @@
           consume_status(new_status)
           if (new_status == Query_Operation.Status.FINISHED) {
             remove_overlay()
-            PIDE.flush_buffers()
+            editor.flush()
           }
         }
       }
@@ -171,7 +171,7 @@
           case None =>
         }
         consume_status(current_status)
-        PIDE.flush_buffers()
+        editor.flush()
       case None =>
     }
   }
@@ -182,7 +182,7 @@
 
     current_location match {
       case Some(command) =>
-        val snapshot = PIDE.document_snapshot(command.node_name)
+        val snapshot = editor.node_snapshot(command.node_name)
         val commands = snapshot.node.commands
         if (commands.contains(command)) {
           // FIXME revert offset (!?)