# 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 =>