diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 14:18:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 15:20:31 +0100 |
| commit | 2acc6327e4d8a05898b75cb3abb47b7941ec420a (patch) | |
| tree | d1f7a8f4cfa5cfef1521b970dadc586819f3b555 /ide/nanoPG.ml | |
| parent | 6736fb9db77be8a6f207b95ae0d5f7b3a843dc89 (diff) | |
Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE buffer.
Diffstat (limited to 'ide/nanoPG.ml')
| -rw-r--r-- | ide/nanoPG.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index c6ac56992..671d85a17 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -294,8 +294,12 @@ let init w nb ags = let status = ref empty in let reset () = eprintf "reset\n%!"; cur := pg in ignore(w#event#connect#key_press ~callback:(fun t -> - if nb#current_term.script#misc#get_property "has-focus" <> - `BOOL true + let on_current_term f = + let term = try Some nb#current_term with Invalid_argument _ -> None in + match term with None -> false | Some t -> f t + in + on_current_term (fun x -> + if x.script#misc#get_property "has-focus" <> `BOOL true then false else begin eprintf "got key %s\n%!" (pr_key t); @@ -309,7 +313,7 @@ let init w nb ags = cur := c; true | `NotFound -> reset (); false end else false - end)); + end))); ignore(w#event#connect#button_press ~callback:(fun t -> reset (); false)) |