# HG changeset patch # User wenzelm # Date 1348242089 -7200 # Node ID 796b3139f5a8ef3ad1bbbf2bf63aa85cc6ceb41b # Parent 82d99fe04018b369e46e5b0610aa5bb655455f32# Parent cbcccf2a0f6fd9c2ba0d32d3aed6b8826f87675b merged diff -r 82d99fe04018 -r 796b3139f5a8 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Pure/PIDE/command.scala Fri Sep 21 17:41:29 2012 +0200 @@ -60,16 +60,15 @@ case XML.Elem(Markup(name, atts), body) => atts match { case Isabelle_Markup.Serial(i) => - val props = Position.purge(atts) - val result = XML.Elem(Markup(name, props), body) - val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body) + val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), atts), body) + val message2 = XML.Elem(Markup(name, Position.purge(atts)), body) - val st0 = copy(results = results + (i -> result_message)) + val st0 = copy(results = results + (i -> message1)) val st1 = - if (Protocol.is_tracing(result)) st0 + if (Protocol.is_tracing(message)) st0 else (st0 /: Protocol.message_positions(command, message))( - (st, range) => st.add_markup(Text.Info(range, result))) + (st, range) => st.add_markup(Text.Info(range, message2))) st1 case _ => System.err.println("Ignored message without serial number: " + message); this diff -r 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/etc/options Fri Sep 21 17:41:29 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 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Sep 21 17:41:29 2012 +0200 @@ -22,7 +22,7 @@ "src/jedit_thy_load.scala" "src/jedit_options.scala" "src/output_dockable.scala" - "src/output2_dockable.scala" + "src/output1_dockable.scala" "src/plugin.scala" "src/pretty_text_area.scala" "src/protocol_dockable.scala" @@ -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 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/src/Isabelle.props Fri Sep 21 17:41:29 2012 +0200 @@ -40,10 +40,10 @@ #menu actions plugin.isabelle.jedit.Plugin.menu.label=Isabelle -plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.output2-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel +plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.output1-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel isabelle.session-panel.label=Prover Session panel isabelle.output-panel.label=Output panel -isabelle.output2-panel.label=Output2 panel +isabelle.output1-panel.label=Output1 panel isabelle.raw-output-panel.label=Raw Output panel isabelle.protocol-panel.label=Protocol panel isabelle.readme-panel.label=README panel @@ -52,7 +52,7 @@ #dockables isabelle-session.title=Prover Session isabelle-output.title=Output -isabelle-output2.title=Output2 +isabelle-output1.title=Output1 isabelle-raw-output.title=Raw Output isabelle-protocol.title=Protocol isabelle-readme.title=README diff -r 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/src/actions.xml Fri Sep 21 17:41:29 2012 +0200 @@ -22,9 +22,9 @@ wm.addDockableWindow("isabelle-output"); - + - wm.addDockableWindow("isabelle-output2"); + wm.addDockableWindow("isabelle-output1"); diff -r 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/dockables.xml --- a/src/Tools/jEdit/src/dockables.xml Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/src/dockables.xml Fri Sep 21 17:41:29 2012 +0200 @@ -14,8 +14,8 @@ new isabelle.jedit.Output_Dockable(view, position); - - new isabelle.jedit.Output2_Dockable(view, position); + + new isabelle.jedit.Output1_Dockable(view, position); new isabelle.jedit.Raw_Output_Dockable(view, position); diff -r 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 21 17:41:29 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 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 21 17:41:29 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,26 @@ } + def sendback(range: Text.Range): Option[Text.Info[Document.Exec_ID]] = + { + val results = + snapshot.cumulate_markup[(Option[Document.Exec_ID], Option[Text.Range])](range, + (None, None), Some(messages_include + Isabelle_Markup.SENDBACK), + { + case ((_, info), Text.Info(_, XML.Elem(Markup(name, Position.Id(id)), _))) + if messages_include(name) => (Some(id), info) + + case ((id, _), Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) => + (id, Some(snapshot.convert(info_range))) + }) + + (for (Text.Info(_, (Some(id), Some(r))) <- results) yield Text.Info(r, id)) match { + case res #:: _ => Some(res) + case _ => None + } + } + + private def tooltip_text(msg: XML.Tree): String = Pretty.string_of(List(msg), margin = options.int("jedit_tooltip_margin")) @@ -357,6 +379,10 @@ } + private val messages_include = + Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE, + Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE) + private val message_colors = Map( Isabelle_Rendering.writeln_pri -> writeln_message_color, Isabelle_Rendering.tracing_pri -> tracing_message_color, @@ -365,11 +391,8 @@ def line_background(range: Text.Range): Option[(Color, Boolean)] = { - val messages = - Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE, - Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE) val results = - snapshot.cumulate_markup[Int](range, 0, Some(messages), + snapshot.cumulate_markup[Int](range, 0, Some(messages_include), { case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) if name == Isabelle_Markup.WRITELN_MESSAGE || @@ -388,6 +411,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 +425,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 +434,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 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/output1_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/output1_dockable.scala Fri Sep 21 17:41:29 2012 +0200 @@ -0,0 +1,188 @@ +/* Title: Tools/jEdit/src/output1_dockable.scala + Author: Makarius + +Dockable window with result message output. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.actors.Actor._ + +import scala.swing.{FlowPanel, Button, CheckBox} +import scala.swing.event.ButtonClicked + +import java.lang.System +import java.awt.BorderLayout +import java.awt.event.{ComponentEvent, ComponentAdapter} + +import org.gjt.sp.jedit.View + + +class Output1_Dockable(view: View, position: String) extends Dockable(view, position) +{ + Swing_Thread.require() + + + /* component state -- owned by Swing thread */ + + private var zoom_factor = 100 + private var show_tracing = false + private var do_update = true + private var current_state = Command.empty.init_state + private var current_body: XML.Body = Nil + + + /* HTML panel */ + + private val html_panel = + new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) + { + override val handler: PartialFunction[HTML_Panel.Event, Unit] = + { + case HTML_Panel.Mouse_Click(elem, event) + if Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).isDefined => + val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get + Document_View(view.getTextArea) match { + case Some(doc_view) => + doc_view.rich_text_area.robust_body() { + val cmd = current_state.command + val model = doc_view.model + val buffer = model.buffer + val snapshot = model.snapshot() + snapshot.node.command_start(cmd) match { + case Some(start) if !snapshot.is_outdated => + val text = Pretty.string_of(sendback) + try { + buffer.beginCompoundEdit() + buffer.remove(start, cmd.proper_range.length) + buffer.insert(start, text) + } + finally { buffer.endCompoundEdit() } + case _ => + } + } + case None => + } + } + } + + set_content(html_panel) + + + private def handle_resize() + { + Swing_Thread.require() + + html_panel.resize(Isabelle.font_family(), + scala.math.round(Isabelle.font_size() * zoom_factor / 100)) + } + + private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) + { + Swing_Thread.require() + + val new_state = + if (follow) { + Document_View(view.getTextArea) match { + case Some(doc_view) => + val snapshot = doc_view.model.snapshot() + snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { + case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) + case None => Command.empty.init_state + } + case None => Command.empty.init_state + } + } + else current_state + + val new_body = + if (!restriction.isDefined || restriction.get.contains(new_state.command)) + new_state.results.iterator.map(_._2) + .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable + else current_body + + if (new_body != current_body) html_panel.render(new_body) + + current_state = new_state + current_body = new_body + } + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case Session.Global_Settings => + Swing_Thread.later { handle_resize() } + case changed: Session.Commands_Changed => + Swing_Thread.later { handle_update(do_update, Some(changed.commands)) } + case Session.Caret_Focus => + Swing_Thread.later { handle_update(do_update, None) } + case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) + } + } + } + + override def init() + { + Swing_Thread.require() + + Isabelle.session.global_settings += main_actor + Isabelle.session.commands_changed += main_actor + Isabelle.session.caret_focus += main_actor + handle_update(true, None) + } + + override def exit() + { + Swing_Thread.require() + + Isabelle.session.global_settings -= main_actor + Isabelle.session.commands_changed -= main_actor + Isabelle.session.caret_focus -= main_actor + delay_resize.revoke() + } + + + /* resize */ + + private val delay_resize = + Swing_Thread.delay_first( + Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() } + + addComponentListener(new ComponentAdapter { + override def componentResized(e: ComponentEvent) { delay_resize.invoke() } + }) + + + /* controls */ + + private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) + zoom.tooltip = "Zoom factor for basic font size" + + private val tracing = new CheckBox("Tracing") { + reactions += { + case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) } + } + tracing.selected = show_tracing + tracing.tooltip = "Indicate output of tracing messages" + + private val auto_update = new CheckBox("Auto update") { + reactions += { + case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) } + } + auto_update.selected = do_update + auto_update.tooltip = "Indicate automatic update following cursor movement" + + private val update = new Button("Update") { + reactions += { case ButtonClicked(_) => handle_update(true, None) } + } + update.tooltip = "Update display according to the command at cursor position" + + private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) + add(controls.peer, BorderLayout.NORTH) +} diff -r 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/output2_dockable.scala --- a/src/Tools/jEdit/src/output2_dockable.scala Fri Sep 21 17:02:23 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,162 +0,0 @@ -/* Title: Tools/jEdit/src/output2_dockable.scala - Author: Makarius - -Dockable window with result message output. -*/ - -package isabelle.jedit - - -import isabelle._ - -import scala.actors.Actor._ - -import scala.swing.{FlowPanel, Button, CheckBox} -import scala.swing.event.ButtonClicked - -import java.lang.System -import java.awt.BorderLayout -import java.awt.event.{ComponentEvent, ComponentAdapter} - -import org.gjt.sp.jedit.View - - -class Output2_Dockable(view: View, position: String) extends Dockable(view, position) -{ - Swing_Thread.require() - - - /* component state -- owned by Swing thread */ - - private var zoom_factor = 100 - private var show_tracing = false - private var do_update = true - private var current_snapshot = Document.State.init.snapshot() - private var current_state = Command.empty.init_state - private var current_output: List[XML.Tree] = Nil - - - /* pretty text panel */ - - private val pretty_text_area = new Pretty_Text_Area(view) - set_content(pretty_text_area) - - - private def handle_resize() - { - Swing_Thread.require() - - pretty_text_area.resize(Isabelle.font_family(), - scala.math.round(Isabelle.font_size() * zoom_factor / 100)) - } - - private def handle_update(follow: Boolean, restriction: Option[Set[Command]]) - { - Swing_Thread.require() - - val (new_snapshot, new_state) = - Document_View(view.getTextArea) match { - case Some(doc_view) => - val snapshot = doc_view.model.snapshot() - if (follow && !snapshot.is_outdated) { - snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { - case Some(cmd) => - (snapshot, snapshot.state.command_state(snapshot.version, cmd)) - case None => - (Document.State.init.snapshot(), Command.empty.init_state) - } - } - else (current_snapshot, current_state) - case None => (current_snapshot, current_state) - } - - val new_output = - if (!restriction.isDefined || restriction.get.contains(new_state.command)) - new_state.results.iterator.map(_._2) - .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable - else current_output - - if (new_output != current_output) - pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output)) - - current_snapshot = new_snapshot - current_state = new_state - current_output = new_output - } - - - /* main actor */ - - private val main_actor = actor { - loop { - react { - case Session.Global_Settings => - Swing_Thread.later { handle_resize() } - case changed: Session.Commands_Changed => - Swing_Thread.later { handle_update(do_update, Some(changed.commands)) } - case Session.Caret_Focus => - Swing_Thread.later { handle_update(do_update, None) } - case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) - } - } - } - - override def init() - { - Swing_Thread.require() - - Isabelle.session.global_settings += main_actor - Isabelle.session.commands_changed += main_actor - Isabelle.session.caret_focus += main_actor - handle_update(true, None) - } - - override def exit() - { - Swing_Thread.require() - - Isabelle.session.global_settings -= main_actor - Isabelle.session.commands_changed -= main_actor - Isabelle.session.caret_focus -= main_actor - delay_resize.revoke() - } - - - /* resize */ - - private val delay_resize = - Swing_Thread.delay_first( - Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() } - - addComponentListener(new ComponentAdapter { - override def componentResized(e: ComponentEvent) { delay_resize.invoke() } - }) - - - /* controls */ - - private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) - zoom.tooltip = "Zoom factor for basic font size" - - private val tracing = new CheckBox("Tracing") { - reactions += { - case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) } - } - tracing.selected = show_tracing - tracing.tooltip = "Indicate output of tracing messages" - - private val auto_update = new CheckBox("Auto update") { - reactions += { - case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) } - } - auto_update.selected = do_update - auto_update.tooltip = "Indicate automatic update following cursor movement" - - private val update = new Button("Update") { - reactions += { case ButtonClicked(_) => handle_update(true, None) } - } - update.tooltip = "Update display according to the command at cursor position" - - private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) - add(controls.peer, BorderLayout.NORTH) -} diff -r 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri Sep 21 17:41:29 2012 +0200 @@ -31,52 +31,22 @@ private var zoom_factor = 100 private var show_tracing = false private var do_update = true + private var current_snapshot = Document.State.init.snapshot() private var current_state = Command.empty.init_state - private var current_body: XML.Body = Nil + private var current_output: List[XML.Tree] = Nil - /* HTML panel */ + /* pretty text panel */ - private val html_panel = - new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) - { - override val handler: PartialFunction[HTML_Panel.Event, Unit] = - { - case HTML_Panel.Mouse_Click(elem, event) - if Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).isDefined => - val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get - Document_View(view.getTextArea) match { - case Some(doc_view) => - doc_view.rich_text_area.robust_body() { - val cmd = current_state.command - val model = doc_view.model - val buffer = model.buffer - val snapshot = model.snapshot() - snapshot.node.command_start(cmd) match { - case Some(start) if !snapshot.is_outdated => - val text = Pretty.string_of(sendback) - try { - buffer.beginCompoundEdit() - buffer.remove(start, cmd.proper_range.length) - buffer.insert(start, text) - } - finally { buffer.endCompoundEdit() } - case _ => - } - } - case None => - } - } - } - - set_content(html_panel) + private val pretty_text_area = new Pretty_Text_Area(view) + set_content(pretty_text_area) private def handle_resize() { Swing_Thread.require() - html_panel.resize(Isabelle.font_family(), + pretty_text_area.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size() * zoom_factor / 100)) } @@ -84,30 +54,34 @@ { Swing_Thread.require() - val new_state = - if (follow) { - Document_View(view.getTextArea) match { - case Some(doc_view) => - val snapshot = doc_view.model.snapshot() + val (new_snapshot, new_state) = + Document_View(view.getTextArea) match { + case Some(doc_view) => + val snapshot = doc_view.model.snapshot() + if (follow && !snapshot.is_outdated) { snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { - case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) - case None => Command.empty.init_state + case Some(cmd) => + (snapshot, snapshot.state.command_state(snapshot.version, cmd)) + case None => + (Document.State.init.snapshot(), Command.empty.init_state) } - case None => Command.empty.init_state - } + } + else (current_snapshot, current_state) + case None => (current_snapshot, current_state) } - else current_state - val new_body = + val new_output = if (!restriction.isDefined || restriction.get.contains(new_state.command)) new_state.results.iterator.map(_._2) .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable - else current_body + else current_output - if (new_body != current_body) html_panel.render(new_body) + if (new_output != current_output) + pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output)) + current_snapshot = new_snapshot current_state = new_state - current_body = new_body + current_output = new_output } diff -r 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Sep 21 17:41:29 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 82d99fe04018 -r 796b3139f5a8 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Fri Sep 21 17:02:23 2012 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Sep 21 17:41:29 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 @@ -97,17 +101,25 @@ private class Active_Area[A]( rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]]) { - private var the_info: Option[Text.Info[A]] = None + private var the_text_info: Option[(String, Text.Info[A])] = None - def info: Option[Text.Info[A]] = the_info + def text_info: Option[(String, Text.Info[A])] = the_text_info + def info: Option[Text.Info[A]] = the_text_info.map(_._2) def update(new_info: Option[Text.Info[A]]) { - val old_info = the_info - if (new_info != old_info) { - for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt } - JEdit_Lib.invalidate_range(text_area, range) - the_info = new_info + val old_text_info = the_text_info + val new_text_info = + new_info.map(info => (text_area.getText(info.range.start, info.range.length), info)) + + if (new_text_info != old_text_info) { + for { + r0 <- JEdit_Lib.visible_range(text_area) + opt <- List(old_text_info, new_text_info) + (_, Text.Info(r1, _)) <- opt + r2 <- r1.try_restrict(r0) // FIXME more precise?! + } JEdit_Lib.invalidate_range(text_area, r2) + the_text_info = new_text_info } } @@ -123,8 +135,12 @@ 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[Document.Exec_ID]((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 +155,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.text_info match { + case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id) case None => } } @@ -150,12 +170,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 +241,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 82d99fe04018 -r 796b3139f5a8 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 17:41:29 2012 +0200 @@ -0,0 +1,47 @@ +/* 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 + + +object Sendback +{ + def activate(view: View, text: String, exec_id: Document.Exec_ID) + { + 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.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 _ => + } + } + case None => + } + } +} +