From 2bdcd093b357adb2185518dabbafd1a0b9279044 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Tue, 27 Mar 2012 07:41:19 +0200 Subject: Imported Upstream version 8.3.pl4 --- ide/coq.ml | 8 ++++---- ide/coqide.ml | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 1c6229b4..1a5b9def 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -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 -- cgit v1.2.3