aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/configwin.ml2
-rw-r--r--ide/configwin.mli2
-rw-r--r--ide/configwin_ihm.ml104
-rw-r--r--ide/configwin_ihm.mli2
-rw-r--r--ide/configwin_types.ml2
-rw-r--r--ide/coq.ml21
-rw-r--r--ide/coqOps.ml2
-rw-r--r--ide/coqide.ml35
-rw-r--r--ide/coqide_main.ml2
-rw-r--r--ide/dune7
-rw-r--r--ide/ide.mllib1
-rw-r--r--ide/ideutils.ml37
-rw-r--r--ide/ideutils.mli6
-rw-r--r--ide/nanoPG.ml2
-rw-r--r--ide/preferences.ml101
-rw-r--r--ide/preferences.mli8
-rw-r--r--ide/session.ml8
-rw-r--r--ide/tags.ml12
-rw-r--r--ide/tags.mli3
-rw-r--r--ide/wg_Command.ml8
-rw-r--r--ide/wg_Detachable.ml3
-rw-r--r--ide/wg_Find.ml26
-rw-r--r--ide/wg_MessageView.ml8
-rw-r--r--ide/wg_Notebook.mli3
-rw-r--r--ide/wg_ProofView.ml8
-rw-r--r--ide/wg_ScriptView.ml18
-rw-r--r--ide/wg_ScriptView.mli8
-rw-r--r--ide/wg_Segment.ml22
-rw-r--r--ide/wg_Segment.mli2
29 files changed, 192 insertions, 271 deletions
diff --git a/ide/configwin.ml b/ide/configwin.ml
index 24be721631..79a1eae880 100644
--- a/ide/configwin.ml
+++ b/ide/configwin.ml
@@ -37,8 +37,10 @@ type return_button =
| Return_cancel
let string = Configwin_ihm.string
+(*
let strings = Configwin_ihm.strings
let list = Configwin_ihm.list
+*)
let bool = Configwin_ihm.bool
let combo = Configwin_ihm.combo
let custom = Configwin_ihm.custom
diff --git a/ide/configwin.mli b/ide/configwin.mli
index 0ee77d69b5..fa22846d19 100644
--- a/ide/configwin.mli
+++ b/ide/configwin.mli
@@ -69,6 +69,7 @@ val string : ?editable: bool -> ?expand: bool -> ?help: string ->
val bool : ?editable: bool -> ?help: string ->
?f: (bool -> unit) -> string -> bool -> parameter_kind
+(*
(** [strings label value] creates a string list parameter.
@param editable indicate if the value is editable (default is [true]).
@param help an optional help message.
@@ -119,6 +120,7 @@ val list : ?editable: bool -> ?help: string ->
('a -> string list) ->
'a list ->
parameter_kind
+*)
(** [combo label choices value] creates a combo parameter.
@param editable indicate if the value is editable (default is [true]).
diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml
index 8420d930d5..0f3fd38a7a 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -27,6 +27,10 @@
open Configwin_types
+let set_help_tip wev = function
+ | None -> ()
+ | Some help -> GtkBase.Widget.Tooltip.set_text wev#as_widget help
+
let modifiers_to_string m =
let rec iter m s =
match m with
@@ -55,7 +59,7 @@ class type widget =
let debug = false
let dbg s = if debug then Minilib.log s else ()
-
+(*
(** This class builds a frame with a clist and two buttons :
one to add items and one to remove the selected items.
The class takes in parameter a function used to add items and
@@ -71,7 +75,6 @@ class ['a] list_selection_box
f_color
(eq : 'a -> 'a -> bool)
add_function title editable
- (tt:GData.tooltips)
=
let _ = dbg "list_selection_box" in
let wev = GBin.event_box () in
@@ -94,12 +97,8 @@ class ['a] list_selection_box
~titles_show: true
~packing: wscroll#add ()
in
- let _ =
- match help_opt with
- None -> ()
- | Some help ->
- tt#set_tip ~text: help ~privat: help wev#coerce
- in (* the vbox for the buttons *)
+ let _ = set_help_tip wev help_opt in
+ (* the vbox for the buttons *)
let vbox_buttons = GPack.vbox () in
let _ =
if editable then
@@ -279,10 +278,10 @@ class ['a] list_selection_box
(* initialize the clist with the listref *)
self#update !listref
end;;
-
+*)
(** This class is used to build a box for a string parameter.*)
-class string_param_box param (tt:GData.tooltips) =
+class string_param_box param =
let _ = dbg "string_param_box" in
let hbox = GPack.hbox () in
let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
@@ -292,12 +291,7 @@ class string_param_box param (tt:GData.tooltips) =
~packing: (hbox#pack ~expand: param.string_expand ~padding: 2)
()
in
- let _ =
- match param.string_help with
- None -> ()
- | Some help ->
- tt#set_tip ~text: help ~privat: help wev#coerce
- in
+ let _ = set_help_tip wev param.string_help in
let _ = we#set_text (param.string_to_string param.string_value) in
object (self)
@@ -316,17 +310,12 @@ class string_param_box param (tt:GData.tooltips) =
end ;;
(** This class is used to build a box for a combo parameter.*)
-class combo_param_box param (tt:GData.tooltips) =
+class combo_param_box param =
let _ = dbg "combo_param_box" in
let hbox = GPack.hbox () in
let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
let _wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in
- let _ =
- match param.combo_help with
- None -> ()
- | Some help ->
- tt#set_tip ~text: help ~privat: help wev#coerce
- in
+ let _ = set_help_tip wev param.combo_help in
let get_value = if not param.combo_new_allowed then
let wc = GEdit.combo_box_text
~strings: param.combo_choices
@@ -341,13 +330,13 @@ class combo_param_box param (tt:GData.tooltips) =
fun () -> match GEdit.text_combo_get_active wc with |None -> "" |Some s -> s
else
let (wc,_) = GEdit.combo_box_entry_text
- ~strings: param.combo_choices
- ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
- ()
+ ~strings: param.combo_choices
+ ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
+ ()
in
let _ = wc#entry#set_editable param.combo_editable in
let _ = wc#entry#set_text param.combo_value in
- fun () -> wc#entry#text
+ fun () -> wc#entry#text
in
object (self)
@@ -365,7 +354,7 @@ object (self)
end ;;
(** Class used to pack a custom box. *)
-class custom_param_box param (tt:GData.tooltips) =
+class custom_param_box param =
let _ = dbg "custom_param_box" in
let top =
match param.custom_framed with
@@ -381,7 +370,7 @@ class custom_param_box param (tt:GData.tooltips) =
end
(** This class is used to build a box for a text parameter.*)
-class text_param_box param (tt:GData.tooltips) =
+class text_param_box param =
let _ = dbg "text_param_box" in
let wf = GBin.frame ~label: param.string_label ~height: 100 () in
let wev = GBin.event_box ~packing: wf#add () in
@@ -395,12 +384,7 @@ class text_param_box param (tt:GData.tooltips) =
~packing: wscroll#add
()
in
- let _ =
- match param.string_help with
- None -> ()
- | Some help ->
- tt#set_tip ~text: help ~privat: help wev#coerce
- in
+ let _ = set_help_tip wev param.string_help in
let _ = dbg "text_param_box: buffer creation" in
let buffer = GText.buffer () in
@@ -427,17 +411,13 @@ class text_param_box param (tt:GData.tooltips) =
end ;;
(** This class is used to build a box for a boolean parameter.*)
-class bool_param_box param (tt:GData.tooltips) =
+class bool_param_box param =
let _ = dbg "bool_param_box" in
let wchk = GButton.check_button
~label: param.bool_label
()
in
- let _ =
- match param.bool_help with
- None -> ()
- | Some help -> tt#set_tip ~text: help ~privat: help wchk#coerce
- in
+ let _ = set_help_tip wchk param.bool_help in
let _ = wchk#set_active param.bool_value in
let _ = wchk#misc#set_sensitive param.bool_editable in
@@ -471,14 +451,7 @@ class modifiers_param_box param =
else value := List.filter ((<>) modifier) !value)))
param.md_allow
in
- let _ =
- match param.md_help with
- None -> ()
- | Some help ->
- let tooltips = GData.tooltips () in
- ignore (hbox#connect#destroy ~callback: tooltips#destroy);
- tooltips#set_tip wev#coerce ~text: help ~privat: help
- in
+ let _ = set_help_tip wev param.md_help in
object (self)
(** This method returns the main box ready to be packed. *)
@@ -493,9 +466,9 @@ class modifiers_param_box param =
else
()
end ;;
-
+(*
(** This class is used to build a box for a parameter whose values are a list.*)
-class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) =
+class ['a] list_param_box (param : 'a list_param) =
let _ = dbg "list_param_box" in
let listref = ref param.list_value in
let frame_selection = new list_selection_box
@@ -520,9 +493,10 @@ class ['a] list_param_box (param : 'a list_param) (tt:GData.tooltips) =
param.list_f_apply !listref ;
param.list_value <- !listref
end ;;
+*)
(** This class creates a configuration box from a configuration structure *)
-class configuration_box (tt : GData.tooltips) conf_struct =
+class configuration_box conf_struct =
let main_box = GPack.hbox () in
@@ -553,27 +527,27 @@ class configuration_box (tt : GData.tooltips) conf_struct =
let make_param (main_box : #GPack.box) = function
| String_param p ->
- let box = new string_param_box p tt in
+ let box = new string_param_box p in
let _ = main_box#pack ~expand: false ~padding: 2 box#box in
box
| Combo_param p ->
- let box = new combo_param_box p tt in
+ let box = new combo_param_box p in
let _ = main_box#pack ~expand: false ~padding: 2 box#box in
box
| Text_param p ->
- let box = new text_param_box p tt in
+ let box = new text_param_box p in
let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
box
| Bool_param p ->
- let box = new bool_param_box p tt in
+ let box = new bool_param_box p in
let _ = main_box#pack ~expand: false ~padding: 2 box#box in
box
| List_param f ->
- let box = f tt in
+ let box = f () in
let _ = main_box#pack ~expand: true ~padding: 2 box#box in
box
| Custom_param p ->
- let box = new custom_param_box p tt in
+ let box = new custom_param_box p in
let _ = main_box#pack ~expand: p.custom_expand ~padding: 2 box#box in
box
| Modifiers_param p ->
@@ -684,11 +658,9 @@ let edit ?(with_apply=true)
?parent ?height ?width
()
in
- let tooltips = GData.tooltips () in
-
- let config_box = new configuration_box tooltips conf_struct in
+ let config_box = new configuration_box conf_struct in
- let _ = dialog#vbox#add config_box#box#coerce in
+ let _ = dialog#vbox#pack ~expand:true config_box#box#coerce in
if with_apply then
dialog#add_button Configwin_messages.mApply `APPLY;
@@ -697,7 +669,6 @@ let edit ?(with_apply=true)
dialog#add_button Configwin_messages.mCancel `CANCEL;
let destroy () =
- tooltips#destroy () ;
dialog#destroy ();
in
let rec iter rep =
@@ -714,10 +685,12 @@ let edit ?(with_apply=true)
in
iter Return_cancel
+(*
let edit_string l s =
match GToolbox.input_string ~title: l ~text: s Configwin_messages.mValue with
None -> s
| Some s2 -> s2
+*)
(** Create a string param. *)
let string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
@@ -744,6 +717,7 @@ let bool ?(editable=true) ?help ?(f=(fun _ -> ())) label v =
bool_f_apply = f ;
}
+(*
(** Create a list param. *)
let list ?(editable=true) ?help
?(f=(fun (_:'a list) -> ()))
@@ -753,7 +727,7 @@ let list ?(editable=true) ?help
?titles ?(color=(fun (_:'a) -> (None : string option)))
label (f_strings : 'a -> string list) v =
List_param
- (fun tt ->
+ (fun () ->
new list_param_box
{
list_label = label ;
@@ -768,7 +742,6 @@ let list ?(editable=true) ?help
list_f_add = add ;
list_f_apply = f ;
}
- tt
)
(** Create a strings param. *)
@@ -777,6 +750,7 @@ let strings ?(editable=true) ?help
?(eq=Pervasives.(=))
?(add=(fun () -> [])) label v =
list ~editable ?help ~f ~eq ~edit: (edit_string label) ~add label (fun s -> [s]) v
+*)
(** Create a combo param. *)
let combo ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ()))
diff --git a/ide/configwin_ihm.mli b/ide/configwin_ihm.mli
index 772a0958ff..ce6cd4d7c1 100644
--- a/ide/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
@@ -29,6 +29,7 @@ val string : ?editable: bool -> ?expand: bool -> ?help: string ->
?f: (string -> unit) -> string -> string -> parameter_kind
val bool : ?editable: bool -> ?help: string ->
?f: (bool -> unit) -> string -> bool -> parameter_kind
+(*
val strings : ?editable: bool -> ?help: string ->
?f: (string list -> unit) ->
?eq: (string -> string -> bool) ->
@@ -45,6 +46,7 @@ val list : ?editable: bool -> ?help: string ->
('a -> string list) ->
'a list ->
parameter_kind
+*)
val combo : ?editable: bool -> ?expand: bool -> ?help: string ->
?f: (string -> unit) ->
?new_allowed: bool -> ?blank_allowed: bool ->
diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml
index 9e339d135d..251e3dded3 100644
--- a/ide/configwin_types.ml
+++ b/ide/configwin_types.ml
@@ -97,7 +97,7 @@ type modifiers_param = {
(** This type represents the different kinds of parameters. *)
type parameter_kind =
String_param of string string_param
- | List_param of (GData.tooltips -> <box: GObj.widget ; apply : unit>)
+ | List_param of (unit -> <box: GObj.widget ; apply : unit>)
| Bool_param of bool_param
| Text_param of string string_param
| Combo_param of combo_param
diff --git a/ide/coq.ml b/ide/coq.ml
index 91cd448eda..a420a3cbf5 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -119,7 +119,7 @@ let rec filter_coq_opts args =
and asks_for_coqtop args =
let pb_mes = GWindow.message_dialog
- ~message:"Failed to load coqtop. Reset the preference to default ?"
+ ~message:"Failed to load coqidetop. Reset the preference to default ?"
~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
match pb_mes#run () with
| `YES ->
@@ -128,16 +128,15 @@ and asks_for_coqtop args =
let () = pb_mes#destroy () in
filter_coq_opts args
| `DELETE_EVENT | `NO ->
- let () = pb_mes#destroy () in
- let cmd_sel = GWindow.file_selection
- ~title:"Coqtop to execute (edit your preference then)"
- ~filename:(coqtop_path ()) ~urgency_hint:true () in
- match cmd_sel#run () with
- | `OK ->
- let () = custom_coqtop := (Some cmd_sel#filename) in
- let () = cmd_sel#destroy () in
+ let file = select_file_for_open
+ ~title:"coqidetop to execute (edit your preference then)"
+ ~filter:false
+ ~filename:(coqtop_path ()) () in
+ match file with
+ | Some _ ->
+ let () = custom_coqtop := file in
filter_coq_opts args
- | `CANCEL | `DELETE_EVENT | `HELP -> exit 0
+ | None -> exit 0
exception WrongExitStatus of string
@@ -419,7 +418,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
let title = "Warning" in
let icon = (warn_image ())#coerce in
let buttons = ["Reset"; "Save all and quit"; "Quit without saving"] in
- let ans = GToolbox.question_box ~title ~buttons ~icon "Coqtop died badly." in
+ let ans = GToolbox.question_box ~title ~buttons ~icon "coqidetop died badly." in
if ans = 2 then (!save_all (); GtkMain.Main.quit ())
else if ans = 3 then GtkMain.Main.quit ()
| Planned -> ()
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 8da9900724..4aa801c2b2 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -250,6 +250,7 @@ object(self)
feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback;
let md = segment_model document in
segment#set_model md;
+(*
let on_click id =
let find _ _ s = Int.equal s.index id in
let sentence = Doc.find document find in
@@ -266,6 +267,7 @@ object(self)
ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
in
let _ = segment#connect#clicked ~callback:on_click in
+*)
()
method private tooltip_callback ~x ~y ~kbd tooltip =
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 48c08899e0..eaeeaa0001 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -193,7 +193,7 @@ let confirm_save ok =
let select_and_save ?parent ~saveas ?filename sn =
let do_save = if saveas then sn.fileops#saveas ?parent else sn.fileops#save in
let title = if saveas then "Save file as" else "Save file" in
- match select_file_for_save ~title ?filename () with
+ match select_file_for_save ~title ?parent ?filename () with
|None -> false
|Some f ->
let ok = do_save f in
@@ -213,7 +213,8 @@ let check_save ?parent ~saveas sn =
exception DontQuit
let check_quit ?parent saveall =
- (try save_pref () with _ -> flash_info "Cannot save preferences");
+ (try save_pref ()
+ with e -> flash_info ("Cannot save preferences (" ^ Printexc.to_string e ^ ")"));
let is_modified sn = sn.buffer#modified in
if List.exists is_modified notebook#pages then begin
let answ = Configwin_ihm.question_box ~title:"Quit"
@@ -271,11 +272,11 @@ let newfile _ =
let index = notebook#append_term session in
notebook#goto_page index
-let load _ =
+let load ?parent _ =
let filename =
try notebook#current_term.fileops#filename
with Invalid_argument _ -> None in
- match select_file_for_open ~title:"Load file" ?filename () with
+ match select_file_for_open ~title:"Load file" ?parent ?filename () with
| None -> ()
| Some f -> FileAux.load_file f
@@ -359,7 +360,7 @@ let print sn =
Filename.quote (Filename.basename f_name) ^ " | " ^ cmd_print#get
in
let w = GWindow.window ~title:"Print" ~modal:true
- ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" ()
+ ~position:`CENTER ~wmclass:("CoqIDE","CoqIDE") ()
in
let v = GPack.vbox ~spacing:10 ~border_width:10 ~packing:w#add ()
in
@@ -812,7 +813,7 @@ let zoom_fit sn =
let space = script#misc#allocation.Gtk.width in
let cols = script#right_margin_position in
let pango_ctx = script#misc#pango_context in
- let layout = pango_ctx#create_layout in
+ let layout = pango_ctx#create_layout#as_layout in
let fsize = Pango.Font.get_size (Pango.Font.from_string text_font#get) in
Pango.Layout.set_text layout (String.make cols 'X');
let tlen = fst (Pango.Layout.get_pixel_size layout) in
@@ -939,7 +940,7 @@ let emit_to_focus window sgn =
let build_ui () =
let w = GWindow.window
- ~wm_class:"CoqIde" ~wm_name:"CoqIde"
+ ~wmclass:("CoqIde","CoqIde")
~width:window_width#get ~height:window_height#get
~title:"CoqIde" ()
in
@@ -972,7 +973,7 @@ let build_ui () =
menu file_menu [
item "File" ~label:"_File";
item "New" ~callback:File.newfile ~stock:`NEW;
- item "Open" ~callback:File.load ~stock:`OPEN;
+ item "Open" ~callback:(File.load ~parent:w) ~stock:`OPEN;
item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer";
item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w);
item "Save all" ~label:"Sa_ve all" ~callback:File.saveall;
@@ -1021,7 +1022,8 @@ let build_ui () =
~callback:(fun _ ->
begin
try Preferences.configure ~apply:refresh_notebook_pos w
- with _ -> flash_info "Cannot save preferences"
+ with e ->
+ flash_info ("Editing preferences failed (" ^ Printexc.to_string e ^ ")")
end;
reset_revert_timer ());
];
@@ -1182,10 +1184,10 @@ let build_ui () =
item "Help" ~label:"_Help";
item "Browse Coq Manual" ~label:"Browse Coq _Manual"
~callback:(fun _ ->
- browse notebook#current_term.messages#default_route#add_string (doc_url ()));
+ browse notebook#current_term.messages#default_route#add_string Coq_config.wwwrefman);
item "Browse Coq Library" ~label:"Browse Coq _Library"
~callback:(fun _ ->
- browse notebook#current_term.messages#default_route#add_string library_url#get);
+ browse notebook#current_term.messages#default_route#add_string Coq_config.wwwstdlib);
item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
~callback:(fun _ -> on_current_term (fun sn ->
browse_keyword sn.messages#default_route#add_string (get_current_word sn)));
@@ -1220,10 +1222,10 @@ let build_ui () =
((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
in
let () = GtkButton.Toolbar.set
- ~orientation:`HORIZONTAL ~style:`ICONS ~tooltips:true tbar
+ ~orientation:`HORIZONTAL ~style:`ICONS tbar
in
- let toolbar = new GObj.widget tbar in
- let () = vbox#pack toolbar in
+ let toolbar = new GButton.toolbar tbar in
+ let () = vbox#pack toolbar#coerce in
(* Emacs/PG mode *)
NanoPG.init w notebook all_menus;
@@ -1303,11 +1305,6 @@ let build_ui () =
let _ = source_style#connect#changed ~callback:refresh_style in
let _ = source_language#connect#changed ~callback:refresh_language in
- (* Color configuration *)
- Tags.Script.incomplete#set_property
- (`BACKGROUND_STIPPLE
- (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
-
(* Showtime ! *)
w#show ();
w
diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml
index 21f513b8f4..79420b3857 100644
--- a/ide/coqide_main.ml
+++ b/ide/coqide_main.ml
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-let _ = GtkMain.Main.init ()
+let _ = Coqide.set_signal_handlers ()
(* We handle Gtk warning messages ourselves :
- on win32, we don't want them to end on a non-existing console
diff --git a/ide/dune b/ide/dune
index 5e3886624c..e3e61609af 100644
--- a/ide/dune
+++ b/ide/dune
@@ -25,12 +25,11 @@
; IDE Client
(library
- (name gui)
- (public_name coqide.gui)
+ (name coqide_gui)
(wrapped false)
(modules (:standard \ document fake_ide idetop coqide_main))
(optional)
- (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2))
+ (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3))
(rule
(targets coqide_os_specific.ml)
@@ -42,7 +41,7 @@
(public_name coqide)
(package coqide)
(modules coqide_main)
- (libraries coqide.gui))
+ (libraries coqide_gui))
; FIXME: we should install those in share/coqide. We better do this
; once the make-based system has been phased out.
diff --git a/ide/ide.mllib b/ide/ide.mllib
index a7ade71307..30ac5c9ad7 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,7 +9,6 @@ Config_lexer
Utf8_convert
Preferences
Project_file
-Topfmt
Ideutils
Coq
Coq_lex
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index c14af7d21d..8c5b3fcc5b 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -8,9 +8,10 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-
open Preferences
+let _ = GtkMain.Main.init ()
+
let warn_image () =
let img = GMisc.image () in
img#set_stock `DIALOG_WARNING;
@@ -229,14 +230,17 @@ let current_dir () = match project_path#get with
| None -> ""
| Some dir -> dir
-let select_file_for_open ~title ?filename () =
+let select_file_for_open ~title ?(filter=true) ?parent ?filename () =
let file_chooser =
- GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ()
+ GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ?parent ()
in
file_chooser#add_button_stock `CANCEL `CANCEL ;
file_chooser#add_select_button_stock `OPEN `OPEN ;
- file_chooser#add_filter (filter_coq_files ());
- file_chooser#add_filter (filter_all_files ());
+ if filter then
+ begin
+ file_chooser#add_filter (filter_coq_files ());
+ file_chooser#add_filter (filter_all_files ())
+ end;
file_chooser#set_default_response `OPEN;
let dir = match filename with
| None -> current_dir ()
@@ -255,10 +259,10 @@ let select_file_for_open ~title ?filename () =
file_chooser#destroy ();
file
-let select_file_for_save ~title ?filename () =
+let select_file_for_save ~title ?parent ?filename () =
let file = ref None in
let file_chooser =
- GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title ()
+ GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title ?parent ()
in
file_chooser#add_button_stock `CANCEL `CANCEL ;
file_chooser#add_select_button_stock `SAVE `SAVE ;
@@ -458,15 +462,6 @@ let browse prerr url =
in
run_command (fun _ -> ()) finally com
-let doc_url () =
- if doc_url#get = use_default_doc_url || doc_url#get = ""
- then
- let addr = List.fold_left Filename.concat (Envars.docdir ())
- ["html";"refman";"index.html"]
- in
- if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman
- else doc_url#get
-
let url_for_keyword =
let ht = Hashtbl.create 97 in
lazy (
@@ -476,13 +471,7 @@ let url_for_keyword =
(fun x -> Sys.file_exists (Filename.concat x "index_urls.txt"))
(Minilib.coqide_data_dirs ())) "index_urls.txt" in
open_in index_urls
- with Not_found ->
- let doc_url = doc_url () in
- let n = String.length doc_url in
- if n > 8 && String.sub doc_url 0 7 = "file://" then
- open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt")
- else
- raise Exit
+ with Not_found -> raise Exit
in
try while true do
let s = input_line cin in
@@ -503,7 +492,7 @@ let url_for_keyword =
let browse_keyword prerr text =
try
let u = Lazy.force url_for_keyword text in
- browse prerr (doc_url() ^ u)
+ browse prerr (Coq_config.wwwrefman ^ u)
with Not_found -> prerr ("No documentation found for \""^text^"\".\n")
let rec is_valid (s : Pp.t) = match Pp.repr s with
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 0031c59c17..57f59d19fe 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -13,7 +13,6 @@ val warning : string -> unit
val cb : GData.clipboard
-val doc_url : unit -> string
val browse : (string -> unit) -> string -> unit
val browse_keyword : (string -> unit) -> string -> unit
@@ -31,9 +30,10 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter
val find_tag_start : GText.tag -> GText.iter -> GText.iter
val find_tag_stop : GText.tag -> GText.iter -> GText.iter
-val select_file_for_open : title:string -> ?filename:string -> unit -> string option
+val select_file_for_open :
+ title:string -> ?filter:bool -> ?parent:GWindow.window -> ?filename:string -> unit -> string option
val select_file_for_save :
- title:string -> ?filename:string -> unit -> string option
+ title:string -> ?parent:GWindow.window -> ?filename:string -> unit -> string option
val try_convert : string -> string
val try_export : string -> string -> bool
val stock_to_widget :
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index f2913b1d1d..d85d87142c 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -52,7 +52,7 @@ let pr_key t =
type action =
| Action of string * string
| Callback of (gui -> unit)
- | Edit of (status -> GSourceView2.source_buffer -> GText.iter ->
+ | Edit of (status -> GSourceView3.source_buffer -> GText.iter ->
(string -> string -> unit) -> status)
| Motion of (status -> GText.iter -> GText.iter * status)
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4aa8c92f73..69dbc0b235 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -12,10 +12,10 @@ open Configwin
let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
-let lang_manager = GSourceView2.source_language_manager ~default:true
+let lang_manager = GSourceView3.source_language_manager ~default:true
let () = lang_manager#set_search_path
((Minilib.coqide_data_dirs ())@lang_manager#search_path)
-let style_manager = GSourceView2.source_style_scheme_manager ~default:true
+let style_manager = GSourceView3.source_style_scheme_manager ~default:true
let () = style_manager#set_search_path
((Minilib.coqide_data_dirs ())@style_manager#search_path)
@@ -73,11 +73,11 @@ object (self)
method default = default
end
-let stick (pref : 'a preference) (obj : #GObj.widget as 'obj)
+let stick (pref : 'a preference) (obj : < connect : #GObj.widget_signals ; .. >)
(cb : 'a -> unit) =
let _ = cb pref#get in
let p_id = pref#connect#changed ~callback:(fun v -> cb v) in
- let _ = obj#misc#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in
+ let _ = obj#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in
()
(** Useful marshallers *)
@@ -366,33 +366,6 @@ let text_font =
in
new preference ~name:["text_font"] ~init ~repr:Repr.(string)
-let is_standard_doc_url url =
- let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
- let n = String.length Coq_config.wwwcoq in
- let n' = String.length Coq_config.wwwrefman in
- url = Coq_config.localwwwrefman ||
- url = Coq_config.wwwrefman ||
- url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
-
-let doc_url =
-object
- inherit [string] preference
- ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string)
- as super
-
- method! set v =
- if not (is_standard_doc_url v) &&
- v <> use_default_doc_url &&
- (* Extra hack to support links to last released doc version *)
- v <> Coq_config.wwwcoq ^ "doc" &&
- v <> Coq_config.wwwcoq ^ "doc/"
- then super#set v
-
-end
-
-let library_url =
- new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string)
-
let show_toolbar =
new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool)
@@ -440,8 +413,11 @@ let attach_fg (pref : string preference) (tag : GText.tag) =
let processing_color =
new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)
+let incompletely_processed_color =
+ new preference ~name:["incompletely_processed_color"] ~init:"light sky blue" ~repr:Repr.(string)
+
let _ = attach_bg processing_color Tags.Script.to_process
-let _ = attach_bg processing_color Tags.Script.incomplete
+let _ = attach_bg incompletely_processed_color Tags.Script.incomplete
let tags = ref Util.String.Map.empty
@@ -602,7 +578,7 @@ object (self)
| None -> set#set_active true
| Some c ->
set#set_active false;
- but#set_color (Tags.color_of_string c)
+ but#set_color (Gdk.Color.color_parse c)
in
track tag.tag_bg_color bg_color bg_unset;
track tag.tag_fg_color fg_color fg_unset;
@@ -614,7 +590,7 @@ object (self)
method tag =
let get but set =
if set#active then None
- else Some (Tags.string_of_color but#color)
+ else Some (Gdk.Color.color_to_string but#color)
in
{
tag_bg_color = get bg_color bg_unset;
@@ -692,7 +668,7 @@ let configure ?(apply=(fun () -> ())) parent =
let cmd_coqtop =
string
~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s))
- " coqtop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in
+ " coqidetop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in
let cmd_coqc = pstring " coqc" cmd_coqc in
let cmd_make = pstring " make" cmd_make in
let cmd_coqmakefile = pstring "coqmakefile" cmd_coqmakefile in
@@ -718,7 +694,7 @@ let configure ?(apply=(fun () -> ())) parent =
let config_color =
let box = GPack.vbox () in
- let table = GPack.table
+ let grid = GPack.grid
~row_spacings:5
~col_spacings:5
~border_width:2
@@ -730,19 +706,19 @@ let configure ?(apply=(fun () -> ())) parent =
in
let iter i (text, pref) =
let label = GMisc.label
- ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:i) ()
+ ~text ~packing:(grid#attach (*~expand:`X*) ~left:0 ~top:i) ()
in
let () = label#set_xalign 0. in
let button = GButton.color_button
- ~color:(Tags.color_of_string pref#get)
- ~packing:(table#attach ~left:1 ~top:i) ()
+ ~color:(Gdk.Color.color_parse pref#get)
+ ~packing:(grid#attach ~left:1 ~top:i) ()
in
let _ = button#connect#color_set ~callback:begin fun () ->
- pref#set (Tags.string_of_color button#color)
+ pref#set (Gdk.Color.color_to_string button#color)
end in
let reset _ =
pref#reset ();
- button#set_color Tags.(color_of_string pref#get)
+ button#set_color (Gdk.Color.color_parse pref#get)
in
let _ = reset_button#connect#clicked ~callback:reset in
()
@@ -751,6 +727,7 @@ let configure ?(apply=(fun () -> ())) parent =
("Background color", background_color);
("Background color of processed text", processed_color);
("Background color of text being processed", processing_color);
+ ("Background color of incompletely processed Qed", incompletely_processed_color);
("Background color of errors", error_color);
("Foreground color of errors", error_fg_color);
] in
@@ -767,7 +744,7 @@ let configure ?(apply=(fun () -> ())) parent =
~packing:(box#pack ~expand:true)
()
in
- let table = GPack.table
+ let grid = GPack.grid
~row_spacings:5
~col_spacings:5
~border_width:2
@@ -777,13 +754,13 @@ let configure ?(apply=(fun () -> ())) parent =
let cb = ref [] in
let iter text tag =
let label = GMisc.label
- ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:!i) ()
+ ~text ~packing:(grid#attach (*~expand:`X*) ~left:0 ~top:!i) ()
in
let () = label#set_xalign 0. in
let button = tag_button () in
let callback () = tag#set button#tag in
button#set_tag tag#get;
- table#attach ~left:1 ~top:!i button#coerce;
+ grid#attach ~left:1 ~top:!i button#coerce;
incr i;
cb := callback :: !cb;
in
@@ -948,32 +925,7 @@ let configure ?(apply=(fun () -> ())) parent =
else cmd_browse#get])
cmd_browse#get
in
- let doc_url =
- let predefined = [
- "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]);
- Coq_config.wwwrefman;
- use_default_doc_url
- ] in
- combo
- "Manual URL"
- ~f:doc_url#set
- ~new_allowed: true
- (predefined@[if List.mem doc_url#get predefined then ""
- else doc_url#get])
- doc_url#get in
- let library_url =
- let predefined = [
- "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]);
- Coq_config.wwwstdlib
- ] in
- combo
- "Library URL"
- ~f:(fun s -> library_url#set s)
- ~new_allowed: true
- (predefined@[if List.mem library_url#get predefined then ""
- else library_url#get])
- library_url#get
- in
+(*
let automatic_tactics =
strings
~f:automatic_tactics#set
@@ -982,12 +934,14 @@ let configure ?(apply=(fun () -> ())) parent =
automatic_tactics#get
in
+*)
let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in
let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
vertical_tabs;opposite_tabs] in
+(*
let add_user_query () =
let input_string l v =
match GToolbox.input_string ~title:l v with
@@ -1017,6 +971,7 @@ let configure ?(apply=(fun () -> ())) parent =
user_queries#get
in
+*)
(* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
(shame on Benjamin) *)
@@ -1039,13 +994,15 @@ let configure ?(apply=(fun () -> ())) parent =
Section("Appearance", Some `PREFERENCES, [window_width; window_height]);
Section("Externals", None,
[cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
- cmd_print;cmd_editor;cmd_browse;doc_url;library_url]);
+ cmd_print;cmd_editor;cmd_browse]);
+(*
Section("Tactics Wizard", None,
[automatic_tactics]);
+*)
Section("Shortcuts", Some `PREFERENCES,
[modifiers_valid; modifier_for_tactics;
modifier_for_templates; modifier_for_display; modifier_for_navigation;
- modifier_for_queries; user_queries]);
+ modifier_for_queries (*; user_queries *)]);
Section("Misc", Some `ADD,
misc)]
in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 7ed6a40bdb..8745c2ae91 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -8,8 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val lang_manager : GSourceView2.source_language_manager
-val style_manager : GSourceView2.source_style_scheme_manager
+val lang_manager : GSourceView3.source_language_manager
+val style_manager : GSourceView3.source_style_scheme_manager
type project_behavior = Ignore_args | Append_args | Subst_args
type inputenc = Elocale | Eutf8 | Emanual of string
@@ -74,8 +74,6 @@ val modifiers_valid : string preference
val cmd_browse : string preference
val cmd_editor : string preference
val text_font : string preference
-val doc_url : string preference
-val library_url : string preference
val show_toolbar : bool preference
val contextual_menus_on_goal : bool preference
val window_width : int preference
@@ -110,6 +108,6 @@ val load_pref : unit -> unit
val configure : ?apply:(unit -> unit) -> GWindow.window -> unit
val stick : 'a preference ->
- (#GObj.widget as 'obj) -> ('a -> unit) -> unit
+ < connect : #GObj.widget_signals ; .. > -> ('a -> unit) -> unit
val use_default_doc_url : string
diff --git a/ide/session.ml b/ide/session.ml
index e2427a9b51..fd21515ca5 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -47,7 +47,7 @@ type session = {
}
let create_buffer () =
- let buffer = GSourceView2.source_buffer
+ let buffer = GSourceView3.source_buffer
~tag_table:Tags.Script.table
~highlight_matching_brackets:true
?language:(lang_manager#language source_language#get)
@@ -257,7 +257,7 @@ let make_table_widget ?sort cd cb =
~model:store ~packing:frame#add () in
let () = data#set_headers_visible true in
let () = data#set_headers_clickable true in
- let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in
+ let refresh clr = data#misc#modify_bg [`NORMAL, `NAME clr] in
let _ = background_color#connect#changed ~callback:refresh in
let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in
let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
@@ -442,11 +442,11 @@ let build_layout (sn:session) =
let eval_paned = GPack.paned `HORIZONTAL ~border_width:5
~packing:(session_box#pack ~expand:true) () in
let script_frame = GBin.frame ~shadow_type:`IN
- ~packing:eval_paned#add1 () in
+ ~packing:(eval_paned#pack1 ~shrink:false) () in
let script_scroll = GBin.scrolled_window
~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in
let state_paned = GPack.paned `VERTICAL
- ~packing:eval_paned#add2 () in
+ ~packing:(eval_paned#pack2 ~shrink:false) () in
(* Proof buffer. *)
diff --git a/ide/tags.ml b/ide/tags.ml
index 60195e8acb..e9dbcb9e67 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -24,7 +24,7 @@ struct
let error_bg = make_tag table ~name:"error_bg" []
let to_process = make_tag table ~name:"to_process" []
let processed = make_tag table ~name:"processed" []
- let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true]
+ let incomplete = make_tag table ~name:"incomplete" []
let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
let ephemere =
@@ -48,13 +48,3 @@ struct
let warning = make_tag table ~name:"warning" [`FOREGROUND "orange"]
let item = make_tag table ~name:"item" [`WEIGHT `BOLD]
end
-
-let string_of_color clr =
- let r = Gdk.Color.red clr in
- let g = Gdk.Color.green clr in
- let b = Gdk.Color.blue clr in
- Printf.sprintf "#%04X%04X%04X" r g b
-
-let color_of_string s =
- let colormap = Gdk.Color.get_system_colormap () in
- Gdk.Color.alloc ~colormap (`NAME s)
diff --git a/ide/tags.mli b/ide/tags.mli
index 3194f87971..1df934fddf 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -41,6 +41,3 @@ sig
val warning : GText.tag
val item : GText.tag
end
-
-val string_of_color : Gdk.color -> string
-val color_of_string : string -> Gdk.color
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 06281d6287..be400a5f2d 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,10 +100,10 @@ object(self)
router#register_route route_id result;
r_bin#add_with_viewport (result :> GObj.widget);
views <- (frame#coerce, result, combo#entry) :: views;
- let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
+ let cb clr = result#misc#modify_bg [`NORMAL, `NAME clr] in
let _ = background_color#connect#changed ~callback:cb in
let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
- let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
+ let cb ft = result#misc#modify_font (GPango.font_description_from_string ft) in
stick text_font result cb;
result#misc#set_can_focus true; (* false causes problems for selection *)
let callback () =
@@ -163,8 +163,8 @@ object(self)
frame#visible
method private refresh_color clr =
- let clr = Tags.color_of_string clr in
- let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in
+ let clr = Gdk.Color.color_parse clr in
+ let iter (_,view,_) = view#misc#modify_bg [`NORMAL, `COLOR clr] in
List.iter iter views
initializer
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml
index d753687077..755a42eadd 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/wg_Detachable.ml
@@ -15,6 +15,9 @@ class type detachable_signals =
method detached : callback:(GObj.widget -> unit) -> unit
end
+(* Cannot do a local warning in 4.05.0, fixme when we use a newer
+ OCaml to avoid the warning in the method itself. *)
+[@@@ocaml.warning "-7"]
class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) =
object(self)
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 7d2d7da570..fe079e8a9e 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -14,10 +14,10 @@ class finder name (view : GText.view) =
let widget = Wg_Detachable.detachable
~title:(Printf.sprintf "Find & Replace (%s)" name) () in
- let replace_box = GPack.table ~columns:4 ~rows:2 ~homogeneous:false
+ let replace_box = GPack.grid (* ~columns:4 ~rows:2 *) ~col_homogeneous:false ~row_homogeneous:false
~packing:widget#add () in
let hb = GPack.hbox ~packing:(replace_box#attach
- ~left:1 ~top:0 ~expand:`X ~fill:`X) () in
+ ~left:1 ~top:0 (*~expand:`X ~fill:`X*)) () in
let use_regex =
GButton.check_button ~label:"Regular expression"
~packing:(hb#pack ~expand:false ~fill:true ~padding:3) () in
@@ -26,25 +26,25 @@ class finder name (view : GText.view) =
~packing:(hb#pack ~expand:false ~fill:true ~padding:3) () in
let _ = GMisc.label ~text:"Find:" ~xalign:1.0
~packing:(replace_box#attach
- ~xpadding:3 ~ypadding:3 ~left:0 ~top:1 ~fill:`X) () in
+ (*~xpadding:3 ~ypadding:3*) ~left:0 ~top:1 (*~fill:`X*)) () in
let _ = GMisc.label ~text:"Replace:" ~xalign:1.0
~packing:(replace_box#attach
- ~xpadding:3 ~ypadding:3 ~left:0 ~top:2 ~fill:`X) () in
+ (* ~xpadding:3 ~ypadding:3*) ~left:0 ~top:2 (*~fill:`X*)) () in
let find_entry = GEdit.entry ~editable:true
~packing:(replace_box#attach
- ~xpadding:3 ~ypadding:3 ~left:1 ~top:1 ~expand:`X ~fill:`X) () in
+ (*~xpadding:3 ~ypadding:3*) ~left:1 ~top:1 (*~expand:`X ~fill:`X*)) () in
let replace_entry = GEdit.entry ~editable:true
~packing:(replace_box#attach
- ~xpadding:3 ~ypadding:3 ~left:1 ~top:2 ~expand:`X ~fill:`X) () in
+ (*~xpadding:3 ~ypadding:3*) ~left:1 ~top:2 (*~expand:`X ~fill:`X*)) () in
let next_button = GButton.button ~label:"_Next" ~use_mnemonic:true
- ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:2 ~top:1) () in
+ ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:2 ~top:1) () in
let previous_button = GButton.button ~label:"_Previous" ~use_mnemonic:true
- ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:3 ~top:1) () in
+ ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:3 ~top:1) () in
let replace_button = GButton.button ~label:"_Replace" ~use_mnemonic:true
- ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:2 ~top:2) () in
+ ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:2 ~top:2) () in
let replace_all_button =
GButton.button ~label:"Replace _All" ~use_mnemonic:true
- ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:3 ~top:2) () in
+ ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:3 ~top:2) () in
object (self)
val mutable last_found = None
@@ -135,13 +135,13 @@ class finder name (view : GText.view) =
view#buffer#end_user_action ()
method private set_not_found () =
- find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"];
+ find_entry#misc#modify_bg [`NORMAL, `NAME "#F7E6E6"];
method private set_found () =
- find_entry#misc#modify_base [`NORMAL, `NAME "#BAF9CE"]
+ find_entry#misc#modify_bg [`NORMAL, `NAME "#BAF9CE"]
method private set_normal () =
- find_entry#misc#modify_base [`NORMAL, `NAME "white"]
+ find_entry#misc#modify_bg [`NORMAL, `NAME "white"]
method private find_from backward ?(wrapped=false) (starti : GText.iter) =
let found =
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 6b09b344b5..7943b099fc 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -42,7 +42,7 @@ class type message_view =
end
let message_view () : message_view =
- let buffer = GSourceView2.source_buffer
+ let buffer = GSourceView3.source_buffer
~highlight_matching_brackets:true
~tag_table:Tags.Message.table ()
in
@@ -50,7 +50,7 @@ let message_view () : message_view =
let box = GPack.vbox () in
let scroll = GBin.scrolled_window
~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in
- let view = GSourceView2.source_view
+ let view = GSourceView3.source_view
~source_buffer:buffer ~packing:scroll#add
~editable:false ~cursor_visible:false ~wrap_mode:`WORD ()
in
@@ -59,10 +59,10 @@ let message_view () : message_view =
let _ = buffer#add_selection_clipboard default_clipboard in
let () = view#set_left_margin 2 in
view#misc#show ();
- let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
+ let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in
let _ = background_color#connect#changed ~callback:cb in
let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
- let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
+ let cb ft = view#misc#modify_font (GPango.font_description_from_string ft) in
stick text_font view cb;
(* Inserts at point, advances the mark *)
diff --git a/ide/wg_Notebook.mli b/ide/wg_Notebook.mli
index 85ecdf6cdd..9447b21c0b 100644
--- a/ide/wg_Notebook.mli
+++ b/ide/wg_Notebook.mli
@@ -28,11 +28,10 @@ val create :
('a -> GObj.widget option * GObj.widget option * GObj.widget) ->
('a -> unit) ->
?enable_popup:bool ->
- ?homogeneous_tabs:bool ->
+ ?group_name:string ->
?scrollable:bool ->
?show_border:bool ->
?show_tabs:bool ->
- ?tab_border:int ->
?tab_pos:Gtk.Tags.position ->
?border_width:int ->
?width:int ->
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 9be562d3ed..596df227b7 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -193,21 +193,21 @@ let display mode (view : #GText.view_skel) goals hints evars =
let proof_view () =
- let buffer = GSourceView2.source_buffer
+ let buffer = GSourceView3.source_buffer
~highlight_matching_brackets:true
~tag_table:Tags.Proof.table ()
in
let text_buffer = new GText.buffer buffer#as_buffer in
- let view = GSourceView2.source_view
+ let view = GSourceView3.source_view
~source_buffer:buffer ~editable:false ~wrap_mode:`WORD ()
in
let () = Gtk_parsing.fix_double_click view in
let default_clipboard = GData.clipboard Gdk.Atom.primary in
let _ = buffer#add_selection_clipboard default_clipboard in
- let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
+ let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in
let _ = background_color#connect#changed ~callback:cb in
let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
- let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
+ let cb ft = view#misc#modify_font (GPango.font_description_from_string ft) in
stick text_font view cb;
let pf = object
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 5e26c50797..e95176bf4d 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -284,12 +284,12 @@ end
class script_view (tv : source_view) (ct : Coq.coqtop) =
-let view = new GSourceView2.source_view (Gobject.unsafe_cast tv) in
+let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in
let completion = new Wg_Completion.complete_model ct view#buffer in
let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in
object (self)
- inherit GSourceView2.source_view (Gobject.unsafe_cast tv)
+ inherit GSourceView3.source_view (Gobject.unsafe_cast tv)
val undo_manager = new undo_manager view#buffer
@@ -461,7 +461,7 @@ object (self)
in
let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
(* Plug on preferences *)
- let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
+ let cb clr = self#misc#modify_bg [`NORMAL, `NAME clr] in
let _ = background_color#connect#changed ~callback:cb in
let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
@@ -484,24 +484,24 @@ object (self)
stick tab_length self self#set_tab_width;
stick auto_complete self self#set_auto_complete;
- let cb ft = self#misc#modify_font (Pango.Font.from_string ft) in
+ let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in
stick text_font self cb;
()
end
-let script_view ct ?(source_buffer:GSourceView2.source_buffer option) ?draw_spaces =
- GtkSourceView2.SourceView.make_params [] ~cont:(
+let script_view ct ?(source_buffer:GSourceView3.source_buffer option) ?draw_spaces =
+ GtkSourceView3.SourceView.make_params [] ~cont:(
GtkText.View.make_params ~cont:(
GContainer.pack_container ~create:
(fun pl ->
let w = match source_buffer with
- | None -> GtkSourceView2.SourceView.new_ ()
- | Some buf -> GtkSourceView2.SourceView.new_with_buffer
+ | None -> GtkSourceView3.SourceView.new_ ()
+ | Some buf -> GtkSourceView3.SourceView.new_with_buffer
(Gobject.try_cast buf#as_buffer "GtkSourceBuffer")
in
let w = Gobject.unsafe_cast w in
Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
- Gaux.may ~f:(GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
+ Gaux.may ~f:(GtkSourceView3.SourceView.set_draw_spaces w) draw_spaces;
((new script_view w ct) : script_view))))
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index be6510dbe2..ef7e92ff38 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -14,7 +14,7 @@ type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj
class script_view : source_view -> Coq.coqtop ->
object
- inherit GSourceView2.source_view
+ inherit GSourceView3.source_view
method undo : unit -> unit
method redo : unit -> unit
method clear_undo : unit -> unit
@@ -31,8 +31,8 @@ object
end
val script_view : Coq.coqtop ->
- ?source_buffer:GSourceView2.source_buffer ->
- ?draw_spaces:SourceView2Enums.source_draw_spaces_flags list ->
+ ?source_buffer:GSourceView3.source_buffer ->
+ ?draw_spaces:SourceView3Enums.source_draw_spaces_flags list ->
?auto_indent:bool ->
?highlight_current_line:bool ->
?indent_on_tab:bool ->
@@ -42,7 +42,7 @@ val script_view : Coq.coqtop ->
?show_line_marks:bool ->
?show_line_numbers:bool ->
?show_right_margin:bool ->
- ?smart_home_end:SourceView2Enums.source_smart_home_end_type ->
+ ?smart_home_end:SourceView3Enums.source_smart_home_end_type ->
?tab_width:int ->
?editable:bool ->
?cursor_visible:bool ->
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 3b2572f9d2..2e5de64254 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -8,8 +8,10 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+(*
open Util
open Preferences
+*)
type color = GDraw.color
@@ -22,6 +24,7 @@ object
method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
end
+(*
let i2f = float_of_int
let f2i = int_of_float
@@ -32,14 +35,14 @@ let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with
| `RGB (r1, g1, b1), `RGB (r2, g2, b2) -> r1 = r2 && g1 = g2 && b1 = b2
| `WHITE, `WHITE -> true
| _ -> false
-
+*)
class type segment_signals =
object
inherit GObj.misc_signals
inherit GUtil.add_ml_signals
method clicked : callback:(int -> unit) -> GtkSignal.id
end
-
+(*
class segment_signals_impl obj (clicked : 'a GUtil.signal) : segment_signals =
object
val after = false
@@ -47,11 +50,14 @@ object
inherit GUtil.add_ml_signals obj [clicked#disconnect]
method clicked = clicked#connect ~after
end
+*)
class segment () =
let box = GBin.frame () in
+(*
let eventbox = GBin.event_box ~packing:box#add () in
let draw = GMisc.image ~packing:eventbox#add () in
+*)
object (self)
inherit GObj.widget box#as_widget
@@ -60,11 +66,13 @@ object (self)
val mutable height = 20
val mutable model : model option = None
val mutable default : color = `WHITE
+(*
val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
+*)
val clicked = new GUtil.signal ()
val mutable need_refresh = false
val refresh_timer = Ideutils.mktimer ()
-
+(*
initializer
box#misc#set_size_request ~height ();
let cb rect =
@@ -95,17 +103,18 @@ object (self)
draw#set_pixmap pixmap;
refresh_timer.Ideutils.run ~ms:300
~callback:(fun () -> if need_refresh then self#refresh (); true)
-
+*)
method set_model md =
model <- Some md;
let changed_cb = function
| `INSERT | `REMOVE ->
if self#misc#visible then need_refresh <- true
| `SET (i, color) ->
- if self#misc#visible then self#fill_range color i (i + 1)
+ ()
+(* if self#misc#visible then self#fill_range color i (i + 1)*)
in
md#changed ~callback:changed_cb
-
+(*
method private fill_range color i j = match model with
| None -> ()
| Some md ->
@@ -150,5 +159,6 @@ object (self)
method connect =
new segment_signals_impl box#as_widget clicked
+*)
end
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index 07f545fee7..84d487f35f 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -31,7 +31,9 @@ class segment : unit ->
inherit GObj.widget
val obj : Gtk.widget Gtk.obj
method set_model : model -> unit
+(*
method connect : segment_signals
method default_color : color
method set_default_color : color -> unit
+*)
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:51:12 +0000