Coqide : ported to lablgtk2 snapshot of 2003/07/07

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

9 files changed, 88 insertions, 76 deletions

diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml
index 83d900cc6e..d02243d118 100644
--- a/ide/blaster_window.ml
+++ b/ide/blaster_window.ml
@@ -49,16 +49,16 @@ class blaster_window (n:int) =
   let _ = view#set_rules_hint true in
 
   let col = GTree.view_column ~title:"Argument" ()
-	      ~renderer:(GTree.cell_renderer_text(), ["text",argument]) in
+	      ~renderer:(GTree.cell_renderer_text [], ["text",argument]) in
   let _ = view#append_column col in
   let col = GTree.view_column ~title:"Tactics" ()
-	      ~renderer:(GTree.cell_renderer_text(), ["text",tactic]) in
+	      ~renderer:(GTree.cell_renderer_text [], ["text",tactic]) in
   let _ = view#append_column col in
   let col = GTree.view_column ~title:"Status" ()
-	      ~renderer:(GTree.cell_renderer_toggle (), ["active",status]) in
+	      ~renderer:(GTree.cell_renderer_toggle [], ["active",status]) in
   let _ = view#append_column col in
   let col = GTree.view_column ~title:"Delta Goal" ()
-	      ~renderer:(GTree.cell_renderer_text (), ["text",nb_goals]) in
+	      ~renderer:(GTree.cell_renderer_text [], ["text",nb_goals]) in
   let _ = view#append_column col in 
 
   let _ = GMisc.separator `HORIZONTAL ~packing:box1#pack () in
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 904b08c632..dfd83e6956 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -67,8 +67,8 @@ object(self)
     let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
     let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
     let combo = GEdit.combo ~popdown_strings:Coq_commands.state_preserving
-		  ~use_arrows:`DEFAULT
-		  ~ok_if_empty:false
+		  ~enable_arrow_keys:true
+		  ~allow_empty:false
 		  ~value_in_list:false (* true is not ok with disable_activate...*)
 		  ~packing:hbox#pack
 		  ()
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 01805ab1e0..45f56f1eeb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -18,7 +18,7 @@ let out_some s = match s with
   | None -> failwith "Internal error in out_some" | Some f -> f
 
 let cb_ = ref None
-let cb () = out_some !cb_
+let cb () = ((out_some !cb_):GData.clipboard)
 let last_cb_content = ref ""
 
 let yes_icon = `YES
@@ -63,13 +63,15 @@ let set_tab_label i n =
   let nb = notebook () in
   let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget 
   in
-  lbl#set_markup n
+  lbl#set_use_markup true;
+  lbl#set_text n
 
 let set_tab_image i s = 
   let nb = notebook () in
   let _,img,_ = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
   in
-  img#set_stock s ~size:small_size
+  img#set_icon_size small_size;
+  img#set_stock s
 
 let set_current_tab_image s = set_tab_image (notebook())#current_page s
   
@@ -419,7 +421,7 @@ let rec complete input_buffer w (offset:int) =
 	  
 let get_current_word () =
   let av = out_some ((get_current_view ()).analyzed_view) in 
-  match GtkBase.Clipboard.wait_for_text (cb ()) with
+  match GtkBase.Clipboard.wait_for_text (cb ())#as_clipboard with
     | None -> 
 	prerr_endline "None selected";
 	let it = av#get_insert in
@@ -665,7 +667,8 @@ object(self)
 	       ~default:1
 	       ~icon:
 	       (let img = GMisc.image () in
-		img#set_stock warning_icon ~size:dialog_size;
+		img#set_stock warning_icon;
+		img#set_icon_size dialog_size;
 		img#coerce)
 	       ("File "^f^"already exists")
 	    )
@@ -800,7 +803,7 @@ object(self)
 		ignore
 		  (tag#connect#event ~callback:
 		     (fun ~origin ev it ->
-			match GdkEvent.get_type ev with 
+			begin match GdkEvent.get_type ev with 
 			| `BUTTON_PRESS -> 
 			    let ev = (GdkEvent.Button.cast ev) in
 			    if (GdkEvent.Button.button ev) = 3
@@ -844,7 +847,9 @@ object(self)
 			    
 			    prerr_endline "Applied tag";
 			    ()
-			| _ -> ())
+			| _ -> ()
+			end;true
+		     )
 		  );
 		tag
 	      in
@@ -1523,7 +1528,7 @@ Please restart and report NOW.";
     let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"]  in
     self#electric_paren paren_highlight_tag;
     ignore (input_buffer#connect#after#mark_set 
-	      ~callback:(fun it (m:Gtk.textmark) ->
+	      ~callback:(fun it (m:Gtk.text_mark) ->
 			   !set_location 
 			   (Printf.sprintf 
 			      "Line: %5d Char: %3d" (self#get_insert#line + 1)
@@ -1901,7 +1906,8 @@ let main files =
 	       ~default:0
 	       ~icon:
 	       (let img = GMisc.image () in
-		img#set_stock warning_icon ~size:dialog_size;
+		img#set_stock warning_icon;
+		img#set_icon_size dialog_size;
 		img#coerce)
 	       "There are unsaved buffers"
 	    )
@@ -1928,18 +1934,18 @@ let main files =
   ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
 	   (fun () -> GtkSignal.emit_unit
 	      (get_current_view()).view#as_view 
-	      GtkText.View.Signals.copy_clipboard));
+	      GtkText.View.S.copy_clipboard));
   ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
 	   (do_if_not_computing 
 	      (fun () -> GtkSignal.emit_unit
 		 (get_current_view()).view#as_view 
-		 GtkText.View.Signals.cut_clipboard)));
+		 GtkText.View.S.cut_clipboard)));
   ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
 	   (do_if_not_computing
 	      (fun () -> 
 		 try GtkSignal.emit_unit
 		   (get_current_view()).view#as_view 
-		   GtkText.View.Signals.paste_clipboard
+		   GtkText.View.S.paste_clipboard
 		 with _ -> prerr_endline "EMIT PASTE FAILED")));
   ignore (edit_f#add_separator ());
   let read_only_i = edit_f#add_check_item "Expert" ~active:false
@@ -2486,7 +2492,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   in
   let search_history = ref [] in
   let search_input = GEdit.combo ~popdown_strings:!search_history
-		       ~use_arrows:`DEFAULT
+		       ~enable_arrow_keys:true
 		       ~show:false
 		       ~packing:(lower_hbox#pack ~expand:false) () 
   in
@@ -2638,7 +2644,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 
   (* Progress Bar *)
   pulse := 
-  (GRange.progress_bar ~text:"CoqIde started" ~pulse_step:0.2 ~packing:lower_hbox#pack ())#pulse;
+  (let pb = GRange.progress_bar ~pulse_step:0.2 ~packing:lower_hbox#pack ()
+   in pb#set_text "CoqIde started";pb)#pulse;
   let tv2 = GText.view ~packing:(sw2#add) () in
   tv2#misc#set_name "GoalWindow";
   let _ = tv2#set_editable false in
@@ -2673,7 +2680,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 				     t#as_tag
 				     tv2#as_widget
 				     e 
-				     it#as_textiter))
+				     it#as_iter))
 		       tags;
 		     false)) e;
 	       false)
@@ -2751,7 +2758,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		   !current.window_width <- w;
 		 end
 	    ));
-  ignore(nb#connect#switch_page 
+  ignore(nb#connect#change_current_page
 	   ~callback:
 	   (fun i -> List.iter (function f -> f i) !to_do_on_page_switch)
 	);
@@ -2779,7 +2786,7 @@ let start () =
   ignore (GtkMain.Main.init ());
   GtkData.AccelGroup.set_default_mod_mask 
     (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);
-  cb_ := Some (GtkBase.Clipboard.get Gdk.Atom.primary);
+  cb_ := Some (GData.clipboard Gdk.Atom.primary);
   ignore (
     Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
 							`WARNING;`CRITICAL]
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index e1c1a2f64b..8c7a2ec1f4 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -187,12 +187,12 @@ let select_file ~title ?(dir = last_dir) ?(filename="") () =
     if Filename.is_relative filename then begin
       if !dir <> "" then
         let filename = Filename.concat !dir filename in 
-        GWindow.file_selection ~fileop_buttons:true ~modal:true ~title ~filename ()
+        GWindow.file_selection ~show_fileops:true ~modal:true ~title ~filename ()
       else
-        GWindow.file_selection ~fileop_buttons:true ~modal:true ~title ()
+        GWindow.file_selection ~show_fileops:true ~modal:true ~title ()
     end else begin
       dir := Filename.dirname filename;
-      GWindow.file_selection ~fileop_buttons:true ~modal:true ~title ~filename ()
+      GWindow.file_selection ~show_fileops:true ~modal:true ~title ~filename ()
     end
   in
   fs#complete ~filter:"";
@@ -200,8 +200,8 @@ let select_file ~title ?(dir = last_dir) ?(filename="") () =
   let file = ref None in 
   ignore (fs#ok_button#connect#clicked ~callback:
     begin fun () ->
-      file := Some fs#get_filename; 
-      dir := Filename.dirname fs#get_filename;
+      file := Some fs#filename; 
+      dir := Filename.dirname fs#filename;
       fs#destroy ()
     end);
   ignore (fs # cancel_button # connect#clicked ~callback:fs#destroy);
@@ -233,7 +233,7 @@ let async =
 
 let stock_to_widget ?(size=`DIALOG) s = 
   let img = GMisc.image () 
-  in img#set_stock ~size s ;
+  in img#set_stock s;
   img#coerce
 
 let rec print_list print fmt = function
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 9e22a36369..1c7f37f7f3 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -273,9 +273,10 @@ let configure () =
     custom
       ~label:"Fonts for text"
       box
-      (fun () -> match w#font_name with 
-	 | None -> () 
-	 | Some fd -> !current.text_font <- (Pango.Font.from_string fd) ; !change_font !current.text_font)
+      (fun () -> 
+	 let fd =  w#font_name in
+	 !current.text_font <- (Pango.Font.from_string fd) ; 
+	 !change_font !current.text_font)
       true
   in
   let show_toolbar = 
diff --git a/ide/undo.ml b/ide/undo.ml
index 5099580667..18d224902e 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -1,4 +1,3 @@
-
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
@@ -19,7 +18,7 @@ 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.textview Gtk.obj) =
+class undoable_view (tv:Gtk.text_view Gtk.obj) =
   let undo_lock = ref true in 
 object(self)
   inherit GText.view tv as super
@@ -166,13 +165,14 @@ object(self)
 	      ))
 end
 
-let undoable_view ?(buffer:buffer option) 
-?editable ?cursor_visible ?wrap_mode
-    ?packing ?show () = 
-    let w = match buffer with 
-      | None -> GtkText.View.create ()
-      | Some b -> GtkText.View.create_with_buffer b#as_buffer
-    in
-    GtkText.View.set w ?editable ?cursor_visible ?wrap_mode;
-    GObj.pack_return (new undoable_view w) ~packing ~show
-
+let undoable_view ?(buffer:GText.buffer option) =
+  GtkText.View.make_params [] 
+    ~cont:(GContainer.pack_container 
+	     ~create:
+	     (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)))
+    
+    
diff --git a/ide/undo.mli b/ide/undo.mli
index 64812a53e4..bc19bd933d 100644
--- a/ide/undo.mli
+++ b/ide/undo.mli
@@ -10,7 +10,7 @@
 
 (* An undoable view class *)
 
-class undoable_view : Gtk.textview Gtk.obj ->
+class undoable_view : Gtk.text_view Gtk.obj ->
 object
   inherit GText.view
   method undo : bool
@@ -19,10 +19,17 @@ object
 end
 
 val undoable_view : 
-  ?buffer:GText.buffer ->
-  ?editable:bool ->
-  ?cursor_visible:bool ->
-  ?wrap_mode:Gtk.Tags.wrap_mode ->
-  ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> undoable_view
+    ?buffer:GText.buffer ->
+    ?editable:bool ->
+    ?cursor_visible:bool ->
+    ?justification:GtkEnums.justification ->
+    ?wrap_mode:GtkEnums.wrap_mode ->
+    ?border_width:int ->
+    ?width:int ->
+    ?height:int ->
+    ?packing:(GObj.widget -> unit) ->
+    ?show:bool ->
+    unit ->
+  undoable_view
 
 
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 835682b691..b6f6550bd4 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -70,9 +70,9 @@ let select_files ?dir
   let _ = fs # ok_button # connect#clicked ~callback:
       (match fok with
         None ->
-          (fun () -> files := [fs#get_filename] ; fs#destroy ())
+          (fun () -> files := [fs#filename] ; fs#destroy ())
       | Some f ->
-          (fun () -> f fs#get_filename)
+          (fun () -> f fs#filename)
       )
   in
   let _ = fs # cancel_button # connect#clicked ~callback:fs#destroy in
@@ -371,7 +371,7 @@ class combo_param_box param =
   let wc = GEdit.combo
       ~popdown_strings: param.combo_choices
       ~value_in_list: (not param.combo_new_allowed)
-      ~ok_if_empty: param.combo_blank_allowed
+(*      ~ok_if_empty: param.combo_blank_allowed*)
       ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
       ()
   in
@@ -464,7 +464,7 @@ class color_param_box param =
     let _ = dialog#connect#destroy GMain.Main.quit in
     let _ = wb_ok#connect#clicked
 	(fun () -> 
-	  let color = dialog#colorsel#get_color in
+	  (* let color = dialog#colorsel#get_color in
 	  let r = int_of_float (ceil (color.Gtk.red *. 255.)) in
 	  let g = int_of_float (ceil (color.Gtk.green *. 255.)) in
 	  let b = int_of_float (ceil (color.Gtk.blue *. 255.)) in
@@ -475,7 +475,7 @@ class color_param_box param =
 	    done
 	  in
 	  we#set_text s ;
-	  set_color s;
+	  set_color s;*)
 	  dialog#destroy ()
 	)
     in
@@ -548,8 +548,8 @@ class font_param_box param =
     let _ = wb_ok#connect#clicked
 	(fun () -> 
 	  let font_opt = dialog#selection#font_name in
-	  we#set_text (match font_opt with None -> "" | Some s -> s) ;
-	  set_entry_font font_opt;
+(*	  we#set_text (match font_opt with None -> "" | Some s -> s) ;
+	  set_entry_font font_opt;*)
 	  dialog#destroy ()
 	)
     in
@@ -582,7 +582,7 @@ class text_param_box param =
       ~packing: (hbox#pack ~expand: true ~padding: 2) () 
   in
   let wt = GText.view ~packing:wscroll#add () in
-  let _ = wt#coerce#misc#set_size_request ~height:100 in
+(*   let _ = wt#coerce#misc#set_size_request ~height:100 in *)
   let _ = wt#set_editable param.string_editable in
   let _ = 
     match param.string_help with
@@ -1198,9 +1198,9 @@ let simple_edit ?(with_apply=true)
   let window = GWindow.window ~modal: true ~title: title () in
   let _ = match width, height with
     None, None -> ()
-  | Some w, None -> window#misc#set_geometry ~width: w ()
-  | None, Some h -> window#misc#set_geometry ~height: h ()
-  | Some w, Some h -> window#misc#set_geometry ~width: w ~height: h ()
+  | Some w, None -> window#misc#set_size_request ~width: w ()
+  | None, Some h -> window#misc#set_size_request ~height: h ()
+  | Some w, Some h -> window#misc#set_size_request ~width: w ~height: h ()
   in
   let _ = window#connect#destroy ~callback: GMain.Main.quit in
   let buttons = 
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index 20111bf84a..e6d2f4d48c 100644
--- a/ide/utils/editable_cells.ml
+++ b/ide/utils/editable_cells.ml
@@ -26,27 +26,24 @@ let create l =
   (* Alternate colors for the rows *)
   view#set_rules_hint true;
 
-  let renderer_comm = GTree.cell_renderer_text () in
-  ignore (GtkSignal.connect renderer_comm 
-	    ~sgn:GtkTree.CellRendererText.Signals.edited 
-	    ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
-			 store#set 
-			 ~row:(store#get_iter path) 
-			 ~column:command_col s));
-  GtkText.Tag.set_property renderer_comm (`EDITABLE true);
+  let renderer_comm = GTree.cell_renderer_text [`EDITABLE true]  in
+  ignore (renderer_comm#connect#edited 
+    ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
+		 store#set 
+		 ~row:(store#get_iter path) 
+		 ~column:command_col s));
   let first = 
     GTree.view_column ~title:"Coq Command to try" 
       ~renderer:(renderer_comm,["text",command_col]) 
       () 
   in ignore (view#append_column first);
 
-  let renderer_coq = GTree.cell_renderer_text () in
-  ignore (GtkSignal.connect renderer_coq ~sgn:GtkTree.CellRendererText.Signals.edited 
-    ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
-		 store#set 
-		 ~row:(store#get_iter path) 
-		 ~column:coq_col s));
-  GtkText.Tag.set_property renderer_coq (`EDITABLE true);
+  let renderer_coq = GTree.cell_renderer_text [`EDITABLE true] in
+  ignore(renderer_coq#connect#edited
+	   ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
+			store#set 
+			~row:(store#get_iter path) 
+			~column:coq_col s));
   let second = 
     GTree.view_column ~title:"Coq Command to insert" 
       ~renderer:(renderer_coq,["text",coq_col])