# HG changeset patch # User wenzelm # Date 1348241333 -7200 # Node ID cbcccf2a0f6fd9c2ba0d32d3aed6b8826f87675b # Parent db58490a68acb7f97f186c15ed6e24bac7a35dee renamed Output to Output1 and Output2 to Output, and thus make the new version the default; diff -r db58490a68ac -r cbcccf2a0f6f src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 21 16:50:44 2012 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Sep 21 17:28:53 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" diff -r db58490a68ac -r cbcccf2a0f6f src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Fri Sep 21 16:50:44 2012 +0200 +++ b/src/Tools/jEdit/src/Isabelle.props Fri Sep 21 17:28:53 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 db58490a68ac -r cbcccf2a0f6f src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Fri Sep 21 16:50:44 2012 +0200 +++ b/src/Tools/jEdit/src/actions.xml Fri Sep 21 17:28:53 2012 +0200 @@ -22,9 +22,9 @@ wm.addDockableWindow("isabelle-output"); - + - wm.addDockableWindow("isabelle-output2"); + wm.addDockableWindow("isabelle-output1"); diff -r db58490a68ac -r cbcccf2a0f6f src/Tools/jEdit/src/dockables.xml --- a/src/Tools/jEdit/src/dockables.xml Fri Sep 21 16:50:44 2012 +0200 +++ b/src/Tools/jEdit/src/dockables.xml Fri Sep 21 17:28:53 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 db58490a68ac -r cbcccf2a0f6f 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:28:53 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 db58490a68ac -r cbcccf2a0f6f src/Tools/jEdit/src/output2_dockable.scala --- a/src/Tools/jEdit/src/output2_dockable.scala Fri Sep 21 16:50:44 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 db58490a68ac -r cbcccf2a0f6f src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Fri Sep 21 16:50:44 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri Sep 21 17:28:53 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 }