--- a/src/Pure/General/pretty.scala Fri Jun 11 13:25:28 2010 +0200
+++ b/src/Pure/General/pretty.scala Mon Jun 14 21:10:15 2010 +0200
@@ -134,7 +134,7 @@
def string_of(input: List[XML.Tree], margin: Int = margin_default,
metric: String => Double = metric_default): String =
- formatted(input).iterator.flatMap(XML.content).mkString
+ formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
/* unformatted output */
--- a/src/Pure/PIDE/command.scala Fri Jun 11 13:25:28 2010 +0200
+++ b/src/Pure/PIDE/command.scala Mon Jun 14 21:10:15 2010 +0200
@@ -48,8 +48,7 @@
def name: String = if (is_command) span.head.content else ""
override def toString =
- if (is_command) name + "(" + id + ")"
- else if (is_ignored) "<ignored>" else "<malformed>"
+ id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
/* source text */
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Fri Jun 11 13:25:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jun 14 21:10:15 2010 +0200
@@ -129,19 +129,18 @@
reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
}
tracing.selected = show_tracing
- tracing.tooltip =
- "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
+ tracing.tooltip = "Indicate output of tracing messages"
private val auto_update = new CheckBox("Auto update") {
reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
}
auto_update.selected = follow_caret
- auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>"
+ auto_update.tooltip = "Indicate automatic update following cursor movement"
private val update = new Button("Update") {
reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
}
- update.tooltip = "<html>Update display according to the command at cursor position</html>"
+ update.tooltip = "Update display according to the command at cursor position"
val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
add(controls.peer, BorderLayout.NORTH)