equal
deleted
inserted
replaced
75 private def output_state_=(b: Boolean) |
75 private def output_state_=(b: Boolean) |
76 { |
76 { |
77 if (output_state != b) { |
77 if (output_state != b) { |
78 PIDE.options.bool("editor_output_state") = b |
78 PIDE.options.bool("editor_output_state") = b |
79 PIDE.session.update_options(PIDE.options.value) |
79 PIDE.session.update_options(PIDE.options.value) |
80 PIDE.editor.flush(hidden = true) |
80 PIDE.editor.flush_edits(hidden = true) |
81 PIDE.editor.flush() |
81 PIDE.editor.flush() |
82 } |
82 } |
83 } |
83 } |
84 |
84 |
85 private val output_state_button = new CheckBox("Proof state") |
85 private val output_state_button = new CheckBox("Proof state") |