equal
deleted
inserted
replaced
30 |
30 |
31 |
31 |
32 /* component state -- owned by Swing thread */ |
32 /* component state -- owned by Swing thread */ |
33 |
33 |
34 private var zoom_factor = 100 |
34 private var zoom_factor = 100 |
35 private var show_debug = false |
|
36 private var show_tracing = false |
35 private var show_tracing = false |
37 private var follow_caret = true |
36 private var follow_caret = true |
38 private var current_command: Option[Command] = None |
37 private var current_command: Option[Command] = None |
39 |
38 |
40 |
39 |
66 current_command match { |
65 current_command match { |
67 case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
66 case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
68 val snapshot = doc_view.model.snapshot() |
67 val snapshot = doc_view.model.snapshot() |
69 val filtered_results = |
68 val filtered_results = |
70 snapshot.state(cmd).results.iterator.map(_._2) filter { |
69 snapshot.state(cmd).results.iterator.map(_._2) filter { |
71 case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing |
70 case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable |
72 case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug |
|
73 case _ => true |
71 case _ => true |
74 } |
72 } |
75 html_panel.render(filtered_results.toList) |
73 html_panel.render(filtered_results.toList) |
76 case _ => |
74 case _ => |
77 } |
75 } |
120 /* controls */ |
118 /* controls */ |
121 |
119 |
122 private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
120 private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
123 zoom.tooltip = "Zoom factor for basic font size" |
121 zoom.tooltip = "Zoom factor for basic font size" |
124 |
122 |
125 private val debug = new CheckBox("Debug") { |
|
126 reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() } |
|
127 } |
|
128 debug.selected = show_debug |
|
129 debug.tooltip = |
|
130 "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>" |
|
131 |
|
132 private val tracing = new CheckBox("Tracing") { |
123 private val tracing = new CheckBox("Tracing") { |
133 reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
124 reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
134 } |
125 } |
135 tracing.selected = show_tracing |
126 tracing.selected = show_tracing |
136 tracing.tooltip = "Indicate output of tracing messages" |
127 tracing.tooltip = "Indicate output of tracing messages" |
144 private val update = new Button("Update") { |
135 private val update = new Button("Update") { |
145 reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() } |
136 reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() } |
146 } |
137 } |
147 update.tooltip = "Update display according to the command at cursor position" |
138 update.tooltip = "Update display according to the command at cursor position" |
148 |
139 |
149 val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update) |
140 val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) |
150 add(controls.peer, BorderLayout.NORTH) |
141 add(controls.peer, BorderLayout.NORTH) |
151 |
142 |
152 handle_update() |
143 handle_update() |
153 } |
144 } |