equal
deleted
inserted
replaced
89 private def output_state_=(b: Boolean) |
89 private def output_state_=(b: Boolean) |
90 { |
90 { |
91 if (output_state != b) { |
91 if (output_state != b) { |
92 PIDE.options.bool("editor_output_state") = b |
92 PIDE.options.bool("editor_output_state") = b |
93 PIDE.session.update_options(PIDE.options.value) |
93 PIDE.session.update_options(PIDE.options.value) |
|
94 PIDE.editor.flush(hidden = true) |
|
95 PIDE.editor.flush() |
94 } |
96 } |
95 } |
97 } |
96 |
98 |
97 private val output_state_button = new CheckBox("Output state") |
99 private val output_state_button = new CheckBox("Proof state") |
98 { |
100 { |
99 tooltip = "Implicit output of proof state" |
101 tooltip = "Output of proof state (normally shown on State panel)" |
100 reactions += { case ButtonClicked(_) => output_state = selected } |
102 reactions += { case ButtonClicked(_) => output_state = selected } |
101 selected = output_state |
103 selected = output_state |
102 } |
104 } |
103 |
105 |
104 private val auto_update_button = new CheckBox("Auto update") { |
106 private val auto_update_button = new CheckBox("Auto update") { |