29 |
29 |
30 |
30 |
31 /* component state -- owned by Swing thread */ |
31 /* component state -- owned by Swing thread */ |
32 |
32 |
33 private var zoom_factor = 100 |
33 private var zoom_factor = 100 |
|
34 private var show_debug = false |
|
35 private var show_tracing = false |
|
36 private var follow_caret = true |
|
37 private var current_command: Option[Command] = None |
34 |
38 |
35 private def handle_resize() = |
39 |
|
40 private def handle_resize() |
|
41 { |
36 Swing_Thread.now { |
42 Swing_Thread.now { |
37 html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100)) |
43 html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100)) |
38 } |
44 } |
|
45 } |
39 |
46 |
40 |
47 private def handle_caret() |
41 private var current_command: Option[Command] = None |
48 { |
42 private var follow_caret = true |
49 Swing_Thread.now { |
43 private var show_debug = false |
50 Document_View(view.getTextArea) match { |
44 private var show_tracing = false |
51 case Some(doc_view) => current_command = doc_view.selected_command |
|
52 case None => |
|
53 } |
|
54 } |
|
55 } |
45 |
56 |
46 private def handle_update(restriction: Option[Set[Command]] = None) |
57 private def handle_update(restriction: Option[Set[Command]] = None) |
47 { |
58 { |
48 Swing_Thread.now { |
59 Swing_Thread.now { |
|
60 if (follow_caret) handle_caret() |
49 Document_View(view.getTextArea) match { |
61 Document_View(view.getTextArea) match { |
50 case Some(doc_view) => |
62 case Some(doc_view) => |
51 if (follow_caret) current_command = doc_view.selected_command |
|
52 current_command match { |
63 current_command match { |
53 case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
64 case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => |
54 val document = doc_view.model.recent_document |
65 val document = doc_view.model.recent_document |
55 val filtered_results = |
66 val filtered_results = |
56 document.current_state(cmd).results filter { |
67 document.current_state(cmd).results filter { |
103 /* controls */ |
114 /* controls */ |
104 |
115 |
105 private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
116 private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) |
106 zoom.tooltip = "Zoom factor for basic font size" |
117 zoom.tooltip = "Zoom factor for basic font size" |
107 |
118 |
108 private val update = new Button("Update") { |
119 private val debug = new CheckBox("Debug") { |
109 reactions += { case ButtonClicked(_) => handle_update() } |
120 reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() } |
110 } |
121 } |
111 update.tooltip = |
122 debug.selected = show_debug |
112 "<html>Update display according to the<br>state of command at caret position</html>" |
123 debug.tooltip = |
|
124 "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>" |
113 |
125 |
114 private val tracing = new CheckBox("Tracing") { |
126 private val tracing = new CheckBox("Tracing") { |
115 reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
127 reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } |
116 } |
128 } |
117 tracing.selected = show_tracing |
129 tracing.selected = show_tracing |
118 tracing.tooltip = |
130 tracing.tooltip = |
119 "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>" |
131 "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>" |
120 |
132 |
121 private val debug = new CheckBox("Debug") { |
133 private val auto_update = new CheckBox("Auto update") { |
122 reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() } |
|
123 } |
|
124 debug.selected = show_debug |
|
125 debug.tooltip = |
|
126 "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>" |
|
127 |
|
128 private val follow = new CheckBox("Follow") { |
|
129 reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } |
134 reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } |
130 } |
135 } |
131 follow.selected = follow_caret |
136 auto_update.selected = follow_caret |
132 follow.tooltip = "<html>Indicate automatic update following cursor movement</html>" |
137 auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>" |
133 |
138 |
134 val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, update, debug, tracing, follow) |
139 private val update = new Button("Update") { |
|
140 reactions += { case ButtonClicked(_) => handle_caret(); handle_update() } |
|
141 } |
|
142 update.tooltip = "<html>Update display according to the command at cursor position</html>" |
|
143 |
|
144 val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update) |
135 add(controls.peer, BorderLayout.NORTH) |
145 add(controls.peer, BorderLayout.NORTH) |
136 |
146 |
137 handle_update() |
147 handle_update() |
138 } |
148 } |