--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 21 14:53:19 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 21 15:29:20 2010 +0200
@@ -28,15 +28,45 @@
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
- val controls = new FlowPanel(FlowPanel.Alignment.Right)()
- add(controls.peer, BorderLayout.NORTH)
-
val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
add(html_panel, BorderLayout.CENTER)
/* controls */
+ private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
+ zoom.tooltip = "Zoom factor for basic font size"
+
+ private val update = new Button("Update") {
+ reactions += { case ButtonClicked(_) => handle_update() }
+ }
+ update.tooltip = "Update display according to state of command at caret position"
+
+ private val tracing = new CheckBox("Tracing") {
+ reactions += { case ButtonClicked(_) => handle_update() }
+ }
+ tracing.tooltip = "Indicate output of tracing messages"
+
+ private val debug = new CheckBox("Debug") {
+ reactions += { case ButtonClicked(_) => handle_update() }
+ }
+ debug.tooltip = "Indicate output of debug messages (usually disabled on the prover side)"
+
+ private val follow = new CheckBox("Follow")
+ follow.selected = true
+ follow.tooltip = "Indicate automatic update according to caret movement or state changes"
+
+ private def filtered_results(document: Document, cmd: Command): List[XML.Tree] =
+ {
+ val show_tracing = tracing.selected
+ val show_debug = debug.selected
+ document.current_state(cmd).results filter {
+ case Output.Message(Markup.TRACING, _, _) => show_tracing
+ case Output.Message(Markup.DEBUG, _, _) => show_debug
+ case _ => true
+ }
+ }
+
private case class Render(body: List[XML.Tree])
private def handle_update()
@@ -47,7 +77,7 @@
val document = model.recent_document
document.command_at(view.getTextArea.getCaretPosition) match {
case Some((cmd, _)) =>
- output_actor ! Render(document.current_state(cmd).results)
+ output_actor ! Render(filtered_results(document, cmd))
case None =>
}
case None =>
@@ -62,18 +92,6 @@
html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
}
- private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
- zoom.tooltip = "Zoom factor for basic font size"
-
- private val update = new Button("Update") {
- reactions += { case ButtonClicked(_) => handle_update() }
- }
- update.tooltip = "Update display according to state of command at caret position"
-
- private val follow = new CheckBox("Follow")
- follow.tooltip = "Indicate automatic update according to caret movement or state changes"
- follow.selected = true
-
/* actor wiring */
@@ -88,7 +106,8 @@
if (follow.selected) Document_Model(view.getBuffer) else None
} match {
case None =>
- case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results)
+ case Some(model) =>
+ html_panel.render(filtered_results(model.recent_document, cmd))
}
case bad => System.err.println("output_actor: ignoring bad message " + bad)
@@ -121,6 +140,8 @@
/* init controls */
- controls.contents ++= List(zoom, update, follow)
+ val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, update, debug, tracing, follow)
+ add(controls.peer, BorderLayout.NORTH)
+
handle_update()
}