# HG changeset patch
# User wenzelm
# Date 1353591639 -3600
# Node ID 77668b522ffeaceff6d7771dda5f30482220b6df
# Parent  c62ce309dc268ead549db668519b32b0548bae16
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;

diff -r c62ce309dc26 -r 77668b522ffe src/Pure/PIDE/sendback.ML
--- a/src/Pure/PIDE/sendback.ML	Thu Nov 22 13:21:02 2012 +0100
+++ b/src/Pure/PIDE/sendback.ML	Thu Nov 22 14:40:39 2012 +0100
@@ -9,6 +9,7 @@
 sig
   val make_markup: unit -> Markup.T
   val markup: string -> string
+  val markup_implicit: string -> string
 end;
 
 structure Sendback: SENDBACK =
@@ -24,5 +25,7 @@
 
 fun markup s = Markup.markup (make_markup ()) s;
 
+val markup_implicit = Markup.markup Isabelle_Markup.sendback;
+
 end;
 
diff -r c62ce309dc26 -r 77668b522ffe src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Nov 22 13:21:02 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Nov 22 14:40:39 2012 +0100
@@ -245,11 +245,11 @@
   }
 
 
-  def sendback(range: Text.Range): Option[Text.Info[Document.Exec_ID]] =
+  def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
     snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)),
         {
-          case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, Position.Id(id)), _)) =>
-            Text.Info(snapshot.convert(info_range), id)
+          case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, props), _)) =>
+            Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
 
 
diff -r c62ce309dc26 -r 77668b522ffe src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 22 13:21:02 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Nov 22 14:40:39 2012 +0100
@@ -136,7 +136,7 @@
   private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
   private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
   private val sendback_area =
-    new Active_Area[Document.Exec_ID]((r: Isabelle_Rendering) => r.sendback _)
+    new Active_Area[Option[Document.Exec_ID]]((r: Isabelle_Rendering) => r.sendback _)
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
diff -r c62ce309dc26 -r 77668b522ffe src/Tools/jEdit/src/sendback.scala
--- a/src/Tools/jEdit/src/sendback.scala	Thu Nov 22 13:21:02 2012 +0100
+++ b/src/Tools/jEdit/src/sendback.scala	Thu Nov 22 14:40:39 2012 +0100
@@ -14,7 +14,7 @@
 
 object Sendback
 {
-  def activate(view: View, text: String, exec_id: Document.Exec_ID)
+  def activate(view: View, text: String, id: Option[Document.Exec_ID])
   {
     Swing_Thread.require()
 
@@ -25,19 +25,28 @@
           val buffer = model.buffer
           val snapshot = model.snapshot()
 
-          snapshot.state.execs.get(exec_id).map(_.command) match {
-            case Some(command) if !snapshot.is_outdated =>
-              snapshot.node.command_start(command) match {
-                case Some(start) =>
-                  try {
-                    buffer.beginCompoundEdit()
-                    buffer.remove(start, command.proper_range.length)
-                    buffer.insert(start, text)
-                  }
-                  finally { buffer.endCompoundEdit() }
-                case None =>
-              }
-            case _ =>
+          if (!snapshot.is_outdated) {
+            id match {
+              case None =>
+                doc_view.text_area.setSelectedText(text)
+              case Some(exec_id) =>
+                snapshot.state.execs.get(exec_id).map(_.command) match {
+                  case Some(command) =>
+                    snapshot.node.command_start(command) match {
+                      case Some(start) =>
+                        try {
+                          buffer.beginCompoundEdit()
+                          buffer.remove(start, command.proper_range.length)
+                          buffer.insert(start, text)
+                        }
+                        finally {
+                          buffer.endCompoundEdit()
+                        }
+                      case None =>
+                    }
+                  case None =>
+                }
+            }
           }
         }
       case None =>