File tree Expand file tree Collapse file tree 1 file changed +12
-6
lines changed Expand file tree Collapse file tree 1 file changed +12
-6
lines changed Original file line number Diff line number Diff line change @@ -9,6 +9,7 @@ let ui_xml = {|
99< ui>
1010 < popup name= 'PopupMenu '>
1111 < menuitem action= 'export- image' />
12+ < menuitem action= 'reload'/>
1213 < menuitem action= 'viewport- set- start' />
1314 < menuitem action= 'viewport- set- duration' />
1415 < / popup>
@@ -168,15 +169,20 @@ let create ~title tracefile =
168169 ~label: " Set duration..."
169170 ~callback: (fun _a -> show_duration () );
170171
171- window#event#connect#key_press ==> (fun ev ->
172- let keyval = GdkEvent.Key. keyval ev in
173- if keyval = GdkKeysyms. _F5 then (
172+ GAction. add_action " reload" actions
173+ ~label: " Reload"
174+ ~accel: " F5"
175+ ~stock: `REFRESH
176+ ~callback: (fun _a ->
174177 let layout = Layout. load tracefile in
175178 View. set_layout v layout;
176179 set_scollbars () ;
177- redraw () ;
178- true
179- ) else if Minibuffer. is_open minibuffer then (
180+ redraw ()
181+ );
182+
183+ window#event#connect#key_press ==> (fun ev ->
184+ let keyval = GdkEvent.Key. keyval ev in
185+ if Minibuffer. is_open minibuffer then (
180186 if keyval = GdkKeysyms. _Escape then (
181187 Minibuffer. hide minibuffer;
182188 true
You can’t perform that action at this time.
0 commit comments