--- a/src/Tools/jEdit/src/output_dockable.scala Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Dec 13 17:29:23 2012 +0100
@@ -77,7 +77,7 @@
else current_output
if (new_output != current_output)
- pretty_text_area.update(new_snapshot, Pretty.separate(new_output))
+ pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
current_snapshot = new_snapshot
current_state = new_state
@@ -152,7 +152,8 @@
private val detach = new Button("Detach") {
reactions += {
case ButtonClicked(_) =>
- Info_Dockable(view, current_snapshot, Pretty.separate(current_output))
+ Info_Dockable(view, current_snapshot,
+ current_state.results, Pretty.separate(current_output))
}
}
detach.tooltip = "Detach window with static copy of current output"