# HG changeset patch # User wenzelm # Date 1348234791 -7200 # Node ID 2e3e7ea5ce8e4f8c1240fda6d4906bb9d8c119e1 # Parent 6b48c76f5b3fadb3cb891d3e9f7361e447501497 some support for hovering and sendback area; diff -r 6b48c76f5b3f -r 2e3e7ea5ce8e src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Fri Sep 21 12:07:59 2012 +0200 +++ b/src/Tools/jEdit/etc/options Fri Sep 21 15:39:51 2012 +0200 @@ -40,6 +40,8 @@ option quoted_color : string = "8B8B8B19" option highlight_color : string = "50505032" option hyperlink_color : string = "000000FF" +option sendback_color : string = "DCDCDCFF" +option sendback_active_color : string = "9DC75DFF" option keyword1_color : string = "006699FF" option keyword2_color : string = "009966FF" diff -r 6b48c76f5b3f -r 2e3e7ea5ce8e src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 21 12:07:59 2012 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Sep 21 15:39:51 2012 +0200 @@ -30,6 +30,7 @@ "src/readme_dockable.scala" "src/rich_text_area.scala" "src/scala_console.scala" + "src/sendback.scala" "src/session_dockable.scala" "src/syslog_dockable.scala" "src/text_overview.scala" diff -r 6b48c76f5b3f -r 2e3e7ea5ce8e src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Fri Sep 21 12:07:59 2012 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 21 15:39:51 2012 +0200 @@ -70,7 +70,7 @@ def get_rendering(): Isabelle_Rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value) - val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _) + val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false) /* perspective */ diff -r 6b48c76f5b3f -r 2e3e7ea5ce8e src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 21 12:07:59 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 21 15:39:51 2012 +0200 @@ -125,6 +125,8 @@ val quoted_color = color_value("quoted_color") val highlight_color = color_value("highlight_color") val hyperlink_color = color_value("hyperlink_color") + val sendback_color = color_value("sendback_color") + val sendback_active_color = color_value("sendback_active_color") val keyword1_color = color_value("keyword1_color") val keyword2_color = color_value("keyword2_color") @@ -237,6 +239,22 @@ } + def sendback(range: Text.Range): Option[Text.Info[Sendback]] = + { + snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)), + { + case Text.Info(info_range, Protocol.Sendback(body)) => + Text.Info(snapshot.convert(info_range), body) + }) match + { + case Text.Info(_, Text.Info(range, body)) #:: _ => + snapshot.node.command_at(range.start) + .map(command_range => Text.Info(range, Sendback(command_range._1, body))) + case _ => None + } + } + + private def tooltip_text(msg: XML.Tree): String = Pretty.string_of(List(msg), margin = options.int("jedit_tooltip_margin")) @@ -388,6 +406,13 @@ message_colors.get(pri).map((_, is_separator)) } + + private val background1_include = + Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE + + Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE + + Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY + + Isabelle_Markup.SENDBACK + def background1(range: Text.Range): Stream[Text.Info[Color]] = { if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color)) @@ -395,10 +420,7 @@ for { Text.Info(r, result) <- snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])]( - range, (Some(Protocol.Status.init), None), - Some(Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE + - Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE + - Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY), + range, (Some(Protocol.Status.init), None), Some(background1_include), { case (((Some(status), color), Text.Info(_, XML.Elem(markup, _)))) if (Protocol.command_status_markup(markup.name)) => @@ -407,6 +429,8 @@ (None, Some(bad_color)) case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) => (None, Some(intensify_color)) + case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) => + (None, Some(sendback_color)) }) color <- (result match { diff -r 6b48c76f5b3f -r 2e3e7ea5ce8e src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Sep 21 12:07:59 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Sep 21 15:39:51 2012 +0200 @@ -67,7 +67,7 @@ Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2 private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None - private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering) + private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering, true) def refresh() { diff -r 6b48c76f5b3f -r 2e3e7ea5ce8e src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Fri Sep 21 12:07:59 2012 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Sep 21 15:39:51 2012 +0200 @@ -23,7 +23,11 @@ import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea} -class Rich_Text_Area(view: View, text_area: TextArea, get_rendering: () => Isabelle_Rendering) +class Rich_Text_Area( + view: View, + text_area: TextArea, + get_rendering: () => Isabelle_Rendering, + hovering: Boolean) { private val buffer = text_area.getBuffer @@ -123,8 +127,11 @@ 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 active_areas = List(highlight_area, hyperlink_area) - private def active_reset(): Unit = active_areas.foreach(_.reset) + private val sendback_area = new Active_Area[Sendback]((r: Isabelle_Rendering) => r.sendback _) + + private val active_areas = + List((highlight_area, true), (hyperlink_area, true), (sendback_area, false)) + private def active_reset(): Unit = active_areas.foreach(_._1.reset) private val focus_listener = new FocusAdapter { override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } } @@ -139,7 +146,11 @@ override def mouseClicked(e: MouseEvent) { robust_body(()) { hyperlink_area.info match { - case Some(Text.Info(range, link)) => link.follow(view) + case Some(Text.Info(_, link)) => link.follow(view) + case None => + } + sendback_area.info match { + case Some(Text.Info(_, sendback)) => sendback.activate(view) case None => } } @@ -150,12 +161,18 @@ override def mouseMoved(e: MouseEvent) { robust_body(()) { control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown - if (control && !buffer.isLoading) { + + if ((control || hovering) && !buffer.isLoading) { JEdit_Lib.buffer_lock(buffer) { val rendering = get_rendering() val mouse_offset = text_area.xyToOffset(e.getX(), e.getY()) val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset) - active_areas.foreach(_.update_rendering(rendering, mouse_range)) + for ((area, require_control) <- active_areas) + { + if (control == require_control) + area.update_rendering(rendering, mouse_range) + else area.reset + } } } else active_reset() @@ -215,6 +232,16 @@ gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } + // sendback range -- potentially from other snapshot + for { + info <- sendback_area.info + Text.Info(range, _) <- info.try_restrict(line_range) + r <- JEdit_Lib.gfx_range(text_area, range) + } { + gfx.setColor(rendering.sendback_active_color) + gfx.fillRect(r.x, y + i * line_height, r.length, line_height) + } + // background color (2) for { Text.Info(range, color) <- rendering.background2(line_range) diff -r 6b48c76f5b3f -r 2e3e7ea5ce8e src/Tools/jEdit/src/sendback.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/sendback.scala Fri Sep 21 15:39:51 2012 +0200 @@ -0,0 +1,49 @@ +/* Title: Tools/jEdit/src/sendback.scala + Author: Makarius + +Clickable "sendback" areas within the source text. +*/ + +package isabelle.jedit + + +import isabelle._ + +import org.gjt.sp.jedit.{View, jEdit} +import org.gjt.sp.jedit.textarea.JEditTextArea + + +object Sendback +{ + def apply(command: Command, body: XML.Body): Sendback = new Sendback(command, body) +} + +class Sendback private(command: Command, body: XML.Body) +{ + def activate(view: View) + { + Swing_Thread.require() + + Document_View(view.getTextArea) match { + case Some(doc_view) => + doc_view.rich_text_area.robust_body() { + val model = doc_view.model + val buffer = model.buffer + val snapshot = model.snapshot() + snapshot.node.command_start(command) match { + case Some(start) if !snapshot.is_outdated => + val text = Pretty.string_of(body) + try { + buffer.beginCompoundEdit() + buffer.remove(start, command.proper_range.length) + buffer.insert(start, text) + } + finally { buffer.endCompoundEdit() } + case _ => + } + } + case None => + } + } +} +