some support for hovering and sendback area;
authorwenzelm
Fri Sep 21 15:39:51 2012 +0200 (2012-09-21)
changeset 494922e3e7ea5ce8e
parent 49491 6b48c76f5b3f
child 49493 db58490a68ac
some support for hovering and sendback area;
src/Tools/jEdit/etc/options
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/sendback.scala
     1.1 --- a/src/Tools/jEdit/etc/options	Fri Sep 21 12:07:59 2012 +0200
     1.2 +++ b/src/Tools/jEdit/etc/options	Fri Sep 21 15:39:51 2012 +0200
     1.3 @@ -40,6 +40,8 @@
     1.4  option quoted_color : string = "8B8B8B19"
     1.5  option highlight_color : string = "50505032"
     1.6  option hyperlink_color : string = "000000FF"
     1.7 +option sendback_color : string = "DCDCDCFF"
     1.8 +option sendback_active_color : string = "9DC75DFF"
     1.9  option keyword1_color : string = "006699FF"
    1.10  option keyword2_color : string = "009966FF"
    1.11  
     2.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 21 12:07:59 2012 +0200
     2.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 21 15:39:51 2012 +0200
     2.3 @@ -30,6 +30,7 @@
     2.4    "src/readme_dockable.scala"
     2.5    "src/rich_text_area.scala"
     2.6    "src/scala_console.scala"
     2.7 +  "src/sendback.scala"
     2.8    "src/session_dockable.scala"
     2.9    "src/syslog_dockable.scala"
    2.10    "src/text_overview.scala"
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Sep 21 12:07:59 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Sep 21 15:39:51 2012 +0200
     3.3 @@ -70,7 +70,7 @@
     3.4    def get_rendering(): Isabelle_Rendering =
     3.5      Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
     3.6  
     3.7 -  val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _)
     3.8 +  val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false)
     3.9  
    3.10  
    3.11    /* perspective */
     4.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 21 12:07:59 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 21 15:39:51 2012 +0200
     4.3 @@ -125,6 +125,8 @@
     4.4    val quoted_color = color_value("quoted_color")
     4.5    val highlight_color = color_value("highlight_color")
     4.6    val hyperlink_color = color_value("hyperlink_color")
     4.7 +  val sendback_color = color_value("sendback_color")
     4.8 +  val sendback_active_color = color_value("sendback_active_color")
     4.9    val keyword1_color = color_value("keyword1_color")
    4.10    val keyword2_color = color_value("keyword2_color")
    4.11  
    4.12 @@ -237,6 +239,22 @@
    4.13    }
    4.14  
    4.15  
    4.16 +  def sendback(range: Text.Range): Option[Text.Info[Sendback]] =
    4.17 +  {
    4.18 +    snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)),
    4.19 +        {
    4.20 +          case Text.Info(info_range, Protocol.Sendback(body)) =>
    4.21 +            Text.Info(snapshot.convert(info_range), body)
    4.22 +        }) match
    4.23 +    {
    4.24 +      case Text.Info(_, Text.Info(range, body)) #:: _ =>
    4.25 +        snapshot.node.command_at(range.start)
    4.26 +          .map(command_range => Text.Info(range, Sendback(command_range._1, body)))
    4.27 +      case _ => None
    4.28 +    }
    4.29 +  }
    4.30 +
    4.31 +
    4.32    private def tooltip_text(msg: XML.Tree): String =
    4.33      Pretty.string_of(List(msg), margin = options.int("jedit_tooltip_margin"))
    4.34  
    4.35 @@ -388,6 +406,13 @@
    4.36      message_colors.get(pri).map((_, is_separator))
    4.37    }
    4.38  
    4.39 +
    4.40 +  private val background1_include =
    4.41 +    Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
    4.42 +      Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
    4.43 +      Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY +
    4.44 +      Isabelle_Markup.SENDBACK
    4.45 +
    4.46    def background1(range: Text.Range): Stream[Text.Info[Color]] =
    4.47    {
    4.48      if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
    4.49 @@ -395,10 +420,7 @@
    4.50        for {
    4.51          Text.Info(r, result) <-
    4.52            snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
    4.53 -            range, (Some(Protocol.Status.init), None),
    4.54 -            Some(Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
    4.55 -              Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
    4.56 -              Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
    4.57 +            range, (Some(Protocol.Status.init), None), Some(background1_include),
    4.58              {
    4.59                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
    4.60                if (Protocol.command_status_markup(markup.name)) =>
    4.61 @@ -407,6 +429,8 @@
    4.62                  (None, Some(bad_color))
    4.63                case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
    4.64                  (None, Some(intensify_color))
    4.65 +              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) =>
    4.66 +                (None, Some(sendback_color))
    4.67              })
    4.68          color <-
    4.69            (result match {
     5.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Sep 21 12:07:59 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Sep 21 15:39:51 2012 +0200
     5.3 @@ -67,7 +67,7 @@
     5.4      Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
     5.5    private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
     5.6  
     5.7 -  private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
     5.8 +  private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering, true)
     5.9  
    5.10    def refresh()
    5.11    {
     6.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Sep 21 12:07:59 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Sep 21 15:39:51 2012 +0200
     6.3 @@ -23,7 +23,11 @@
     6.4  import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
     6.5  
     6.6  
     6.7 -class Rich_Text_Area(view: View, text_area: TextArea, get_rendering: () => Isabelle_Rendering)
     6.8 +class Rich_Text_Area(
     6.9 +  view: View,
    6.10 +  text_area: TextArea,
    6.11 +  get_rendering: () => Isabelle_Rendering,
    6.12 +  hovering: Boolean)
    6.13  {
    6.14    private val buffer = text_area.getBuffer
    6.15  
    6.16 @@ -123,8 +127,11 @@
    6.17  
    6.18    private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
    6.19    private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
    6.20 -  private val active_areas = List(highlight_area, hyperlink_area)
    6.21 -  private def active_reset(): Unit = active_areas.foreach(_.reset)
    6.22 +  private val sendback_area = new Active_Area[Sendback]((r: Isabelle_Rendering) => r.sendback _)
    6.23 +
    6.24 +  private val active_areas =
    6.25 +    List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
    6.26 +  private def active_reset(): Unit = active_areas.foreach(_._1.reset)
    6.27  
    6.28    private val focus_listener = new FocusAdapter {
    6.29      override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
    6.30 @@ -139,7 +146,11 @@
    6.31      override def mouseClicked(e: MouseEvent) {
    6.32        robust_body(()) {
    6.33          hyperlink_area.info match {
    6.34 -          case Some(Text.Info(range, link)) => link.follow(view)
    6.35 +          case Some(Text.Info(_, link)) => link.follow(view)
    6.36 +          case None =>
    6.37 +        }
    6.38 +        sendback_area.info match {
    6.39 +          case Some(Text.Info(_, sendback)) => sendback.activate(view)
    6.40            case None =>
    6.41          }
    6.42        }
    6.43 @@ -150,12 +161,18 @@
    6.44      override def mouseMoved(e: MouseEvent) {
    6.45        robust_body(()) {
    6.46          control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
    6.47 -        if (control && !buffer.isLoading) {
    6.48 +
    6.49 +        if ((control || hovering) && !buffer.isLoading) {
    6.50            JEdit_Lib.buffer_lock(buffer) {
    6.51              val rendering = get_rendering()
    6.52              val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
    6.53              val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
    6.54 -            active_areas.foreach(_.update_rendering(rendering, mouse_range))
    6.55 +            for ((area, require_control) <- active_areas)
    6.56 +            {
    6.57 +              if (control == require_control)
    6.58 +                area.update_rendering(rendering, mouse_range)
    6.59 +              else area.reset
    6.60 +            }
    6.61            }
    6.62          }
    6.63          else active_reset()
    6.64 @@ -215,6 +232,16 @@
    6.65                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    6.66              }
    6.67  
    6.68 +            // sendback range -- potentially from other snapshot
    6.69 +            for {
    6.70 +              info <- sendback_area.info
    6.71 +              Text.Info(range, _) <- info.try_restrict(line_range)
    6.72 +              r <- JEdit_Lib.gfx_range(text_area, range)
    6.73 +            } {
    6.74 +              gfx.setColor(rendering.sendback_active_color)
    6.75 +              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    6.76 +            }
    6.77 +
    6.78              // background color (2)
    6.79              for {
    6.80                Text.Info(range, color) <- rendering.background2(line_range)
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/jEdit/src/sendback.scala	Fri Sep 21 15:39:51 2012 +0200
     7.3 @@ -0,0 +1,49 @@
     7.4 +/*  Title:      Tools/jEdit/src/sendback.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Clickable "sendback" areas within the source text.
     7.8 +*/
     7.9 +
    7.10 +package isabelle.jedit
    7.11 +
    7.12 +
    7.13 +import isabelle._
    7.14 +
    7.15 +import org.gjt.sp.jedit.{View, jEdit}
    7.16 +import org.gjt.sp.jedit.textarea.JEditTextArea
    7.17 +
    7.18 +
    7.19 +object Sendback
    7.20 +{
    7.21 +  def apply(command: Command, body: XML.Body): Sendback = new Sendback(command, body)
    7.22 +}
    7.23 +
    7.24 +class Sendback private(command: Command, body: XML.Body)
    7.25 +{
    7.26 +  def activate(view: View)
    7.27 +  {
    7.28 +    Swing_Thread.require()
    7.29 +
    7.30 +    Document_View(view.getTextArea) match {
    7.31 +      case Some(doc_view) =>
    7.32 +        doc_view.rich_text_area.robust_body() {
    7.33 +          val model = doc_view.model
    7.34 +          val buffer = model.buffer
    7.35 +          val snapshot = model.snapshot()
    7.36 +          snapshot.node.command_start(command) match {
    7.37 +            case Some(start) if !snapshot.is_outdated =>
    7.38 +              val text = Pretty.string_of(body)
    7.39 +              try {
    7.40 +                buffer.beginCompoundEdit()
    7.41 +                buffer.remove(start, command.proper_range.length)
    7.42 +                buffer.insert(start, text)
    7.43 +              }
    7.44 +              finally { buffer.endCompoundEdit() }
    7.45 +            case _ =>
    7.46 +          }
    7.47 +        }
    7.48 +      case None =>
    7.49 +    }
    7.50 +  }
    7.51 +}
    7.52 +