equal
deleted
inserted
replaced
55 } |
55 } |
56 |
56 |
57 |
57 |
58 /* update */ |
58 /* update */ |
59 |
59 |
|
60 private var do_update = true |
|
61 |
|
62 private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() } |
|
63 |
60 def update() |
64 def update() |
61 { |
65 { |
62 GUI_Thread.require {} |
66 GUI_Thread.require {} |
63 |
67 |
64 PIDE.document_model(view.getBuffer).map(_.snapshot()) match { |
68 PIDE.document_model(view.getBuffer).map(_.snapshot()) match { |
72 } |
76 } |
73 |
77 |
74 |
78 |
75 /* controls */ |
79 /* controls */ |
76 |
80 |
|
81 private val auto_update_button = new CheckBox("Auto update") { |
|
82 tooltip = "Indicate automatic update following cursor movement" |
|
83 reactions += { case ButtonClicked(_) => do_update = this.selected; maybe_update() } |
|
84 selected = do_update |
|
85 } |
|
86 |
77 private val update_button = new Button("<html><b>Update</b></html>") { |
87 private val update_button = new Button("<html><b>Update</b></html>") { |
78 tooltip = "Update display according to the command at cursor position" |
88 tooltip = "Update display according to the command at cursor position" |
79 reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) } |
89 reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) } |
80 } |
90 } |
81 |
91 |
85 } |
95 } |
86 |
96 |
87 private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } |
97 private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } |
88 |
98 |
89 private val controls = |
99 private val controls = |
90 new Wrap_Panel(Wrap_Panel.Alignment.Right)(update_button, locate_button, |
100 new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update_button, update_button, |
91 pretty_text_area.search_label, pretty_text_area.search_field, zoom) |
101 locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom) |
92 add(controls.peer, BorderLayout.NORTH) |
102 add(controls.peer, BorderLayout.NORTH) |
93 |
103 |
94 override def focusOnDefaultComponent { update_button.requestFocus } |
104 override def focusOnDefaultComponent { update_button.requestFocus } |
95 |
105 |
96 |
106 |
98 |
108 |
99 private val main = |
109 private val main = |
100 Session.Consumer[Any](getClass.getName) { |
110 Session.Consumer[Any](getClass.getName) { |
101 case _: Session.Global_Options => |
111 case _: Session.Global_Options => |
102 GUI_Thread.later { handle_resize() } |
112 GUI_Thread.later { handle_resize() } |
|
113 |
|
114 case changed: Session.Commands_Changed => |
|
115 if (changed.assignment) GUI_Thread.later { maybe_update() } |
|
116 |
|
117 case Session.Caret_Focus => |
|
118 GUI_Thread.later { maybe_update() } |
103 } |
119 } |
104 |
120 |
105 override def init() |
121 override def init() |
106 { |
122 { |
107 PIDE.session.global_options += main |
123 PIDE.session.global_options += main |
|
124 PIDE.session.commands_changed += main |
|
125 PIDE.session.caret_focus += main |
108 handle_resize() |
126 handle_resize() |
109 print_state.activate() |
127 print_state.activate() |
|
128 maybe_update() |
110 } |
129 } |
111 |
130 |
112 override def exit() |
131 override def exit() |
113 { |
132 { |
114 print_state.deactivate() |
133 print_state.deactivate() |
|
134 PIDE.session.caret_focus -= main |
115 PIDE.session.global_options -= main |
135 PIDE.session.global_options -= main |
|
136 PIDE.session.commands_changed -= main |
116 delay_resize.revoke() |
137 delay_resize.revoke() |
117 } |
138 } |
118 } |
139 } |