+var update_history = function() {
+ if (display_lines[0] === null) {
+ $("#history").html("No history");
+ } else if (truncate_display_history) {
+ $("#history").html(print_pv(0, display_lines[0].pretty_pv, 1, 'W', 8, true));
+ } else {
+ $("#history").html(
+ '(<a class="move" href="javascript:collapse_history(true)">collapse</a>) ' +
+ print_pv(0, display_lines[0].pretty_pv, 1, 'W'));
+ }
+}
+
+/**
+ * @param {!boolean} truncate_history
+ */
+var collapse_history = function(truncate_history) {
+ truncate_display_history = truncate_history;
+ update_history();
+}
+window['collapse_history'] = collapse_history;
+