diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 8 | ||||
| -rw-r--r-- | ide/coqide.ml | 8 |
2 files changed, 8 insertions, 8 deletions
@@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: coq.ml 15025 2012-03-09 14:27:07Z glondu $ *) open Vernac open Vernacexpr @@ -112,7 +112,7 @@ let is_in_proof_mode () = | _ -> true let user_error_loc l s = - raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) + raise (Compat.Exc_located (l, Util.UserError ("CoqIde", s))) type printing_state = { mutable printing_implicit : bool; @@ -443,7 +443,7 @@ let interp_and_replace s = let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e - | Stdpp.Exc_located (_,e) -> is_pervasive_exn e + | Compat.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e | _ -> false @@ -456,7 +456,7 @@ let print_toplevel_error exc = in let (loc,exc) = match exc with - | Stdpp.Exc_located (loc, ie) -> (Some loc),ie + | Compat.Exc_located (loc, ie) -> (Some loc),ie | Error_in_file (s, (_,fname, loc), ie) -> None, ie | _ -> dloc,exc in diff --git a/ide/coqide.ml b/ide/coqide.ml index 162728ad..0c99b8a2 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: coqide.ml 15023 2012-03-08 22:35:31Z pboutill $ *) open Preferences open Vernacexpr @@ -1267,14 +1267,14 @@ object(self) | l when List.mem `MOD1 l -> let k = GdkEvent.Key.keyval k in if GdkKeysyms._Return=k - then ignore( + then let _ = if (input_buffer#insert_interactive "\n") then begin let i= self#get_insert#backward_word_start in prerr_endline "active_kp_hf: Placing cursor"; self#process_until_iter_or_error i - end); - true + end in + true else false | l when List.mem `CONTROL l -> let k = GdkEvent.Key.keyval k in if GdkKeysyms._Break=k |