From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- ide/MacOS/Info.plist.template | 2 +- ide/MacOS/default_accel_map | 1 - ide/coq.lang | 59 ++++++++++++++++++---------------- ide/coqOps.ml | 42 ++++++++++++++++--------- ide/coq_commands.ml | 2 -- ide/coqide.ml | 73 ++++++++++++++++++++++++++++--------------- ide/coqide_ui.ml | 1 - ide/gtk_parsing.ml | 13 ++++++++ ide/ide_slave.ml | 8 ++--- ide/ideutils.ml | 50 ++++++++++++++++------------- ide/ideutils.mli | 4 +-- ide/preferences.ml | 39 +++++++++++++++++------ ide/preferences.mli | 2 ++ ide/project_file.ml4 | 22 +++++-------- ide/session.ml | 41 +++++++++++++++++------- ide/session.mli | 1 + ide/tags.ml | 26 +++++++++++---- ide/tags.mli | 13 ++++++-- ide/wg_Find.ml | 14 ++++++--- ide/wg_MessageView.ml | 31 +++++++++++++++++- ide/wg_MessageView.mli | 9 ++++++ ide/wg_ProofView.ml | 5 +++ ide/wg_ProofView.mli | 1 + ide/wg_ScriptView.ml | 13 ++++++-- ide/wg_Segment.ml | 31 +++++++++++++++++- ide/wg_Segment.mli | 8 +++++ 26 files changed, 357 insertions(+), 154 deletions(-) (limited to 'ide') diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template index fd80c839..e224e812 100644 --- a/ide/MacOS/Info.plist.template +++ b/ide/MacOS/Info.plist.template @@ -66,7 +66,7 @@ CFBundleGetInfoString Coq_vVERSION NSHumanReadableCopyright - Copyright 1999-2014, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS + Copyright 1999-2015, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS CFBundleHelpBookFolder share/doc/coq/html/ CFAppleHelpAnchor diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 6f474eb1..47612cdf 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -247,7 +247,6 @@ ; (gtk_accel_path "/Tactics/Tactic constructor" "") ; (gtk_accel_path "/Tactics/Tactic elim -- with" "") ; (gtk_accel_path "/Templates/Template Identity Coercion" "") -; (gtk_accel_path "/Queries/Whelp Locate" "") (gtk_accel_path "/View/Display all low-level contents" "l") ; (gtk_accel_path "/Tactics/Tactic right" "") ; (gtk_accel_path "/Edit/Find Previous" "F3") diff --git a/ide/coq.lang b/ide/coq.lang index 608a4aea..65150d6a 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -22,19 +22,19 @@ - \s + \s+ [_\p{L}] [_\p{L}'\pN] \%{first_ident_char}\%{ident_char}* (\%{ident}\.)*\%{ident} [-+*{}] \.(\s|\z) - (Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure) - (Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?) - (((Local)|(Global))\%{space}+)? - (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property) - (Qed)|(Defined)|(Admitted)|(Abort) - ((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))|(?'gal2'Goal) + Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion + Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)? + ((Local|Global)\%{space})? + Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property + Qed|Defined|Admitted|Abort|Save + ((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal) "" @@ -97,7 +97,6 @@ then else return - using Prop @@ -113,7 +112,7 @@ - Proof(\%{dot_sep}|\%{space}+(using)|\%{space}+(with)) + Proof(\%{dot_sep}|\%{space}using|\%{space}with) \%{end_proof}\%{dot_sep} @@ -157,17 +156,18 @@ Eval Load Undo + (Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist) Print - Save Comments - Solve\%{space}+Obligation - ((Uns)|(S))et(\%{space}+\%{ident})+ - (\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation + Solve\%{space}Obligation + (Uns|S)et(\%{space}\%{ident})+ + (\%{locality}|(Reserved|Tactic)\%{space})?Notation \%{locality}Infix - (Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist) + Declare\%{space}ML\%{space}Module + Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON) - \%{locality}Hint\%{space}+ + \%{locality}Hint\%{space} Resolve Immediate Constructors @@ -178,35 +178,40 @@ Rewrite - \%{space}+Scope + \%{space}Scope \%{locality}Open \%{locality}Close Bind Delimit - \%{space}+(?'qua'\%{qualit}) + \%{space}(?'qua'\%{qualit}) Chapter - Combined\%{space}+Scheme + Combined\%{space}Scheme + Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for End Section + Module(\%{space}Type)? + Declare\%{space}Module(\%{space}(Import|Export))? + About Arguments - Implicit\%{space}+Arguments - Import + Implicit\%{space}Arguments Include - Export - Require(\%{space}+((Import)|(Export)))? - (Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))? - Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive) + Extract\%{space}((Inlined\%{space})?Constant|Inductive) - - (?'qua_list'(\%{space}+\%{qualit})+) - Typeclasses (Transparent)|(Opaque) + + (?'qua_list'(\%{space}\%{qualit})+) + Typeclasses (Transparent|Opaque) + Require(\%{space}(Import|Export))? + Import + Export + ((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))? + diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 52e18456..af728471 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -215,8 +215,24 @@ object(self) document_length <- pred document_length; segment#set_length document_length; in + let on_click id = + let find _ _ s = Int.equal s.index id in + let sentence = Doc.find document find in + let mark = sentence.start in + let iter = script#buffer#get_iter_at_mark mark in + (** Sentence starts tend to be at the end of a line, so we rather choose + the first non-line-ending position. *) + let rec sentence_start iter = + if iter#ends_line then sentence_start iter#forward_line + else iter + in + let iter = sentence_start iter in + script#buffer#place_cursor iter; + ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) + in let _ = (Doc.connect document)#pushed on_push in let _ = (Doc.connect document)#popped on_pop in + let _ = segment#connect#clicked on_click in () method private tooltip_callback ~x ~y ~kbd tooltip = @@ -260,21 +276,11 @@ object(self) Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop); self#print_stack; let qed_s = Doc.tip_data document in - buffer#apply_tag Tags.Script.read_only - ~start:((buffer#get_iter_at_mark qed_s.start)#forward_find_char - (fun c -> not(Glib.Unichar.isspace c))) - ~stop:(buffer#get_iter_at_mark qed_s.stop); buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop) (`NAME "stop_of_input") method private exit_focus = Minilib.log "Unfocusing"; - begin try - let { start; stop } = Doc.tip_data document in - buffer#remove_tag Tags.Script.read_only - ~start:(buffer#get_iter_at_mark start) - ~stop:(buffer#get_iter_at_mark stop) - with Doc.Empty -> () end; Doc.unfocus document; self#print_stack; begin try @@ -347,7 +353,7 @@ object(self) else if has_flag sentence `ERROR then [error_bg] else if has_flag sentence `INCOMPLETE then [incomplete] else [processed]) @ - (if [ `UNSAFE ] = sentence.flags then [unjustified] else []) + (if has_flag sentence `UNSAFE then [unjustified] else []) in List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags; List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags @@ -499,7 +505,7 @@ object(self) | Some (start, stop) -> if until n start stop then begin () - end else if start#has_tag Tags.Script.processed then begin + end else if stop#backward_char#has_tag Tags.Script.processed then begin Queue.push (`Skip (start, stop)) queue; loop n stop end else begin @@ -547,12 +553,15 @@ object(self) script#recenter_insert; match topstack with | [] -> self#show_goals_aux ?move_insert () - | (_,s) :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in + | (_,s)::_ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in let process_queue queue = let rec loop tip topstack = if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with - | `Skip(start,stop), [] -> assert false + | `Skip(start,stop), [] -> + logger Pp.Error "You muse close the proof with Qed or Admitted"; + self#discard_command_queue queue; + conclude [] | `Skip(start,stop), (_,s) :: topstack -> assert(start#equal (buffer#get_iter_at_mark s.start)); assert(stop#equal (buffer#get_iter_at_mark s.stop)); @@ -646,10 +655,13 @@ object(self) buffer#remove_tag Tags.Script.unjustified ~start ~stop; buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; + buffer#remove_tag Tags.Script.error ~start ~stop; + buffer#remove_tag Tags.Script.error_bg ~start ~stop; buffer#move_mark ~where:start (`NAME "start_of_input") end; List.iter (fun { start } -> buffer#delete_mark start) seg; - List.iter (fun { stop } -> buffer#delete_mark stop) seg + List.iter (fun { stop } -> buffer#delete_mark stop) seg; + self#print_stack (** Wrapper around the raw undo command *) method private backtrack_to_id ?(move_insert=true) (to_id, unfocus_needed) = diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 995c45c5..37e38a54 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -228,8 +228,6 @@ let state_preserving = [ "Test Printing Synth"; "Test Printing Wildcard"; - "Whelp Hint"; - "Whelp Locate"; ] diff --git a/ide/coqide.ml b/ide/coqide.ml index fa64defa..0f4cb7b0 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -84,14 +84,15 @@ let pr_exit_status = function | _ -> " failed" let make_coqtop_args = function - |None -> !sup_args + |None -> "", !sup_args |Some the_file -> let get_args f = Project_file.args_from_project f !custom_project_files prefs.project_file_name in match prefs.read_project with - |Ignore_args -> !sup_args - |Append_args -> get_args the_file @ !sup_args + |Ignore_args -> "", !sup_args + |Append_args -> + let fname, args = get_args the_file in fname, args @ !sup_args |Subst_args -> get_args the_file (** Setting drag & drop on widgets *) @@ -120,7 +121,10 @@ let set_drag (w : GObj.drag_ops) = (** Session management *) let create_session f = - let ans = Session.create f (make_coqtop_args f) in + let project_file, args = make_coqtop_args f in + if project_file <> "" then + flash_info (Printf.sprintf "Reading options from %s" project_file); + let ans = Session.create f args in let _ = set_drag ans.script#drag in ans @@ -249,11 +253,14 @@ let newfile _ = !refresh_editor_hook (); notebook#goto_page index -let load _ = - match select_file_for_open ~title:"Load file" () with +let load sn = + let filename = sn.fileops#filename in + match select_file_for_open ~title:"Load file" ?filename () with | None -> () | Some f -> FileAux.load_file f +let load = cb_on_current_term load + let save _ = on_current_term (FileAux.check_save ~saveas:false) let saveas sn = @@ -530,7 +537,7 @@ let update_status sn = | None -> "" | Some n -> ", proving " ^ n in - display ("Ready"^ if current.nanoPG then ", [μPG]" else "" ^ path ^ name); + display ("Ready"^ (if current.nanoPG then ", [μPG]" else "") ^ path ^ name); Coq.return () in Coq.bind (Coq.status ~logger:sn.messages#push false) next @@ -588,13 +595,24 @@ let get_current_word term = | Some p -> p | None -> (** Then look at the current selected word *) - if term.script#buffer#has_selection then - let (start, stop) = term.script#buffer#selection_bounds in + let buf1 = term.script#buffer in + let buf2 = term.proof#buffer in + let buf3 = term.messages#buffer in + if buf1#has_selection then + let (start, stop) = buf1#selection_bounds in + buf1#get_text ~slice:true ~start ~stop () + else if buf2#has_selection then + let (start, stop) = buf2#selection_bounds in + buf2#get_text ~slice:true ~start ~stop () + else if buf3#has_selection then + let (start, stop) = buf3#selection_bounds in + buf3#get_text ~slice:true ~start ~stop () + (** Otherwise try to find the word around the cursor *) + else + let it = term.script#buffer#get_iter_at_mark `INSERT in + let start = find_word_start it in + let stop = find_word_end start in term.script#buffer#get_text ~slice:true ~start ~stop () - (** Otherwise try to recover the clipboard *) - else match Ideutils.cb#text with - | Some t -> t - | None -> "" let print_branch c l = Format.fprintf c " | @[%a@]=> _@\n" @@ -838,10 +856,16 @@ let refresh_editor_prefs () = sn.command#refresh_font (); (* Colors *) + Tags.set_processing_color (Tags.color_of_string current.processing_color); + Tags.set_processed_color (Tags.color_of_string current.processed_color); + Tags.set_error_color (Tags.color_of_string current.error_color); + Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color); sn.script#misc#modify_base [`NORMAL, `COLOR clr]; sn.proof#misc#modify_base [`NORMAL, `COLOR clr]; - sn.messages#misc#modify_base [`NORMAL, `COLOR clr]; - sn.command#refresh_color () + sn.messages#refresh_color (); + sn.command#refresh_color (); + sn.errpage#refresh_color (); + sn.jobpage#refresh_color (); in List.iter iter_session notebook#pages @@ -1135,14 +1159,14 @@ let build_ui () = menu templates_menu [ item "Templates" ~label:"Te_mplates"; - template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "L"); + template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "J"); template_item ("Theorem new_theorem : .\nProof.\n\nSave.\n", 8,11, "T"); template_item ("Definition ident := .\n", 11,5, "E"); template_item ("Inductive ident : :=\n | : .\n", 10,5, "I"); template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F"); template_item ("Scheme new_scheme := Induction for _ Sort _\n" ^ "with _ := Induction for _ Sort _.\n", 7,10, "S"); - item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"C") + item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"M") ~callback:match_callback ]; alpha_items templates_menu "Template" Coq_commands.commands; @@ -1150,13 +1174,12 @@ let build_ui () = let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in menu queries_menu [ item "Queries" ~label:"_Queries"; - qitem "Search" (Some "F2"); - qitem "Check" (Some "F3"); - qitem "Print" (Some "F4"); - qitem "About" (Some "F5"); - qitem "Locate" None; - qitem "Print Assumptions" None; - qitem "Whelp Locate" None; + qitem "Search" (Some "K"); + qitem "Check" (Some "C"); + qitem "Print" (Some "P"); + qitem "About" (Some "A"); + qitem "Locate" (Some "L"); + qitem "Print Assumptions" (Some "N"); ]; menu tools_menu [ @@ -1314,8 +1337,6 @@ let build_ui () = refresh_tabs_hook := refresh_notebook_pos; (* Color configuration *) - Tags.set_processing_color (Tags.color_of_string prefs.processing_color); - Tags.set_processed_color (Tags.color_of_string prefs.processed_color); Tags.Script.incomplete#set_property (`BACKGROUND_STIPPLE (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index af71b1e7..edfe28b2 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -119,7 +119,6 @@ let init () = - diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index abbd7e6d..79ccf61a 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -166,3 +166,16 @@ let find_nearest_backward (cursor:GText.iter) targets = | None -> raise Not_found | Some nearest -> nearest +(** On double-click on a view, select the whole word. This is a workaround for + a deficient word handling in TextView. *) +let fix_double_click self = + let callback ev = match GdkEvent.get_type ev with + | `TWO_BUTTON_PRESS -> + let iter = self#buffer#get_iter `INSERT in + let start, stop = get_word_around iter in + let () = self#buffer#move_mark `INSERT ~where:start in + let () = self#buffer#move_mark `SEL_BOUND ~where:stop in + true + | _ -> false + in + ignore (self#event#connect#button_press ~callback) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index ac38f1ea..dc52ea9a 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -123,7 +123,7 @@ let annotate phrase = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in Vernac.parse_sentence (pa,None) in - let (_, _, xml) = + let (_, xml) = Richprinter.richpp_vernac ast in xml @@ -327,14 +327,14 @@ let handle_exn (e, info) = let loc_of e = match Loc.get_loc e with | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) | _ -> None in - let mk_msg e = read_stdout ()^"\n"^string_of_ppcmds (Errors.print e) in + let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in match e with | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" | e -> match Stateid.get info with - | Some (valid, _) -> valid, loc_of info, mk_msg e - | None -> dummy, loc_of info, mk_msg e + | Some (valid, _) -> valid, loc_of info, mk_msg () + | None -> dummy, loc_of info, mk_msg () let init = let initialized = ref false in diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d2305b58..67e4bdb0 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -132,8 +132,6 @@ let mktimer () = with Glib.GError _ -> ()); timer := None) } -let last_dir = ref "" - let filter_all_files () = GFile.filter ~name:"All" ~patterns:["*"] () @@ -142,8 +140,11 @@ let filter_coq_files () = GFile.filter ~name:"Coq source code" ~patterns:[ "*.v"] () -let select_file_for_open ~title () = - let file = ref None in +let current_dir () = match current.project_path with +| None -> "" +| Some dir -> dir + +let select_file_for_open ~title ?filename () = let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title () in @@ -152,19 +153,22 @@ let select_file_for_open ~title () = file_chooser#add_filter (filter_coq_files ()); file_chooser#add_filter (filter_all_files ()); file_chooser#set_default_response `OPEN; - ignore (file_chooser#set_current_folder !last_dir); - begin match file_chooser#run () with + let dir = match filename with + | None -> current_dir () + | Some f -> Filename.dirname f in + ignore (file_chooser#set_current_folder dir); + let file = + match file_chooser#run () with | `OPEN -> begin - file := file_chooser#filename; - match !file with - | None -> () - | Some s -> last_dir := Filename.dirname s; + match file_chooser#filename with + | None -> None + | Some _ as f -> + current.project_path <- file_chooser#current_folder; f end - | `DELETE_EVENT | `CANCEL -> () - end ; + | `DELETE_EVENT | `CANCEL -> None in file_chooser#destroy (); - !file + file let select_file_for_save ~title ?filename () = let file = ref None in @@ -175,13 +179,10 @@ let select_file_for_save ~title ?filename () = file_chooser#add_select_button_stock `SAVE `SAVE ; file_chooser#add_filter (filter_coq_files ()); file_chooser#add_filter (filter_all_files ()); - (* this line will be used when a lablgtk >= 2.10.0 is the default - on most distributions: - file_chooser#set_do_overwrite_confirmation true; - *) + file_chooser#set_do_overwrite_confirmation true; file_chooser#set_default_response `SAVE; let dir,filename = match filename with - |None -> !last_dir, "" + |None -> current_dir (), "" |Some f -> Filename.dirname f, Filename.basename f in ignore (file_chooser#set_current_folder dir); @@ -192,7 +193,7 @@ let select_file_for_save ~title ?filename () = file := file_chooser#filename; match !file with None -> () - | Some s -> last_dir := Filename.dirname s; + | Some s -> current.project_path <- file_chooser#current_folder end | `DELETE_EVENT | `CANCEL -> () end ; @@ -246,7 +247,14 @@ let coqtop_path () = let i = Str.search_backward (Str.regexp_string "coqide") prog pos in String.blit "coqtop" 0 prog i 6; - if Sys.file_exists prog then prog else "coqtop" + if Sys.file_exists prog then prog + else + let in_macos_bundle = + Filename.concat + (Filename.dirname prog) + (Filename.concat "../Resources/bin" (Filename.basename prog)) + in if Sys.file_exists in_macos_bundle then in_macos_bundle + else "coqtop" with Not_found -> "coqtop" in file @@ -279,7 +287,7 @@ let default_logger level message = (** {6 File operations} *) -(** A customized [stat] function. Exceptions are catched. *) +(** A customized [stat] function. Exceptions are caught. *) type stats = MTime of float | NoSuchFile | OtherError diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 8269582d..1fb30e4d 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -29,7 +29,7 @@ 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 -> unit -> string option +val select_file_for_open : title:string -> ?filename:string -> unit -> string option val select_file_for_save : title:string -> ?filename:string -> unit -> string option val try_convert : string -> string @@ -71,7 +71,7 @@ val default_logger : Pp.message_level -> string -> unit (** {6 I/O operations} *) -(** A customized [stat] function. Exceptions are catched. *) +(** A customized [stat] function. Exceptions are caught. *) type stats = MTime of float | NoSuchFile | OtherError val stat : string -> stats diff --git a/ide/preferences.ml b/ide/preferences.ml index c8506132..c59642d3 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -105,6 +105,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; + mutable project_path : string option; mutable encoding : inputenc; @@ -144,6 +145,7 @@ type pref = mutable processing_color : string; mutable processed_color : string; mutable error_color : string; + mutable error_fg_color : string; mutable dynamic_word_wrap : bool; mutable show_line_number : bool; @@ -179,8 +181,9 @@ let current = { source_language = "coq"; source_style = "coq_style"; - read_project = Ignore_args; + read_project = Append_args; project_file_name = "_CoqProject"; + project_path = None; encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale; @@ -220,10 +223,11 @@ let current = { vertical_tabs = false; opposite_tabs = false; - background_color = "cornsilk"; - processed_color = "light green"; - processing_color = "light blue"; - error_color = "#FFCCCC"; + background_color = Tags.default_color; + processed_color = Tags.default_processed_color; + processing_color = Tags.default_processing_color; + error_color = Tags.default_error_color; + error_fg_color = Tags.default_error_fg_color; dynamic_word_wrap = false; show_line_number = false; @@ -263,6 +267,7 @@ let save_pref () = add "project_options" [string_of_project_behavior p.read_project] ++ add "project_file_name" [p.project_file_name] ++ + add "project_path" (match p.project_path with None -> [] | Some s -> [s]) ++ add "encoding" [string_of_inputenc p.encoding] ++ @@ -296,6 +301,7 @@ let save_pref () = add "processing_color" [p.processing_color] ++ add "processed_color" [p.processed_color] ++ add "error_color" [p.error_color] ++ + add "error_fg_color" [p.error_fg_color] ++ add "dynamic_word_wrap" [string_of_bool p.dynamic_word_wrap] ++ add "show_line_number" [string_of_bool p.show_line_number] ++ add "auto_indent" [string_of_bool p.auto_indent] ++ @@ -339,6 +345,7 @@ let load_pref () = set_hd "project_options" (fun v -> np.read_project <- (project_behavior_of_string v)); set_hd "project_file_name" (fun v -> np.project_file_name <- v); + set_option "project_path" (fun v -> np.project_path <- v); set "automatic_tactics" (fun v -> np.automatic_tactics <- v); set_hd "cmd_print" (fun v -> np.cmd_print <- v); @@ -382,6 +389,7 @@ let load_pref () = set_hd "processing_color" (fun v -> np.processing_color <- v); set_hd "processed_color" (fun v -> np.processed_color <- v); set_hd "error_color" (fun v -> np.error_color <- v); + set_hd "error_fg_color" (fun v -> np.error_fg_color <- v); set_bool "dynamic_word_wrap" (fun v -> np.dynamic_word_wrap <- v); set_bool "show_line_number" (fun v -> np.show_line_number <- v); set_bool "auto_indent" (fun v -> np.auto_indent <- v); @@ -466,10 +474,15 @@ let configure ?(apply=(fun () -> ())) () = ~text:"Background color of errors" ~packing:(table#attach ~expand:`X ~left:0 ~top:3) () in + let error_fg_label = GMisc.label + ~text:"Foreground color of errors" + ~packing:(table#attach ~expand:`X ~left:0 ~top:4) () + in let () = background_label#set_xalign 0. in let () = processed_label#set_xalign 0. in let () = processing_label#set_xalign 0. in let () = error_label#set_xalign 0. in + let () = error_fg_label#set_xalign 0. in let background_button = GButton.color_button ~color:(Tags.color_of_string (current.background_color)) ~packing:(table#attach ~left:1 ~top:0) () @@ -486,15 +499,19 @@ let configure ?(apply=(fun () -> ())) () = ~color:(Tags.get_error_color ()) ~packing:(table#attach ~left:1 ~top:3) () in + let error_fg_button = GButton.color_button + ~color:(Tags.get_error_fg_color ()) + ~packing:(table#attach ~left:1 ~top:4) () + in let reset_button = GButton.button ~label:"Reset" ~packing:box#pack () in let reset_cb () = - background_button#set_color (Tags.color_of_string "cornsilk"); - processing_button#set_color (Tags.color_of_string "light blue"); - processed_button#set_color (Tags.color_of_string "light green"); - error_button#set_color (Tags.color_of_string "#FFCCCC"); + background_button#set_color Tags.(color_of_string default_color); + processing_button#set_color Tags.(color_of_string default_processing_color); + processed_button#set_color Tags.(color_of_string default_processed_color); + error_button#set_color Tags.(color_of_string default_error_color); in let _ = reset_button#connect#clicked ~callback:reset_cb in let label = "Color configuration" in @@ -503,10 +520,12 @@ let configure ?(apply=(fun () -> ())) () = current.processing_color <- Tags.string_of_color processing_button#color; current.processed_color <- Tags.string_of_color processed_button#color; current.error_color <- Tags.string_of_color error_button#color; + current.error_fg_color <- Tags.string_of_color error_fg_button#color; !refresh_editor_hook (); Tags.set_processing_color processing_button#color; Tags.set_processed_color processed_button#color; - Tags.set_error_color error_button#color + Tags.set_error_color error_button#color; + Tags.set_error_fg_color error_fg_button#color in custom ~label box callback true in diff --git a/ide/preferences.mli b/ide/preferences.mli index 1b52d20a..1e4f152c 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -32,6 +32,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; + mutable project_path : string option; mutable encoding : inputenc; @@ -71,6 +72,7 @@ type pref = mutable processing_color : string; mutable processed_color : string; mutable error_color : string; + mutable error_fg_color : string; mutable dynamic_word_wrap : bool; mutable show_line_number : bool; diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 41dc1bef..f7279f9c 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -182,29 +182,21 @@ let read_project_file f = (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) let args_from_project file project_files default_name = - let is_f = CUnix.same_file file in - let contains_file dir = - List.exists (fun x -> is_f (CUnix.correct_path x dir)) - in let build_cmd_line ml_inc i_inc r_inc args = List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args []))) in try - let (_,(_,(ml_inc,i_inc,r_inc),(args,_))) = - List.find (fun (dir,((v_files,_,_,_),_,_)) -> - contains_file dir v_files) project_files in - build_cmd_line ml_inc i_inc r_inc args - with Not_found -> + let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in + fname, build_cmd_line ml_inc i_inc r_inc args + with Failure _ -> let rec find_project_file dir = try + let fname = Filename.concat dir default_name in let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) = - read_project_file (Filename.concat dir default_name) in - if contains_file dir v_files - then build_cmd_line ml_inc i_inc r_inc args - else let newdir = Filename.dirname dir in - if dir = newdir then [] else find_project_file newdir + read_project_file fname in + fname, build_cmd_line ml_inc i_inc r_inc args with Sys_error s -> let newdir = Filename.dirname dir in - if dir = newdir then [] else find_project_file newdir + if dir = newdir then "",[] else find_project_file newdir in find_project_file (Filename.dirname file) diff --git a/ide/session.ml b/ide/session.ml index 29363211..12b77966 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -18,6 +18,7 @@ class type ['a] page = inherit GObj.widget method update : 'a -> unit method on_update : callback:('a -> unit) -> unit + method refresh_color : unit -> unit end class type control = @@ -133,6 +134,11 @@ let set_buffer_handlers try ignore(buffer#get_mark (`NAME "stop_of_input")) with GText.No_such_mark _ -> assert false in let get_insert () = buffer#get_iter_at_mark `INSERT in + let update_prev it = + let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in + if it#offset < prev#offset then + buffer#move_mark (`NAME "prev_insert") ~where:it + in let debug_edit_zone () = if false (*!Minilib.debug*) then begin buffer#remove_tag Tags.Script.edit_zone ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -147,10 +153,9 @@ let set_buffer_handlers let insert_cb it s = if String.length s = 0 then () else begin Minilib.log ("insert_cb " ^ string_of_int it#offset); let text_mark = add_mark it in + let () = update_prev it in if it#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" - else if it#has_tag Tags.Script.read_only then - cancel_signal "Altering read_only text not allowed" else if it#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else if it#has_tag Tags.Script.error_bg then begin @@ -160,16 +165,14 @@ let set_buffer_handlers end end in let delete_cb ~start ~stop = Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset); - cur_action := new_action_id (); let min_iter, max_iter = if start#compare stop < 0 then start, stop else stop, start in + let () = update_prev min_iter in let text_mark = add_mark min_iter in let rec aux min_iter = if min_iter#equal max_iter then () else if min_iter#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" - else if min_iter#has_tag Tags.Script.read_only then - cancel_signal "Altering read_only text not allowed" else if min_iter#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) else if min_iter#has_tag Tags.Script.error_bg then @@ -250,6 +253,10 @@ let make_table_widget cd cb = ~rules_hint:true ~headers_visible:false ~model:store ~packing:frame#add () in let () = data#set_headers_visible true in + let refresh () = + let clr = Tags.color_of_string current.background_color in + data#misc#modify_base [`NORMAL, `COLOR clr] + in let mk_rend c = GTree.cell_renderer_text [], ["text",c] in let cols = List.map2 (fun (_,c) (_,n,v) -> @@ -265,10 +272,10 @@ let make_table_widget cd cb = ignore( data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc) ); - frame, (fun f -> f columns store) + frame, (fun f -> f columns store), refresh let create_errpage (script : Wg_ScriptView.script_view) : errpage = - let table, access = + let table, access, refresh = make_table_widget [`Int,"Line",true; `String,"Error message",true] (fun columns store tp vc -> @@ -299,10 +306,11 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = errs end method on_update ~callback:cb = callback := cb + method refresh_color () = refresh () end let create_jobpage coqtop coqops : jobpage = - let table, access = + let table, access, refresh = make_table_widget [`String,"Worker",true; `String,"Job name",true] (fun columns store tp vc -> @@ -338,6 +346,7 @@ let create_jobpage coqtop coqops : jobpage = jobs end method on_update ~callback:cb = callback := cb + method refresh_color () = refresh () end let create_proof () = @@ -465,7 +474,7 @@ let build_layout (sn:session) = message_frame#misc#show (); detachable#show); detachable#button#misc#hide (); - lbl in + detachable, lbl in let session_tab = GPack.hbox ~homogeneous:false () in let img = GMisc.image ~icon_size:`SMALL_TOOLBAR ~packing:session_tab#pack () in @@ -496,9 +505,17 @@ let build_layout (sn:session) = sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false); script_scroll#add sn.script#coerce; proof_scroll#add sn.proof#coerce; - ignore(add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce); - let label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in - ignore(add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce); + let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce in + let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in + let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in + (** When a message is received, focus on the message pane *) + let _ = + sn.messages#connect#pushed ~callback:(fun _ _ -> + let num = message_frame#page_num detach#coerce in + if 0 <= num then message_frame#goto_page num + ) + in + (** When an error occurs, paint the error label in red *) let txt = label#text in let red s = "" ^ s ^ "" in sn.errpage#on_update ~callback:(fun l -> diff --git a/ide/session.mli b/ide/session.mli index 3a6b4585..52e55721 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -14,6 +14,7 @@ class type ['a] page = inherit GObj.widget method update : 'a -> unit method on_update : callback:('a -> unit) -> unit + method refresh_color : unit -> unit end class type control = diff --git a/ide/tags.ml b/ide/tags.ml index 04ad9a51..c9b57af4 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -13,15 +13,23 @@ let make_tag (tt:GText.tag_table) ~name prop = tt#add new_tag#as_tag; new_tag -let processed_color = ref "light green" -let processing_color = ref "light blue" -let error_color = ref "#FFCCCC" +(* These work fine for colorblind people too *) +let default_processed_color = "light green" +let default_processing_color = "light blue" +let default_error_color = "#FFCCCC" +let default_error_fg_color = "red" +let default_color = "cornsilk" + +let processed_color = ref default_processed_color +let processing_color = ref default_processing_color +let error_color = ref default_error_color +let error_fg_color = ref default_error_fg_color module Script = struct let table = GText.tag_table () let comment = make_tag table ~name:"comment" [] - let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND "red"] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color] let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color] let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color] let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color] @@ -44,8 +52,6 @@ struct t let all = edit_zone :: all - let read_only = make_tag table ~name:"read_only" [`EDITABLE false ] - end module Proof = struct @@ -94,3 +100,11 @@ let set_error_color clr = let s = string_of_color clr in error_color := s; Script.error_bg#set_property (`BACKGROUND s) + +let get_error_fg_color () = color_of_string !error_fg_color + +let set_error_fg_color clr = + let s = string_of_color clr in + error_fg_color := s; + Script.error#set_property (`FOREGROUND s) + diff --git a/ide/tags.mli b/ide/tags.mli index 9c3261d6..14cfd0db 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -21,9 +21,6 @@ sig val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) val all : GText.tag list - - (* Not part of the all list. Special tags! *) - val read_only : GText.tag end module Proof : @@ -53,3 +50,13 @@ val set_processing_color : Gdk.color -> unit val get_error_color : unit -> Gdk.color val set_error_color : Gdk.color -> unit + +val get_error_fg_color : unit -> Gdk.color +val set_error_fg_color : Gdk.color -> unit + +val default_processed_color : string +val default_processing_color : string +val default_error_color : string +val default_error_fg_color : string +val default_color : string + diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index b6f63a3b..a0949ca0 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -8,6 +8,8 @@ type mode = [ `FIND | `REPLACE ] +let b2c = Ideutils.byte_offset_to_char_offset + class finder name (view : GText.view) = let widget = Wg_Detachable.detachable @@ -61,8 +63,10 @@ class finder name (view : GText.view) = method replace () = if self#may_replace () then let txt = self#get_selected_word () in + let () = view#buffer#begin_user_action () in let _ = view#buffer#delete_selection () in let _ = view#buffer#insert_interactive (self#replacement txt) in + let () = view#buffer#end_user_action () in self#find_forward () else self#find_forward () @@ -85,8 +89,8 @@ class finder name (view : GText.view) = try let i = Str.search_backward regexp text (String.length text - 1) in let j = Str.match_end () in - Some(view#buffer#start_iter#forward_chars i, - view#buffer#start_iter#forward_chars j) + Some(view#buffer#start_iter#forward_chars (b2c text i), + view#buffer#start_iter#forward_chars (b2c text j)) with Not_found -> None method private forward_search starti = @@ -95,7 +99,7 @@ class finder name (view : GText.view) = try let i = Str.search_forward regexp text 0 in let j = Str.match_end () in - Some(starti#forward_chars i, starti#forward_chars j) + Some(starti#forward_chars (b2c text i), starti#forward_chars (b2c text j)) with Not_found -> None method replace_all () = @@ -115,7 +119,9 @@ class finder name (view : GText.view) = let () = view#buffer#delete_mark (`MARK stop_mark) in replace_at next in - replace_at view#buffer#start_iter + let () = view#buffer#begin_user_action () in + let () = replace_at view#buffer#start_iter in + view#buffer#end_user_action () method private set_not_found () = find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"]; diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 9acda53f..211db537 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -6,9 +6,25 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +class type message_view_signals = +object + inherit GObj.misc_signals + inherit GUtil.add_ml_signals + method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id +end + +class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals = +object + val after = false + inherit GObj.misc_signals obj + inherit GUtil.add_ml_signals obj [pushed#disconnect] + method pushed ~callback = pushed#connect ~after ~callback:(fun (lvl, s) -> callback lvl s) +end + class type message_view = object inherit GObj.widget + method connect : message_view_signals method clear : unit method add : string -> unit method set : string -> unit @@ -17,6 +33,7 @@ class type message_view = method buffer : GText.buffer (** for more advanced text edition *) method modify_font : Pango.font_description -> unit + method refresh_color : unit -> unit end let message_view () : message_view = @@ -32,12 +49,18 @@ let message_view () : message_view = ~source_buffer:buffer ~packing:scroll#add ~editable:false ~cursor_visible: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 () = view#set_left_margin 2 in object (self) inherit GObj.widget box#as_widget + val push = new GUtil.signal () + + method connect = + new message_view_signals_impl box#as_widget push + method clear = buffer#set_text "" @@ -49,7 +72,8 @@ let message_view () : message_view = in if msg <> "" then begin buffer#insert ~tags msg; - buffer#insert ~tags "\n" + buffer#insert ~tags "\n"; + push#call (level, msg) end method add msg = self#push Pp.Notice msg @@ -60,4 +84,9 @@ let message_view () : message_view = method modify_font fd = view#misc#modify_font fd + method refresh_color () = + let open Preferences in + let clr = Tags.color_of_string current.background_color in + view#misc#modify_base [`NORMAL, `COLOR clr] + end diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index cd3f00c9..23c94f40 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -6,9 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +class type message_view_signals = +object + inherit GObj.misc_signals + inherit GUtil.add_ml_signals + method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id +end + class type message_view = object inherit GObj.widget + method connect : message_view_signals method clear : unit method add : string -> unit method set : string -> unit @@ -17,6 +25,7 @@ class type message_view = method buffer : GText.buffer (** for more advanced text edition *) method modify_font : Pango.font_description -> unit + method refresh_color : unit -> unit end val message_view : unit -> message_view diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 7e7a311e..b12d29d6 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -9,6 +9,7 @@ class type proof_view = object inherit GObj.widget + method buffer : GText.buffer method refresh : unit -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit @@ -176,9 +177,11 @@ let proof_view () = ~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 ~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 object @@ -186,6 +189,8 @@ let proof_view () = val mutable goals = None val mutable evars = None + method buffer = text_buffer + method clear () = buffer#set_text "" method set_goals gls = goals <- gls diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index 1fbf9900..c5e042ea 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -9,6 +9,7 @@ class type proof_view = object inherit GObj.widget + method buffer : GText.buffer method refresh : unit -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 1f399070..8298d995 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -186,11 +186,19 @@ object(self) method undo () = Minilib.log "UNDO"; - self#with_lock_undo self#perform_undo (); + self#with_lock_undo begin fun () -> + buffer#begin_user_action (); + self#perform_undo (); + buffer#end_user_action () + end () method redo () = Minilib.log "REDO"; - self#with_lock_undo self#perform_redo (); + self#with_lock_undo begin fun () -> + buffer#begin_user_action (); + self#perform_redo (); + buffer#end_user_action () + end () method process_begin_user_action () = (* Push a new level of event on history stack *) @@ -410,6 +418,7 @@ object (self) self#buffer#end_user_action () initializer + let () = Gtk_parsing.fix_double_click self in let supersed cb _ = let _ = cb () in GtkSignal.stop_emit() diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index 8520727a..25a031d6 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -70,9 +70,25 @@ let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with | `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 + inherit GObj.misc_signals obj + inherit GUtil.add_ml_signals obj [clicked#disconnect] + method clicked = clicked#connect ~after +end + class segment () = let box = GBin.frame () in -let draw = GMisc.image ~packing:box#add () 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 @@ -82,6 +98,7 @@ object (self) val mutable data = Segment.empty val mutable default : color = `WHITE val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 () + val clicked = new GUtil.signal () initializer box#misc#set_size_request ~height (); @@ -96,6 +113,15 @@ object (self) end in let _ = box#misc#connect#size_allocate cb in + let clicked_cb ev = + let x = GdkEvent.Button.x ev in + let (width, _) = pixmap#size in + let len = Segment.length data in + let idx = f2i ((x *. i2f len) /. i2f width) in + let () = clicked#call idx in + true + in + let _ = eventbox#event#connect#button_press clicked_cb in (** Initial pixmap *) draw#set_pixmap pixmap @@ -140,4 +166,7 @@ object (self) Segment.fold color_eq fold data (); draw#set_mask None; + method connect = + new segment_signals_impl box#as_widget clicked + end diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli index ecb45147..0263856a 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.mli @@ -8,10 +8,18 @@ type color = GDraw.color +class type segment_signals = +object + inherit GObj.misc_signals + inherit GUtil.add_ml_signals + method clicked : callback:(int -> unit) -> GtkSignal.id +end + class segment : unit -> object inherit GObj.widget val obj : Gtk.widget Gtk.obj + method connect : segment_signals method length : int method set_length : int -> unit method default_color : color -- cgit v1.2.3