tuned signature -- more abstract PIDE editor operations;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/editor.scala	Mon Aug 12 11:39:29 2013 +0200
@@ -0,0 +1,18 @@
+/*  Title:      Pure/PIDE/editor.scala
+    Author:     Makarius
+
+General editor operations.
+*/
+
+package isabelle
+
+
+abstract class Editor[Context]
+{
+  def session: Session
+  def current_context: Context
+  def current_node(context: Context): Option[Document.Node.Name]
+  def current_snapshot(context: Context): Option[Document.Snapshot]
+  def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]
+}
+

--- a/src/Pure/build-jars	Mon Aug 12 09:08:42 2013 +0200
+++ b/src/Pure/build-jars	Mon Aug 12 11:39:29 2013 +0200
@@ -35,6 +35,7 @@
   PIDE/command.scala
   PIDE/document.scala
   PIDE/document_id.scala
+  PIDE/editor.scala
   PIDE/markup.scala
   PIDE/markup_tree.scala
   PIDE/protocol.scala

--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 12 09:08:42 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 12 11:39:29 2013 +0200
@@ -24,6 +24,7 @@
   "src/isabelle_logic.scala"
   "src/isabelle_options.scala"
   "src/isabelle_sidekick.scala"
+  "src/jedit_editor.scala"
   "src/jedit_lib.scala"
   "src/jedit_main.scala"
   "src/jedit_options.scala"

--- a/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 12 09:08:42 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 12 11:39:29 2013 +0200
@@ -46,7 +46,7 @@
   }
 
   private val find_theorems =
-    Query_Operation(view, "find_theorems", consume_status _,
+    new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _,
       (snapshot, results, body) =>
         pretty_text_area.update(snapshot, results, Pretty.separate(body)))
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:39:29 2013 +0200
@@ -0,0 +1,44 @@
+/*  Title:      Tools/jEdit/src/jedit_editor.scala
+    Author:     Makarius
+
+PIDE editor operations for jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+class JEdit_Editor extends Editor[View]
+{
+  def session: Session = PIDE.session
+
+  def current_context: View =
+    Swing_Thread.require { jEdit.getActiveView() }
+
+  def current_node(view: View): Option[Document.Node.Name] =
+    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.name) }
+
+  def current_snapshot(view: View): Option[Document.Snapshot] =
+    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
+
+  def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
+  {
+    Swing_Thread.require()
+
+    if (snapshot.is_outdated) None
+    else {
+      val text_area = view.getTextArea
+      PIDE.document_view(text_area) match {
+        case Some(doc_view) =>
+          val node = snapshot.version.nodes(doc_view.model.name)
+          node.command_at(text_area.getCaretPosition)
+        case None => None
+      }
+    }
+  }
+}

--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 12 09:08:42 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 12 11:39:29 2013 +0200
@@ -47,6 +47,8 @@
     else Some(current_session.recent_syntax)
   }
 
+  lazy val editor = new JEdit_Editor
+
 
   /* document model and view */
 

--- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 09:08:42 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 11:39:29 2013 +0200
@@ -23,16 +23,10 @@
     val RUNNING = Value("running")
     val FINISHED = Value("finished")
   }
-
-  def apply(
-      view: View,
-      operation_name: String,
-      consume_status: Status.Value => Unit,
-      consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) =
-    new Query_Operation(view, operation_name, consume_status, consume_output)
 }
 
-final class Query_Operation private(
+class Query_Operation(
+  editor: Editor[View],
   view: View,
   operation_name: String,
   consume_status: Query_Operation.Status.Value => Unit,
@@ -156,7 +150,7 @@
   /* query operations */
 
   def cancel_query(): Unit =
-    Swing_Thread.require { PIDE.session.cancel_exec(current_exec_id) }
+    Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
 
   def apply_query(query: List[String])
   {
@@ -221,6 +215,6 @@
     }
   }
 
-  def activate() { PIDE.session.commands_changed += main_actor }
-  def deactivate() { PIDE.session.commands_changed -= main_actor }
+  def activate() { editor.session.commands_changed += main_actor }
+  def deactivate() { editor.session.commands_changed -= main_actor }
 }

--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Aug 12 09:08:42 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Aug 12 11:39:29 2013 +0200
@@ -46,7 +46,7 @@
   }
 
   private val sledgehammer =
-    Query_Operation(view, "sledgehammer", consume_status _,
+    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
       (snapshot, results, body) =>
         pretty_text_area.update(snapshot, results, Pretty.separate(body)))