Delete trailing whitespaces in all *.{v,ml*} files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 33 insertions, 33 deletions

diff --git a/ide/undo.ml b/ide/undo.ml
index d2fe81e1df..18c2f7a4da 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -10,16 +10,16 @@
 
 open GText
 open Ideutils
-type action = 
-  | Insert of string * int * int (* content*pos*length *) 
-  | Delete of string * int * int (* content*pos*length *) 
+type action =
+  | Insert of string * int * int (* content*pos*length *)
+  | Delete of string * int * int (* content*pos*length *)
 
 let neg act = match act with
   | Insert (s,i,l) -> Delete (s,i,l)
   | Delete (s,i,l) -> Insert (s,i,l)
 
 class undoable_view (tv:[>Gtk.text_view] Gtk.obj) =
-  let undo_lock = ref true in 
+  let undo_lock = ref true in
 object(self)
   inherit GText.view tv as super
   val history = (Stack.create () : action Stack.t)
@@ -29,25 +29,25 @@ object(self)
   method private dump_debug =
     if false (* !debug *) then begin
       prerr_endline "==========Stack top=============";
-      Stack.iter 
+      Stack.iter
 	(fun e -> match e with
 	   | Insert(s,p,l) ->
  	       Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l
-	   | Delete(s,p,l) -> 			   
+	   | Delete(s,p,l) ->
 	       Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l)
 	history;
       Printf.eprintf "Stack size %d\n" (Stack.length history);
       prerr_endline "==========Stack Bottom==========";
       prerr_endline "==========Queue start=============";
-      Queue.iter 
+      Queue.iter
 	(fun e -> match e with
 	   | Insert(s,p,l) ->
  	       Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l
-	   | Delete(s,p,l) -> 			   
+	   | Delete(s,p,l) ->
 	       Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l)
 	redo;
       Printf.eprintf "Stack size %d\n" (Queue.length redo);
-      prerr_endline "==========Queue End==========" 
+      prerr_endline "==========Queue End=========="
 
     end
 
@@ -57,16 +57,16 @@ object(self)
     undo_lock := false;
     prerr_endline "UNDO";
     try begin
-      let r = 
+      let r =
 	match Stack.pop history with
-	  | Insert(s,p,l) as act -> 
+	  | Insert(s,p,l) as act ->
 	      let start = self#buffer#get_iter_at_char p in
-	      (self#buffer#delete_interactive 
+	      (self#buffer#delete_interactive
 		 ~start
 		 ~stop:(start#forward_chars l)
 		 ()) or
 	      (Stack.push act history; false)
-	  | Delete(s,p,l) as act -> 
+	  | Delete(s,p,l) as act ->
 	      let iter = self#buffer#get_iter_at_char p in
 	      (self#buffer#insert_interactive ~iter s) or
 	      (Stack.push act history; false)
@@ -75,11 +75,11 @@ object(self)
 	Queue.push act redo;
 	Stack.push act nredo
       end;
-      undo_lock := true; 
+      undo_lock := true;
       r
     end
-    with Stack.Empty -> 
-      undo_lock := true; 
+    with Stack.Empty ->
+      undo_lock := true;
       false
   end else
     (prerr_endline "UNDO DISCARDED"; true)
@@ -97,7 +97,7 @@ object(self)
 	       end)
 	   );
 *)
-    ignore (self#buffer#connect#insert_text 
+    ignore (self#buffer#connect#insert_text
 	      ~callback:
 	      (fun it s ->
 		 if !undo_lock && not (Queue.is_empty redo) then begin
@@ -107,18 +107,18 @@ object(self)
 		   Queue.clear redo;
 		 end;
 (*		 let pos = it#offset in
-		 if Stack.is_empty history or 
+		 if Stack.is_empty history or
 		   s=" " or s="\t" or s="\n" or
-					(match Stack.top history with 
-					   | Insert(old,opos,olen) -> 
+					(match Stack.top history with
+					   | Insert(old,opos,olen) ->
 					       opos + olen <> pos
 					   | _ -> true)
 		 then *)
 		 Stack.push (Insert(s,it#offset,Glib.Utf8.length s)) history
 		 (*else begin
 		   match Stack.pop history with
-		     | Insert(olds,offset,len) -> 
-			 Stack.push 
+		     | Insert(olds,offset,len) ->
+			 Stack.push
 			 (Insert(olds^s,
 				 offset,
 				 len+(Glib.Utf8.length s)))
@@ -129,7 +129,7 @@ object(self)
 	      ));
     ignore (self#buffer#connect#delete_range
 	      ~callback:
-	      (fun ~start ~stop -> 
+	      (fun ~start ~stop ->
 		 if !undo_lock && not (Queue.is_empty redo) then begin
 		   Queue.iter (fun e -> Stack.push e history) redo;
 		   Queue.clear redo;
@@ -138,12 +138,12 @@ object(self)
 		 let stop_offset = stop#offset in
 		 let s = self#buffer#get_text ~start ~stop () in
 (*		 if Stack.is_empty history or (match Stack.top history with
-						 | Delete(old,opos,olen) -> 
+						 | Delete(old,opos,olen) ->
 						     olen=1 or opos <> start_offset
 						 | _ -> true
 					      )
 		 then
-*)		   Stack.push 
+*)		   Stack.push
 		     (Delete(s,
 			     start_offset,
 			     stop_offset - start_offset
@@ -151,27 +151,27 @@ object(self)
 		     history
 	(*	 else begin
 		   match Stack.pop history with
-		     | Delete(olds,offset,len) -> 
-			 Stack.push 
+		     | Delete(olds,offset,len) ->
+			 Stack.push
 			 (Delete(olds^s,
 				 offset,
 				 len+(Glib.Utf8.length s)))
 			 history
 		     | _ -> assert false
-			 
+
 		 end*);
 		 self#dump_debug
 	      ))
 end
 
 let undoable_view ?(buffer:GText.buffer option) =
-  GtkText.View.make_params [] 
-    ~cont:(GContainer.pack_container 
+  GtkText.View.make_params []
+    ~cont:(GContainer.pack_container
 	     ~create:
-	     (fun pl -> let w = match buffer with 
+	     (fun pl -> let w = match buffer with
 	      | None -> GtkText.View.create []
 	      | Some b -> GtkText.View.create_with_buffer b#as_buffer
 	      in
 	      Gobject.set_params w pl; ((new undoable_view w):undoable_view)))
-    
-    
+
+