diff options
| -rw-r--r-- | ide/coqide.ml | 2279 | ||||
| -rw-r--r-- | ide/ideutils.ml | 193 | ||||
| -rw-r--r-- | ide/ideutils.mli | 10 |
3 files changed, 1209 insertions, 1273 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 4f830a421..3c2b2553e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -10,6 +10,8 @@ open Preferences open Gtk_parsing open Ideutils +type direction = Up | Down + type flag = [ `COMMENT | `UNSAFE ] type ide_info = { @@ -31,8 +33,7 @@ object method get_insert : GText.iter method get_start_of_input : GText.iter method go_to_insert : Coq.handle -> unit - method go_to_next_occ_of_cur_word : unit - method go_to_prev_occ_of_cur_word : unit + method find_next_occurrence : direction -> unit method tactic_wizard : Coq.handle -> string list -> unit method insert_message : string -> unit method process_next_phrase : Coq.handle -> bool -> unit @@ -75,18 +76,18 @@ let build_session s = ~packing:(session_box#pack ~expand:true) () in let script_frame = GBin.frame ~shadow_type:`IN ~packing:eval_paned#add1 () in - let script_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC - ~packing:script_frame#add () 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 let proof_frame = GBin.frame ~shadow_type:`IN ~packing:state_paned#add1 () in - let proof_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC - ~packing:proof_frame#add () in + let proof_scroll = GBin.scrolled_window + ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in let message_frame = GBin.frame ~shadow_type:`IN ~packing:state_paned#add2 () in - let message_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC - ~packing:message_frame#add () in + let message_scroll = GBin.scrolled_window + ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:message_frame#add () in let session_tab = GPack.hbox ~homogeneous:false () in let img = GMisc.image ~icon_size:`SMALL_TOOLBAR ~packing:session_tab#pack () in @@ -100,13 +101,17 @@ let build_session s = ~callback: (let old_paned_width = ref 2 in let old_paned_height = ref 2 in - (fun {Gtk.width=paned_width;Gtk.height=paned_height} -> - if !old_paned_width <> paned_width || !old_paned_height <> paned_height then ( - eval_paned#set_position (eval_paned#position * paned_width / !old_paned_width); - state_paned#set_position (state_paned#position * paned_height / !old_paned_height); - old_paned_width := paned_width; - old_paned_height := paned_height; - ))) + fun {Gtk.width=paned_width;Gtk.height=paned_height} -> + if !old_paned_width <> paned_width || + !old_paned_height <> paned_height + then begin + eval_paned#set_position + (eval_paned#position * paned_width / !old_paned_width); + state_paned#set_position + (state_paned#position * paned_height / !old_paned_height); + old_paned_width := paned_width; + old_paned_height := paned_height; + end) in session_box#pack s.finder#coerce; session_paned#pack2 ~shrink:false ~resize:false (s.command#frame#coerce); @@ -126,12 +131,11 @@ let session_notebook = let cb = GData.clipboard Gdk.Atom.primary let update_notebook_pos () = - let pos = - match current.vertical_tabs, current.opposite_tabs with - | false, false -> `TOP - | false, true -> `BOTTOM - | true , false -> `LEFT - | true , true -> `RIGHT + let pos = match current.vertical_tabs, current.opposite_tabs with + | false, false -> `TOP + | false, true -> `BOTTOM + | true , false -> `LEFT + | true , true -> `RIGHT in session_notebook#set_tab_pos pos @@ -198,54 +202,14 @@ let do_if_not_computing term text f = Minilib.log ("Launching thread " ^ text); ignore (Thread.create threaded_task ()) +let warn_image = + let img = GMisc.image () in + img#set_stock `DIALOG_WARNING; + img#set_icon_size `DIALOG; + img#coerce + let warning msg = - GToolbox.message_box ~title:"Warning" - ~icon:(let img = GMisc.image () in - img#set_stock `DIALOG_WARNING; - img#set_icon_size `DIALOG; - img#coerce) - msg - -let remove_current_view_page () = - let do_remove () = - let c = session_notebook#current_page in - session_notebook#remove_page c - in - let current = session_notebook#current_term in - if not current.script#buffer#modified then do_remove () - else - match GToolbox.question_box ~title:"Close" - ~buttons:["Save Buffer and Close"; - "Close without Saving"; - "Don't Close"] - ~default:0 - ~icon:(let img = GMisc.image () in - img#set_stock `DIALOG_WARNING; - img#set_icon_size `DIALOG; - img#coerce) - "This buffer has unsaved modifications" - with - | 1 -> - begin match current.analyzed_view#filename with - | None -> - begin match select_file_for_save ~title:"Save file" () with - | None -> () - | Some f -> - if current.analyzed_view#save_as f then begin - flash_info ("File " ^ f ^ " saved") ; - do_remove () - end else - warning ("Save Failed (check if " ^ f ^ " is writable)") - end - | Some f -> - if current.analyzed_view#save f then begin - flash_info ("File " ^ f ^ " saved") ; - do_remove () - end else - warning ("Save Failed (check if " ^ f ^ " is writable)") - end - | 2 -> do_remove () - | _ -> () + GToolbox.message_box ~title:"Warning" ~icon:warn_image msg module Opt = Coq.PrintOpt @@ -262,14 +226,11 @@ let print_items = [ "Display _existential variable instances","e",false); ([Opt.universes],"Display universe levels","Display _universe levels", "u",false); - ([Opt.all_basic;Opt.existential;Opt.universes], "Display all low-level contents", - "Display all _low-level contents","l",false) + ([Opt.all_basic;Opt.existential;Opt.universes], + "Display all low-level contents", "Display all _low-level contents", + "l",false) ] -let setopts ct opts v = - let opts = List.map (fun o -> (o, v)) opts in - Coq.PrintOpt.set ct opts - let get_current_word () = match session_notebook#current_term,cb#text with | {script=script; analyzed_view=av;},None -> @@ -308,12 +269,13 @@ let split_slice_lax (buffer: GText.buffer) from upto = let rec split_substring str = let off_conv = byte_offset_to_char_offset str in let slice_len = String.length str in - let is_comment,end_off = Coq_lex.delimit_sentence str - in + let is_comment,end_off = Coq_lex.delimit_sentence str in let start = from#forward_chars (off_conv end_off) in let stop = start#forward_char in - buffer#apply_tag ~start ~stop - (if is_comment then Tags.Script.comment_sentence else Tags.Script.sentence); + let tag = + if is_comment then Tags.Script.comment_sentence else Tags.Script.sentence + in + buffer#apply_tag ~start ~stop tag; let next = end_off + 1 in if next < slice_len then begin ignore (from#nocopy#forward_chars (off_conv next)); @@ -332,7 +294,8 @@ let rec backward_search cond (iter:GText.iter) = if iter#is_start || cond iter then iter else backward_search cond iter#backward_char -let is_sentence_end s = s#has_tag Tags.Script.sentence || s#has_tag Tags.Script.comment_sentence +let is_sentence_end s = + s#has_tag Tags.Script.sentence || s#has_tag Tags.Script.comment_sentence let is_char s c = s#char = Char.code c (** Search backward the first character of a sentence, starting at [iter] @@ -389,7 +352,8 @@ let tag_on_insert buffer = with Not_found -> (* This is raised by [grab_sentence_start] *) let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in - buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char + buffer#apply_tag Tags.Script.error + ~start:err_pos ~stop:err_pos#forward_char let force_retag buffer = try split_slice_lax buffer buffer#start_iter buffer#end_iter @@ -447,47 +411,46 @@ object(self) | _ -> () method revert = + let do_revert f = + push_info "Reverting buffer"; + try + Coq.reset_coqtop mycoqtop self#requested_reset_initial; + let b = Buffer.create 1024 in + with_file flash_info f ~f:(input_channel b); + let s = try_convert (Buffer.contents b) in + input_buffer#set_text s; + self#update_stats; + input_buffer#place_cursor ~where:input_buffer#start_iter; + input_buffer#set_modified false; + pop_info (); + flash_info "Buffer reverted"; + force_retag (input_buffer :> GText.buffer); + with _ -> + pop_info (); + flash_info "Warning: could not revert buffer"; + in match filename with - | Some f -> begin - let do_revert () = begin - push_info "Reverting buffer"; - try - Coq.reset_coqtop mycoqtop self#requested_reset_initial; - let b = Buffer.create 1024 in - with_file flash_info f ~f:(input_channel b); - let s = try_convert (Buffer.contents b) in - input_buffer#set_text s; - self#update_stats; - input_buffer#place_cursor ~where:input_buffer#start_iter; - input_buffer#set_modified false; - pop_info (); - flash_info "Buffer reverted"; - force_retag (input_buffer :> GText.buffer); - with _ -> - pop_info (); - flash_info "Warning: could not revert buffer"; - end - in - if input_buffer#modified then - match (GToolbox.question_box - ~title:"Modified buffer changed on disk" - ~buttons:["Revert from File"; - "Overwrite File"; - "Disable Auto Revert"] - ~default:0 - ~icon:(stock_to_widget `DIALOG_WARNING) - "Some unsaved buffers changed on disk" - ) - with 1 -> do_revert () + | None -> () + | Some f -> + if not input_buffer#modified then do_revert f + else + let answ = GToolbox.question_box + ~title:"Modified buffer changed on disk" + ~buttons:["Revert from File"; + "Overwrite File"; + "Disable Auto Revert"] + ~default:0 + ~icon:(stock_to_widget `DIALOG_WARNING) + "Some unsaved buffers changed on disk" + in + match answ with + | 1 -> do_revert f | 2 -> if self#save f then flash_info "Overwritten" else flash_info "Could not overwrite file" | _ -> Minilib.log "Auto revert set to false"; current.global_auto_revert <- false; disconnect_revert_timer () - else do_revert () - end - | None -> () method save f = if try_export f (input_buffer#get_text ()) then begin @@ -533,21 +496,17 @@ object(self) end method save_as f = - if Sys.file_exists f then - match (GToolbox.question_box ~title:"File exists on disk" - ~buttons:["Overwrite"; - "Cancel";] - ~default:1 - ~icon: - (let img = GMisc.image () in - img#set_stock `DIALOG_WARNING; - img#set_icon_size `DIALOG; - img#coerce) - ("File "^f^" already exists") - ) - with 1 -> self#save f + if not (Sys.file_exists f) then self#save f + else + let answ = GToolbox.question_box ~title:"File exists on disk" + ~buttons:["Overwrite"; "Cancel";] + ~default:1 + ~icon:warn_image + ("File "^f^" already exists") + in + match answ with + | 1 -> self#save f | _ -> false - else self#save f method insert_message s = message_view#push Interface.Notice s @@ -559,7 +518,8 @@ object(self) method private push_message level content = message_view#push level content - method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input") + method get_start_of_input = + input_buffer#get_iter_at_mark (`NAME "start_of_input") method get_insert = get_insert input_buffer @@ -575,27 +535,16 @@ object(self) ~within_margin:0.25) `INSERT) - method go_to_next_occ_of_cur_word = - let cv = session_notebook#current_term in - let av = cv.analyzed_view in - let b = (cv.script)#buffer in - let start = find_word_start (av#get_insert) in + (* go to the next occurrence of the current word, forward or backward *) + method find_next_occurrence dir = + let b = input_buffer in + let start = find_word_start self#get_insert in let stop = find_word_end start in let text = b#get_text ~start ~stop () in - match stop#forward_search text with - | None -> () - | Some(start, _) -> - (b#place_cursor start; - self#recenter_insert) - - method go_to_prev_occ_of_cur_word = - let cv = session_notebook#current_term in - let av = cv.analyzed_view in - let b = (cv.script)#buffer in - let start = find_word_start (av#get_insert) in - let stop = find_word_end start in - let text = b#get_text ~start ~stop () in - match start#backward_search text with + let search = + if dir=Down then stop#forward_search else start#backward_search + in + match search text with | None -> () | Some(start, _) -> (b#place_cursor start; @@ -650,12 +599,13 @@ object(self) if until len start stop then raise Exit; input_buffer#apply_tag Tags.Script.to_process ~start ~stop; (* Check if this is a comment *) - let is_comment = stop#backward_char#has_tag Tags.Script.comment_sentence in - let flags = if is_comment then [`COMMENT] else [] in + let is_comment = + stop#backward_char#has_tag Tags.Script.comment_sentence + in let payload = { start = `MARK (input_buffer#create_mark start); stop = `MARK (input_buffer#create_mark stop); - flags = flags; + flags = if is_comment then [`COMMENT] else []; } in Queue.push payload queue; if not stop#is_end then loop (succ len) stop @@ -921,9 +871,9 @@ object(self) | Some f -> let dir = Filename.dirname f in match Coq.inloadpath handle dir with - | Interface.Fail (_,str) -> + | Interface.Fail (_,s) -> self#set_message - ("Could not determine lodpath, this might lead to problems:\n"^str) + ("Could not determine lodpath, this might lead to problems:\n"^s) | Interface.Good true | Interface.Unsafe true -> () | Interface.Good false | Interface.Unsafe false -> let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in @@ -1030,11 +980,6 @@ object(self) Minilib.log "Should recenter: yes"; self#recenter_insert end)); - let callback () = - if Coq.is_computing mycoqtop then pbar#pulse (); - not (Coq.is_closed mycoqtop); - in - ignore (Glib.Timeout.add ~ms:300 ~callback); Coq.grab mycoqtop self#include_file_dir_in_path; end @@ -1045,7 +990,9 @@ let search_compile_error_regexp = "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)";; let search_next_error () = - let _ = Str.search_forward search_compile_error_regexp !last_make !last_make_index in + let _ = + Str.search_forward search_compile_error_regexp !last_make !last_make_index + in let f = Str.matched_group 1 !last_make and l = int_of_string (Str.matched_group 2 !last_make) and b = int_of_string (Str.matched_group 3 !last_make) @@ -1073,17 +1020,20 @@ let create_session file = in let proof = Wg_ProofView.proof_view () in let message = Wg_MessageView.message_view () in - let basename = GMisc.label ~text:(match file with - |None -> "*scratch*" - |Some f -> (Glib.Convert.filename_to_utf8 (Filename.basename f)) - ) () in + let basename = match file with + |None -> "*scratch*" + |Some f -> Glib.Convert.filename_to_utf8 (Filename.basename f) + in + let get_args f = + Project_file.args_from_project f + !custom_project_files current.project_file_name + in let coqtop_args = match file with |None -> !sup_args |Some the_file -> match current.read_project with |Ignore_args -> !sup_args - |Append_args -> (Project_file.args_from_project the_file !custom_project_files current.project_file_name) - @(!sup_args) - |Subst_args -> Project_file.args_from_project the_file !custom_project_files current.project_file_name + |Append_args -> get_args the_file @ !sup_args + |Subst_args -> get_args the_file in let reset = ref (fun _ -> ()) in let trigger handle = !reset handle in @@ -1099,23 +1049,26 @@ let create_session file = let () = reset := legacy_av#erroneous_reset_initial in let () = legacy_av#update_stats in let _ = - script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in + script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter + in let _ = script#buffer#create_mark ~name:"prev_insert" script#buffer#start_iter in let _ = - GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in + GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] + in let () = let fold accu (opts, _, _, _, dflt) = List.fold_left (fun accu opt -> (opt, dflt) :: accu) accu opts in let options = List.fold_left fold [] print_items in - Coq.grab ct (fun handle -> Coq.PrintOpt.set handle options) in + Coq.grab ct (fun handle -> Coq.PrintOpt.set handle options) + in script#misc#set_name "ScriptWindow"; script#buffer#place_cursor ~where:script#buffer#start_iter; proof#misc#set_can_focus true; message#misc#set_can_focus true; - { tab_label=basename; + { tab_label= GMisc.label ~text:basename (); script=script; proof_view=proof; message_view=message; @@ -1125,121 +1078,9 @@ let create_session file = finder=finder; } -(* XXX - to be used later - let load_session session filename encs = - session.encoding <- List.find (IdeIO.load filename session.script#buffer) encs; - session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename)); - session.filename <- filename; - session.script#buffer#set_modified false - - - let save_session session filename encs = - session.encoding <- List.find (IdeIO.save session.script#buffer filename) encs; - session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename)); - session.filename <- filename; - session.script#buffer#set_modified false - - - let init_session session = - session.script#buffer#set_modified false; - session.script#clear_undo; - session.script#buffer#place_cursor session.script#buffer#start_iter -*) - - - - (*********************************************************************) (* functions called by the user interface *) (*********************************************************************) -(* XXX - to be used later - let do_open session filename = - try - load_session session filename ["UTF-8";"ISO-8859-1";"ISO-8859-15"]; - init_session session; - ignore (session_notebook#append_term session) - with _ -> () - - - let do_save session = - try - if session.script#buffer#modified then - save_session session session.filename [session.encoding] - with _ -> () - - - let choose_open = - let last_filename = ref "" in fun session -> - let open_dialog = GWindow.file_chooser_dialog ~action:`OPEN ~title:"Open file" ~modal:true () in - let enc_frame = GBin.frame ~label:"File encoding" ~packing:(open_dialog#vbox#pack ~fill:false) () in - let enc_entry = GEdit.entry ~text:(String.concat " " ["UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in - let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok - ~message:"Invalid encoding, please indicate the encoding to use." () in - let open_response = function - | `OPEN -> begin - match open_dialog#filename with - | Some fn -> begin - try - load_session session fn (Util.split_string_at ' ' enc_entry#text); - session.analyzed_view <- Some (new analyzed_view session); - init_session session; - session_notebook#goto_page (session_notebook#append_term session); - last_filename := fn - with - | Not_found -> open_dialog#misc#hide (); error_dialog#show () - | _ -> - error_dialog#set_markup "Unknown error while loading file, aborting."; - open_dialog#destroy (); error_dialog#destroy () - end - | None -> () - end - | `DELETE_EVENT -> open_dialog#destroy (); error_dialog#destroy () - in - let _ = open_dialog#connect#response open_response in - let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); open_dialog#show ()) in - let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in - let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in - open_dialog#add_select_button_stock `OPEN `OPEN; - open_dialog#add_button_stock `CANCEL `DELETE_EVENT; - open_dialog#add_filter filter_any; - open_dialog#add_filter filter_coq; - ignore(open_dialog#set_filename !last_filename); - open_dialog#show () - - - let choose_save session = - let save_dialog = GWindow.file_chooser_dialog ~action:`SAVE ~title:"Save file" ~modal:true () in - let enc_frame = GBin.frame ~label:"File encoding" ~packing:(save_dialog#vbox#pack ~fill:false) () in - let enc_entry = GEdit.entry ~text:(String.concat " " [session.encoding;"UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in - let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok - ~message:"Invalid encoding, please indicate the encoding to use." () in - let save_response = function - | `SAVE -> begin - match save_dialog#filename with - | Some fn -> begin - try - save_session session fn (Util.split_string_at ' ' enc_entry#text) - with - | Not_found -> save_dialog#misc#hide (); error_dialog#show () - | _ -> - error_dialog#set_markup "Unknown error while saving file, aborting."; - save_dialog#destroy (); error_dialog#destroy () - end - | None -> () - end - | `DELETE_EVENT -> save_dialog#destroy (); error_dialog#destroy () - in - let _ = save_dialog#connect#response save_response in - let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); save_dialog#show ()) in - let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in - let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in - save_dialog#add_select_button_stock `SAVE `SAVE; - save_dialog#add_button_stock `CANCEL `DELETE_EVENT; - save_dialog#add_filter filter_any; - save_dialog#add_filter filter_coq; - ignore(save_dialog#set_filename session.filename); - save_dialog#show () -*) (* Nota: using && here has the advantage of working both under win32 and unix. If someday we want the main command to be tried even if the "cd" has failed, @@ -1249,952 +1090,1058 @@ let create_session file = let local_cd file = "cd " ^ Filename.quote (Filename.dirname file) ^ " && " -let do_print session = - let av = session.analyzed_view in - match av#filename with - |None -> flash_info "Cannot print: this buffer has no name" - |Some f_name -> begin - let cmd = - local_cd f_name ^ - current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f_name) ^ - " | " ^ current.cmd_print - in - let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () in - let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in - let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in - let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in - let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in - let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in - let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in - let callback_print () = - let cmd = print_entry#text in - let s,_ = CUnix.run_command Ideutils.try_convert av#insert_message cmd in - flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed"); - print_window#destroy () - in - ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ; - ignore (print_button#connect#clicked ~callback:callback_print); - print_window#misc#show () - end +let pr_exit_status = function + | Unix.WEXITED 0 -> " succeeded" + | _ -> " failed" + +let run_command av cmd = + CUnix.run_command Ideutils.try_convert av#insert_message cmd + +let current_view () = session_notebook#current_term.analyzed_view + +(** Auxiliary functions for the File operations *) + +module FileAux = struct let load_file handler f = let f = CUnix.correct_path f (Sys.getcwd ()) in try Minilib.log "Loading file starts"; let is_f = CUnix.same_file f in - if not (Util.List.fold_left_i - (fun i found x -> if found then found else - let {analyzed_view=av} = x in - (match av#filename with - | None -> false - | Some fn -> - if is_f fn - then (session_notebook#goto_page i; true) - else false)) - 0 false session_notebook#pages) - then begin - Minilib.log "Loading: must open"; - let b = Buffer.create 1024 in - Minilib.log "Loading: get raw content"; - with_file handler f ~f:(input_channel b); - Minilib.log "Loading: convert content"; - let s = do_convert (Buffer.contents b) in - Minilib.log "Loading: create view"; - let session = create_session (Some f) in - Minilib.log "Loading: adding view"; - let index = session_notebook#append_term session in - let av = session.analyzed_view in - Minilib.log "Loading: stats"; - av#update_stats; - let input_buffer = session.script#buffer in - Minilib.log "Loading: fill buffer"; - input_buffer#set_text s; - input_buffer#place_cursor ~where:input_buffer#start_iter; - force_retag input_buffer; - Minilib.log ("Loading: switch to view "^ string_of_int index); - session_notebook#goto_page index; - Minilib.log "Loading: highlight"; - input_buffer#set_modified false; - Minilib.log "Loading: clear undo"; - session.script#clear_undo (); - Minilib.log "Loading: success"; - !refresh_editor_hook (); - end - with - | e -> handler ("Load failed: "^(Printexc.to_string e)) + let rec search_f i = function + | [] -> false + | p :: pages -> + match p.analyzed_view#filename with + | Some fn when is_f fn -> session_notebook#goto_page i; true + | _ -> search_f (i+1) pages + in + if not (search_f 0 session_notebook#pages) then begin + Minilib.log "Loading: get raw content"; + let b = Buffer.create 1024 in + with_file handler f ~f:(input_channel b); + Minilib.log "Loading: convert content"; + let s = do_convert (Buffer.contents b) in + Minilib.log "Loading: create view"; + let session = create_session (Some f) in + Minilib.log "Loading: adding view"; + let index = session_notebook#append_term session in + let av = session.analyzed_view in + Minilib.log "Loading: stats"; + av#update_stats; + let input_buffer = session.script#buffer in + Minilib.log "Loading: fill buffer"; + input_buffer#set_text s; + input_buffer#place_cursor ~where:input_buffer#start_iter; + force_retag input_buffer; + Minilib.log ("Loading: switch to view "^ string_of_int index); + session_notebook#goto_page index; + Minilib.log "Loading: highlight"; + input_buffer#set_modified false; + Minilib.log "Loading: clear undo"; + session.script#clear_undo (); + Minilib.log "Loading: success"; + !refresh_editor_hook (); + end + with e -> handler ("Load failed: "^(Printexc.to_string e)) let do_load file = load_file flash_info file -let saveall_f () = - List.iter - (function - | {script = view ; analyzed_view = av} -> - begin match av#filename with - | None -> () - | Some f -> - ignore (av#save f) - end - ) session_notebook#pages +let confirm_save ok = + if ok then flash_info "Saved" else warning "Save Failed" + +let select_and_save ~saveas ?filename current = + let av = current.analyzed_view in + let do_save = if saveas then av#save_as else av#save in + let title = if saveas then "Save file as" else "Save file" in + match select_file_for_save ~title ?filename () with + |None -> false + |Some f -> + let ok = do_save f in + confirm_save ok; + if ok then current.tab_label#set_text (Filename.basename f); + ok + +let check_save ~saveas current = + try match current.analyzed_view#filename with + |None -> select_and_save ~saveas current + |Some f -> + let ok = current.analyzed_view#save f in + confirm_save ok; + ok + with _ -> warning "Save Failed"; false + +let revert {analyzed_view = av} = + try match av#filename,av#stats with + | Some f,Some stats -> + let new_stats = Unix.stat f in + if new_stats.Unix.st_mtime > stats.Unix.st_mtime + then av#revert + | Some _, None -> av#revert + | _ -> () + with _ -> av#revert + +exception DontQuit + +let check_quit saveall = + (try save_pref () with _ -> flash_info "Cannot save preferences"); + let is_modified p = p.script#buffer#modified in + if List.exists is_modified session_notebook#pages then begin + let answ = GToolbox.question_box ~title:"Quit" + ~buttons:["Save Named Buffers and Quit"; + "Quit without Saving"; + "Don't Quit"] + ~default:0 + ~icon:warn_image + "There are unsaved buffers" + in + match answ with + | 1 -> saveall () + | 2 -> () + | _ -> raise DontQuit + end; + let wait_w = GWindow.window ~modal:true ~wm_class:"CoqIde" ~wm_name:"CoqIde" + ~kind:`POPUP ~title:"Terminating coqtops" () in + let _ = + GMisc.label ~text:"Terminating coqtops processes, please wait ..." + ~packing:wait_w#add () + in + let warn_w = GWindow.message_dialog ~message_type:`WARNING + ~buttons:GWindow.Buttons.yes_no + ~message: + ("Some coqtops processes are still running.\n" ^ + "If you quit CoqIDE right now, you may have to kill them manually.\n" ^ + "Do you want to wait for those processes to terminate ?") + () + in + let () = + List.iter (fun _ -> session_notebook#remove_page 0) session_notebook#pages + in + let nb_try = ref 0 in + let () = wait_w#show () in + let () = + while (Coq.coqtop_zombies () <> 0) && (!nb_try <= 50) do + incr nb_try; + Thread.delay 0.1 ; + done + in + if !nb_try = 50 then begin + wait_w#misc#hide (); + match warn_w#run () with + | `YES -> warn_w#misc#hide (); raise DontQuit + | `NO | `DELETE_EVENT -> () + end -let forbid_quit_to_save () = - begin try save_pref() with e -> flash_info "Cannot save preferences" end; - (if List.exists - (function - | {script=view} -> view#buffer#modified - ) - session_notebook#pages then - match (GToolbox.question_box ~title:"Quit" - ~buttons:["Save Named Buffers and Quit"; - "Quit without Saving"; - "Don't Quit"] - ~default:0 - ~icon: - (let img = GMisc.image () in - img#set_stock `DIALOG_WARNING; - img#set_icon_size `DIALOG; - img#coerce) - "There are unsaved buffers" - ) - with 1 -> saveall_f () ; false - | 2 -> false - | _ -> true - else false)|| - (let wait_window = - GWindow.window ~modal:true ~wm_class:"CoqIde" ~wm_name:"CoqIde" ~kind:`POPUP - ~title:"Terminating coqtops" () in - let _ = - GMisc.label ~text:"Terminating coqtops processes, please wait ..." - ~packing:wait_window#add () in - let warning_window = - GWindow.message_dialog ~message_type:`WARNING ~buttons:GWindow.Buttons.yes_no - ~message: - ("Some coqtops processes are still running.\n" ^ - "If you quit CoqIDE right now, you may have to kill them manually.\n" ^ - "Do you want to wait for those processes to terminate ?") () in - let () = List.iter (fun _ -> session_notebook#remove_page 0) session_notebook#pages in - let nb_try=ref (0) in - let () = wait_window#show () in - let () = while (Coq.coqtop_zombies () <> 0)&&(!nb_try <= 50) do - incr nb_try; - Thread.delay 0.1 ; - done in - if (!nb_try = 50) then begin - wait_window#misc#hide (); - match warning_window#run () with - | `YES -> warning_window#misc#hide (); true - | `NO | `DELETE_EVENT -> false - end - else false) +end -let main files = +(** Callbacks for the File menu *) - (* Main window *) - let w = GWindow.window - ~wm_class:"CoqIde" ~wm_name:"CoqIde" - ~allow_grow:true ~allow_shrink:true - ~width:current.window_width ~height:current.window_height - ~title:"CoqIde" () - in - (try - let icon_image = Filename.concat (List.find - (fun x -> Sys.file_exists (Filename.concat x "coq.png")) - (Minilib.coqide_data_dirs ())) "coq.png" in - let icon = GdkPixbuf.from_file icon_image in - w#set_icon (Some icon) - with _ -> ()); +module File = struct - let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in +let newfile _ = + let session = create_session None in + let index = session_notebook#append_term session in + !refresh_editor_hook (); + session_notebook#goto_page index - let new_f _ = - let session = create_session None in - let index = session_notebook#append_term session in - !refresh_editor_hook (); - session_notebook#goto_page index - in - let load_f _ = - match select_file_for_open ~title:"Load file" () with +let load _ = + match select_file_for_open ~title:"Load file" () with + | None -> () + | Some f -> FileAux.do_load f + +let save _ = + ignore (FileAux.check_save ~saveas:false session_notebook#current_term) + +let saveas _ = + let current = session_notebook#current_term in + try + let filename = current.analyzed_view#filename in + ignore (FileAux.select_and_save ~saveas:true ?filename current) + with _ -> warning "Save Failed" + +let saveall _ = + List.iter + (function {analyzed_view = av} -> match av#filename with | None -> () - | Some f -> do_load f - in - let save_f _ = - let current = session_notebook#current_term in - try - (match current.analyzed_view#filename with - | None -> - begin match select_file_for_save ~title:"Save file" () - with - | None -> () - | Some f -> - if current.analyzed_view#save_as f then begin - current.tab_label#set_text (Filename.basename f); - flash_info ("File " ^ f ^ " saved") - end - else warning ("Save Failed (check if " ^ f ^ " is writable)") - end - | Some f -> - if current.analyzed_view#save f then - flash_info ("File " ^ f ^ " saved") - else warning ("Save Failed (check if " ^ f ^ " is writable)") - - ) - with - | e -> warning "Save: unexpected error" - in - let saveas_f _ = - let current = session_notebook#current_term in - try (match current.analyzed_view#filename with - | None -> - begin match select_file_for_save ~title:"Save file as" () - with - | None -> () - | Some f -> - if current.analyzed_view#save_as f then begin - current.tab_label#set_text (Filename.basename f); - flash_info "Saved" - end - else flash_info "Save Failed" - end - | Some f -> - begin match select_file_for_save - ~dir:(ref (Filename.dirname f)) - ~filename:(Filename.basename f) - ~title:"Save file as" () - with - | None -> () - | Some f -> - if current.analyzed_view#save_as f then begin - current.tab_label#set_text (Filename.basename f); - flash_info "Saved" - end else flash_info "Save Failed" - end); - with e -> flash_info "Save Failed" - in - let revert_f {analyzed_view = av} = - (try - match av#filename,av#stats with - | Some f,Some stats -> - let new_stats = Unix.stat f in - if new_stats.Unix.st_mtime > stats.Unix.st_mtime - then av#revert - | Some _, None -> av#revert - | _ -> () - with _ -> av#revert) + | Some f -> ignore (av#save f)) + session_notebook#pages + +let revert_all _ = List.iter FileAux.revert session_notebook#pages + +let quit _ = + try FileAux.check_quit saveall; exit 0 with FileAux.DontQuit -> () + +let close_buffer _ = + let do_remove () = + session_notebook#remove_page session_notebook#current_page in - let export_f kind _ = + let current = session_notebook#current_term in + if not current.script#buffer#modified then do_remove () + else + let answ = GToolbox.question_box ~title:"Close" + ~buttons:["Save Buffer and Close"; + "Close without Saving"; + "Don't Close"] + ~default:0 + ~icon:warn_image + "This buffer has unsaved modifications" + in + match answ with + | 1 when FileAux.check_save ~saveas:true current -> do_remove () + | 2 -> do_remove () + | _ -> () + +let export kind _ = + let av = current_view () in + match av#filename with + |None -> flash_info "Cannot print: this buffer has no name" + |Some f -> + let basef = Filename.basename f in + let output = + let basef_we = try Filename.chop_extension basef with _ -> basef in + match kind with + | "latex" -> basef_we ^ ".tex" + | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind + | _ -> assert false + in + let cmd = + local_cd f ^ current.cmd_coqdoc ^ " --" ^ kind ^ + " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) + in + let st,_ = run_command av cmd in + flash_info (cmd ^ pr_exit_status st) + +let print _ = + let av = current_view () in + match av#filename with + |None -> flash_info "Cannot print: this buffer has no name" + |Some f_name -> + let cmd = + local_cd f_name ^ current.cmd_coqdoc ^ " -ps " ^ + Filename.quote (Filename.basename f_name) ^ " | " ^ current.cmd_print + in + let w = GWindow.window ~title:"Print" ~modal:true + ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () + in + let v = GPack.vbox ~spacing:10 ~border_width:10 ~packing:w#add () + in + let _ = GMisc.label ~text:"Print using the following command:" + ~justify:`LEFT ~packing:v#add () + in + let e = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 + ~packing:v#add () + in + let h = GPack.hbox ~spacing:10 ~packing:v#add () + in + let ko = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:h#add () + in + let ok = GButton.button ~stock:`PRINT ~label:"Print" ~packing:h#add () + in + let callback_print () = + let cmd = e#text in + let st,_ = run_command av cmd in + flash_info (cmd ^ pr_exit_status st); + w#destroy () + in + ignore (ko#connect#clicked ~callback:w#destroy); + ignore (ok#connect#clicked ~callback:callback_print); + w#misc#show () + +let highlight _ = + let trm = session_notebook#current_term in + force_retag trm.script#buffer; + trm.analyzed_view#recenter_insert + +end + +(** For MacOSX : *) + +let forbid_quit_to_save () = + try FileAux.check_quit File.saveall; false + with FileAux.DontQuit -> true + +let do_load = FileAux.do_load + +(** Callbacks for external commands *) + +module External = struct + +let compile _ = + let v = session_notebook#current_term in + let av = v.analyzed_view in + File.save (); + match av#filename with + |None -> flash_info "Active buffer has no name" + |Some f -> + let cmd = current.cmd_coqc ^ " -I " + ^ (Filename.quote (Filename.dirname f)) + ^ " " ^ (Filename.quote f) in + let st,res = run_command av cmd in + if st = Unix.WEXITED 0 then + flash_info (f ^ " successfully compiled") + else begin + flash_info (f ^ " failed to compile"); + Coq.try_grab v.toplvl av#process_until_end_or_error ignore; + av#insert_message "Compilation output:\n"; + av#insert_message res + end + +let make _ = + let av = current_view () in + match av#filename with + |None -> flash_info "Cannot make: this buffer has no name" + |Some f -> + let cmd = local_cd f ^ current.cmd_make in + (* + save_f (); + *) + av#insert_message "Command output:\n"; + let st,res = run_command av cmd in + last_make := res; + last_make_index := 0; + flash_info (current.cmd_make ^ pr_exit_status st) + +let next_error _ = + try + let file,line,start,stop,error_msg = search_next_error () in + FileAux.do_load file; let v = session_notebook#current_term in let av = v.analyzed_view in - match av#filename with - | None -> - flash_info "Cannot print: this buffer has no name" - | Some f -> - let basef = Filename.basename f in - let output = - let basef_we = try Filename.chop_extension basef with _ -> basef in - match kind with - | "latex" -> basef_we ^ ".tex" - | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind - | _ -> assert false - in - let cmd = - local_cd f ^ current.cmd_coqdoc ^ " --" ^ kind ^ - " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) - in - let s,_ = CUnix.run_command Ideutils.try_convert av#insert_message cmd in - flash_info (cmd ^ - if s = Unix.WEXITED 0 - then " succeeded" - else " failed") - in - let quit_f _ = if not (forbid_quit_to_save ()) then exit 0 in - let emit_to_focus sgn = - let focussed_widget = GtkWindow.Window.get_focus w#as_window in - let obj = Gobject.unsafe_cast focussed_widget in - try GtkSignal.emit_unit obj sgn - with _ -> () - in + let input_buffer = v.script#buffer in + let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in + let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in + input_buffer#apply_tag Tags.Script.error ~start:starti ~stop:stopi; + input_buffer#place_cursor ~where:starti; + av#set_message error_msg; + v.script#misc#grab_focus () + with Not_found -> + last_make_index := 0; + let v = session_notebook#current_term in + let av = v.analyzed_view in + av#set_message "No more errors.\n" -(* begin Preferences *) - let reset_revert_timer () = - disconnect_revert_timer (); - if current.global_auto_revert then - revert_timer := Some - (GMain.Timeout.add ~ms:current.global_auto_revert_delay - ~callback: - (fun () -> - List.iter (fun p -> do_if_not_computing p "revert" (fun _ -> sync revert_f p)) session_notebook#pages; - true)) - in reset_revert_timer (); (* to enable statup preferences timer *) - (* XXX *) - let auto_save_f {analyzed_view = av} = - (try - av#auto_save - with _ -> ()) - in +let coq_makefile _ = + let av = current_view () in + match av#filename with + |None -> flash_info "Cannot make makefile: this buffer has no name" + |Some f -> + let cmd = local_cd f ^ current.cmd_coqmakefile in + let st,res = run_command av cmd in + flash_info (current.cmd_coqmakefile ^ pr_exit_status st) + +let editor _ = + let av = current_view () in + match av#filename with + |None -> warning "Call to external editor available only on named files" + |Some f -> + File.save (); + let f = Filename.quote f in + let cmd = Util.subst_command_placeholder current.cmd_editor f in + let _ = run_command av cmd in + av#revert - let reset_auto_save_timer () = - disconnect_auto_save_timer (); - if current.auto_save then - auto_save_timer := Some - (GMain.Timeout.add ~ms:current.auto_save_delay - ~callback: - (fun () -> - List.iter (fun p -> do_if_not_computing p "autosave" (fun _ -> sync auto_save_f p)) session_notebook#pages; - true)) - in reset_auto_save_timer (); (* to enable statup preferences timer *) -(* end Preferences *) - - let do_or_activate f () = - let p = session_notebook#current_term in - do_if_not_computing p "do_or_activate" - (fun handle -> - let av = p.analyzed_view in - ignore (f handle av); - pop_info (); - let msg = match Coq.status handle with +end + +(** Callbacks for the Navigation menu *) + +let do_or_activate f = + let p = session_notebook#current_term in + do_if_not_computing p "do_or_activate" + (fun handle -> + let av = p.analyzed_view in + ignore (f handle av); + pop_info (); + let msg = match Coq.status handle with | Interface.Fail (l, str) -> "Oops, problem while fetching coq status." | Interface.Good status | Interface.Unsafe status -> let path = match status.Interface.status_path with - | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *) - | _ :: l -> " in " ^ String.concat "." l + | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *) + | _ :: l -> " in " ^ String.concat "." l in let name = match status.Interface.status_proofname with - | None -> "" - | Some n -> ", proving " ^ n + | None -> "" + | Some n -> ", proving " ^ n in "Ready" ^ path ^ name + in + push_info msg) + +let do_if_active f = + let p = session_notebook#current_term in + do_if_not_computing p "do_if_active" + (fun handle -> ignore (f handle p.analyzed_view)) + +module Nav = struct + let forward_one _ = do_or_activate (fun h a -> a#process_next_phrase h) + let backward_one _ = do_or_activate (fun h a -> a#backtrack_last_phrase h) + let goto _ = do_or_activate (fun h a -> a#go_to_insert h) + let restart _ = force_reset_initial () + let goto_end _ = do_or_activate (fun h a -> a#process_until_end_or_error h) + let interrupt _ = break () + let previous_occ _ = (current_view ())#find_next_occurrence Up + let next_occ _ = (current_view ())#find_next_occurrence Down +end + +let tactic_wizard_callback l _ = + do_if_active (fun h a -> a#tactic_wizard h l) + +let printopts_callback opts v = + let b = v#get_active in + let opts = List.map (fun o -> (o,b)) opts in + do_or_activate (fun h av -> + Coq.PrintOpt.set h opts; + av#show_goals h) + +(** Templates menu *) + +let match_callback _ = + let w = get_current_word () in + let coqtop = session_notebook#current_term.toplvl in + try + Coq.try_grab coqtop begin fun handle -> match Coq.mkcases handle w with + | Interface.Fail _ -> raise Not_found + | Interface.Good cases | Interface.Unsafe cases -> + let print_branch c l = + Format.fprintf c " | @[<hov 1>%a@]=> _@\n" + (print_list (fun c s -> Format.fprintf c "%s@ " s)) l in - push_info msg - ) + let b = Buffer.create 1024 in + let fmt = Format.formatter_of_buffer b in + Format.fprintf fmt "@[match var with@\n%aend@]@." + (print_list print_branch) cases; + let s = Buffer.contents b in + Minilib.log s; + let {script = view } = session_notebook#current_term in + ignore (view#buffer#delete_selection ()); + let m = view#buffer#create_mark + (view#buffer#get_iter `INSERT) + in + if view#buffer#insert_interactive s then + let i = view#buffer#get_iter (`MARK m) in + let _ = i#nocopy#forward_chars 9 in + view#buffer#place_cursor ~where:i; + view#buffer#move_mark ~where:(i#backward_chars 3) `SEL_BOUND + end ignore + with Not_found -> flash_info "Not an inductive type" + +(** Queries *) + +module Query = struct + +let searchabout () = + let word = get_current_word () in + let term = session_notebook#current_term in + let query handle = + let results = Coq.search handle [Interface.SubType_Pattern word, true] in + let results = match results with | Interface.Good l -> l | _ -> [] in + let buf = term.message_view#buffer in + let insert result = + let qualid = result.Interface.coq_object_qualid in + let name = String.concat "." qualid in + let tpe = result.Interface.coq_object_object in + buf#insert ~tags:[Tags.Message.item] name; + buf#insert "\n"; + buf#insert tpe; + buf#insert "\n"; + in + term.message_view#clear (); + List.iter insert results + in + Coq.try_grab term.toplvl query ignore + +let otherquery command _ = + let word = get_current_word () in + let term = session_notebook#current_term in + let f query handle = term.analyzed_view#raw_coq_query handle query in + if not (word = "") then + let query = command ^ " " ^ word ^ "." in + term.message_view#clear (); + try Coq.try_grab term.toplvl (f query) ignore + with e -> term.message_view#push Interface.Error (Printexc.to_string e) + +let query command _ = + if command = "SearchAbout" + then searchabout () + else otherquery command () + +end + +(** Misc *) + +module MiscMenu = struct + +let detach_view _ = + (* Open a separate window containing the current buffer *) + let trm = session_notebook#current_term in + let file = match trm.analyzed_view#filename with + |None -> "*scratch*" + |Some f -> f in - let do_if_active f () = - let p = session_notebook#current_term in - do_if_not_computing p "do_if_active" - (fun handle -> ignore (f handle p.analyzed_view)) + let w = GWindow.window ~show:true ~title:file ~position:`CENTER + ~width:(current.window_width*2/3) + ~height:(current.window_height*2/3) + () in - let match_callback _ = - let w = get_current_word () in - let coqtop = session_notebook#current_term.toplvl in - try - Coq.try_grab coqtop begin fun handle -> match Coq.mkcases handle w with - | Interface.Fail _ -> raise Not_found - | Interface.Good cases | Interface.Unsafe cases -> - let print_branch c l = - Format.fprintf c " | @[<hov 1>%a@]=> _@\n" - (print_list (fun c s -> Format.fprintf c "%s@ " s)) l - in - let b = Buffer.create 1024 in - let fmt = Format.formatter_of_buffer b in - Format.fprintf fmt "@[match var with@\n%aend@]@." - (print_list print_branch) cases; - let s = Buffer.contents b in - Minilib.log s; - let {script = view } = session_notebook#current_term in - ignore (view#buffer#delete_selection ()); - let m = view#buffer#create_mark - (view#buffer#get_iter `INSERT) - in - if view#buffer#insert_interactive s then - let i = view#buffer#get_iter (`MARK m) in - let _ = i#nocopy#forward_chars 9 in - view#buffer#place_cursor ~where:i; - view#buffer#move_mark ~where:(i#backward_chars 3) - `SEL_BOUND - end ignore - with Not_found -> flash_info "Not an inductive type" + let sb = GBin.scrolled_window ~packing:w#add () in -(* External command callback *) - let compile_f _ = - let v = session_notebook#current_term in - let av = v.analyzed_view in - save_f (); - match av#filename with - | None -> - flash_info "Active buffer has no name" - | Some f -> - let cmd = current.cmd_coqc ^ " -I " - ^ (Filename.quote (Filename.dirname f)) - ^ " " ^ (Filename.quote f) in - let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in - if s = Unix.WEXITED 0 then - flash_info (f ^ " successfully compiled") - else begin - flash_info (f ^ " failed to compile"); - Coq.try_grab v.toplvl av#process_until_end_or_error ignore; - av#insert_message "Compilation output:\n"; - av#insert_message res - end + let nv = GText.view ~buffer:trm.script#buffer ~packing:sb#add () in - let make_f _ = - let v = session_notebook#current_term in - let av = v.analyzed_view in - match av#filename with - | None -> - flash_info "Cannot make: this buffer has no name" - | Some f -> - let cmd = local_cd f ^ current.cmd_make in - - (* - save_f (); - *) - av#insert_message "Command output:\n"; - let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in - last_make := res; - last_make_index := 0; - flash_info (current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") + nv#misc#modify_font current.text_font; + (* If the buffer in the main window is closed, destroy this detached view *) + ignore (trm.script#connect#destroy ~callback:w#destroy) + +let initial_about () = + let initial_string = + "Welcome to CoqIDE, an Integrated Development Environment for Coq" in - let next_error _ = - try - let file,line,start,stop,error_msg = search_next_error () in - do_load file; - let v = session_notebook#current_term in - let av = v.analyzed_view in - let input_buffer = v.script#buffer in - (* - let init = input_buffer#start_iter in - let i = init#forward_lines (line-1) in - *) - (* - let convert_pos = byte_offset_to_char_offset phrase in - let start = convert_pos start in - let stop = convert_pos stop in - *) - (* - let starti = i#forward_chars start in - let stopi = i#forward_chars stop in - *) - let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in - let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in - input_buffer#apply_tag Tags.Script.error - ~start:starti - ~stop:stopi; - input_buffer#place_cursor ~where:starti; - av#set_message error_msg; - v.script#misc#grab_focus () - with Not_found -> - last_make_index := 0; - let v = session_notebook#current_term in - let av = v.analyzed_view in - av#set_message "No more errors.\n" + let coq_version = Coq.short_version () in + let version_info = + if Glib.Utf8.validate coq_version then + "\nYou are running " ^ coq_version + else "" in - let coq_makefile_f _ = - let v = session_notebook#current_term in - let av = v.analyzed_view in - match av#filename with - | None -> - flash_info "Cannot make makefile: this buffer has no name" - | Some f -> - let cmd = local_cd f ^ current.cmd_coqmakefile in - let s,res = CUnix.run_command Ideutils.try_convert av#insert_message cmd in - flash_info - (current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") + let msg = initial_string ^ version_info in + session_notebook#current_term.message_view#push Interface.Notice msg + +let coq_icon () = + (* May raise Nof_found *) + let name = "coq.png" in + let chk d = Sys.file_exists (Filename.concat d name) in + let dir = List.find chk (Minilib.coqide_data_dirs ()) in + Filename.concat dir name + +let about _ = + let dialog = GWindow.about_dialog () in + let _ = dialog#connect#response (fun _ -> dialog#destroy ()) in + let _ = + try dialog#set_logo (GdkPixbuf.from_file (coq_icon ())) + with _ -> () + in + let copyright = + "Coq is developed by the Coq Development Team\n\ + (INRIA - CNRS - LIX - LRI - PPS)" in + let authors = [ + "Benjamin Monate"; + "Jean-Christophe Filliâtre"; + "Pierre Letouzey"; + "Claude Marché"; + "Bruno Barras"; + "Pierre Corbineau"; + "Julien Narboux"; + "Hugo Herbelin" ] + in + dialog#set_name "CoqIDE"; + dialog#set_comments "The Coq Integrated Development Environment"; + dialog#set_website Coq_config.wwwcoq; + dialog#set_version Coq_config.version; + dialog#set_copyright copyright; + dialog#set_authors authors; + dialog#show () - let file_actions = GAction.action_group ~name:"File" () in - let edit_actions = GAction.action_group ~name:"Edit" () in - let view_actions = GAction.action_group ~name:"View" () in - let export_actions = GAction.action_group ~name:"Export" () in - let navigation_actions = GAction.action_group ~name:"Navigation" () in - let tactics_actions = GAction.action_group ~name:"Tactics" () in - let templates_actions = GAction.action_group ~name:"Templates" () in - let tools_actions = GAction.action_group ~name:"Tools" () in - let queries_actions = GAction.action_group ~name:"Queries" () in - let compile_actions = GAction.action_group ~name:"Compile" () in - let windows_actions = GAction.action_group ~name:"Windows" () in - let help_actions = GAction.action_group ~name:"Help" () in - let add_gen_actions menu_name act_grp l = - let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) in - let add_simple_template menu_name act_grp text = - let text' = - let l = String.length text - 1 in - if String.get text l = '.' - then text ^"\n" - else text ^" " - in - GAction.add_action (menu_name^" "^(no_under text)) ~label:text - ~callback:(fun _ -> let {script = view } = session_notebook#current_term in - ignore (view#buffer#insert_interactive text')) act_grp + let comment _ = session_notebook#current_term.script#comment () + let uncomment _ = session_notebook#current_term.script#uncomment () + +end + +(** Refresh functions *) + +let refresh_editor_prefs () = + let wrap_mode = if current.dynamic_word_wrap then `WORD else `NONE in + let show_spaces = + if current.show_spaces then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *) + else 0 + in + let fd = current.text_font in + let clr = Tags.color_of_string current.background_color + in + let iter_page p = + (* Editor settings *) + p.script#set_wrap_mode wrap_mode; + p.script#set_show_line_numbers current.show_line_number; + p.script#set_auto_indent current.auto_indent; + p.script#set_highlight_current_line current.highlight_current_line; + + (* Hack to handle missing binding in lablgtk *) + let conv = { Gobject.name = "draw-spaces"; Gobject.conv = Gobject.Data.int } in - List.iter (function - | [] -> () - | [s] -> add_simple_template menu_name act_grp s - | s::_ as ll -> let label = "_@..." in label.[1] <- s.[0]; - GAction.add_action (menu_name^" "^(String.make 1 s.[0])) ~label act_grp; - List.iter (add_simple_template menu_name act_grp) ll - ) l + Gobject.set conv p.script#as_widget show_spaces; + + p.script#set_show_right_margin current.show_right_margin; + p.script#set_insert_spaces_instead_of_tabs + current.spaces_instead_of_tabs; + p.script#set_tab_width current.tab_length; + p.script#set_auto_complete current.auto_complete; + + (* Fonts *) + p.script#misc#modify_font fd; + p.proof_view#misc#modify_font fd; + p.message_view#misc#modify_font fd; + p.command#refresh_font (); + + (* Colors *) + p.script#misc#modify_base [`NORMAL, `COLOR clr]; + p.proof_view#misc#modify_base [`NORMAL, `COLOR clr]; + p.message_view#misc#modify_base [`NORMAL, `COLOR clr]; + p.command#refresh_color () + in - let tactic_shortcut s sc = GAction.add_action s ~label:("_"^s) - ~accel:(current.modifier_for_tactics^sc) - ~callback:(fun _ -> do_if_active (fun handle a -> a#tactic_wizard handle [s]) ()) in - let query_searchabout () = - let word = get_current_word () in - let term = session_notebook#current_term in - let query handle = - let results = Coq.search handle [Interface.SubType_Pattern word, true] in - let results = match results with | Interface.Good l -> l | _ -> [] in - let buf = term.message_view#buffer in - let insert result = - let qualid = result.Interface.coq_object_qualid in - let name = String.concat "." qualid in - let tpe = result.Interface.coq_object_object in - buf#insert ~tags:[Tags.Message.item] name; - buf#insert "\n"; - buf#insert tpe; - buf#insert "\n"; - in - term.message_view#clear (); - List.iter insert results + List.iter iter_page session_notebook#pages + + +(** Wrappers around GAction functions for creating menus *) + +let menu = GAction.add_actions +let item = GAction.add_action + +(** Toggle items in menus for printing options *) + +let toggle_item = GAction.add_toggle_action + +let toggle_items menu_name l = + let f (opts,name,label,key,dflt) = + toggle_item name ~active:dflt ~label + ~accel:(current.modifier_for_display^key) + ~callback:(printopts_callback opts) + menu_name + in + List.iter f l + +(** Create alphabetical menu items with elements in sub-items. + [l] is a list of lists, one per initial letter *) + +let alpha_items menu_name item_name l = + let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) + in + let mk_item text = + let text' = + let last = String.length text - 1 in + if text.[last] = '.' + then text ^"\n" + else text ^" " in - Coq.try_grab term.toplvl query ignore + item (item_name^" "^(no_under text)) ~label:text + ~callback:(fun _ -> + let v = session_notebook#current_term.script in + ignore (v#buffer#insert_interactive text')) + menu_name in - let query_callback command _ = - let word = get_current_word () in - let term = session_notebook#current_term in - let f query handle = term.analyzed_view#raw_coq_query handle query in - if not (word = "") then - let query = command ^ " " ^ word ^ "." in - term.message_view#clear (); - try Coq.try_grab term.toplvl (f query) ignore - with e -> term.message_view#push Interface.Error (Printexc.to_string e) + let mk_items = function + | [] -> () + | [s] -> mk_item s + | s::_ as ll -> + let name = item_name^" "^(String.make 1 s.[0]) in + let label = "_@..." in label.[1] <- s.[0]; + item name ~label menu_name; + List.iter mk_item ll in - let query_callback command _ = - if command = "SearchAbout" then query_searchabout () else query_callback command () + List.iter mk_items l + +(** Create a menu item that will insert a given text, + and select the zone given by (offset,len). + The first word in the text is used as item keyword. + Caveat: the offset is now from the start of the text. *) + +let template_item (text, offset, len, key) = + let modifier = current.modifier_for_templates in + let idx = String.index text ' ' in + let name = String.sub text 0 idx in + let label = "_"^name^" __" in + let negoffset = String.length text - offset - len in + let callback _ = + let view = session_notebook#current_term.script in + if view#buffer#insert_interactive text then begin + let iter = view#buffer#get_iter_at_mark `INSERT in + ignore (iter#nocopy#backward_chars negoffset); + view#buffer#move_mark `INSERT ~where:iter; + ignore (iter#nocopy#backward_chars len); + view#buffer#move_mark `SEL_BOUND ~where:iter; + end in - let query_shortcut s accel = - GAction.add_action s ~label:("_"^s) ?accel ~callback:(query_callback s) + item name ~label ~callback ~accel:(modifier^key) + +(** Creation of the main coqide window *) + +let build_ui () = + let w = GWindow.window + ~wm_class:"CoqIde" ~wm_name:"CoqIde" + ~allow_grow:true ~allow_shrink:true + ~width:current.window_width ~height:current.window_height + ~title:"CoqIde" () in - let comment_f _ = session_notebook#current_term.script#comment () in - let uncomment_f _ = session_notebook#current_term.script#uncomment () in - let add_complex_template (name, label, text, offset, len, key) = - (* Templates/Lemma *) - let callback _ = - let {script = view } = session_notebook#current_term in - if view#buffer#insert_interactive text then begin - let iter = view#buffer#get_iter_at_mark `INSERT in - ignore (iter#nocopy#backward_chars offset); - view#buffer#move_mark `INSERT ~where:iter; - ignore (iter#nocopy#backward_chars len); - view#buffer#move_mark `SEL_BOUND ~where:iter; - end in - match key with - |Some ac -> GAction.add_action name ~label ~callback ~accel:(current.modifier_for_templates^ac) - |None -> GAction.add_action name ~label ~callback ?accel:None + let () = + try w#set_icon (Some (GdkPixbuf.from_file (MiscMenu.coq_icon ()))) + with _ -> () in - let detach_view _ = - (* Open a separate window containing the current buffer *) - let trm = session_notebook#current_term in - let file = match trm.analyzed_view#filename with - | None -> "*scratch*" - | Some f -> f - in - let w = GWindow.window ~show:true - ~width:(current.window_width*2/3) - ~height:(current.window_height*2/3) - ~position:`CENTER - ~title:file - () - in - let sb = GBin.scrolled_window ~packing:w#add () - in - let nv = GText.view ~buffer:trm.script#buffer ~packing:sb#add () - in - nv#misc#modify_font current.text_font; - (* If the buffer in the main window is closed, destroy this detached view *) - ignore (trm.script#connect#destroy ~callback:w#destroy) + let _ = w#event#connect#delete ~callback:(fun _ -> File.quit (); true) + in + let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in + + let emit_to_focus sgn = + let focussed_widget = GtkWindow.Window.get_focus w#as_window in + let obj = Gobject.unsafe_cast focussed_widget in + try GtkSignal.emit_unit obj sgn + with _ -> () in - GAction.add_actions file_actions [ - GAction.add_action "File" ~label:"_File"; - GAction.add_action "New" ~callback:new_f ~stock:`NEW; - GAction.add_action "Open" ~callback:load_f ~stock:`OPEN; - GAction.add_action "Save" ~callback:save_f ~stock:`SAVE ~tooltip:"Save current buffer"; - GAction.add_action "Save as" ~label:"S_ave as" ~callback:saveas_f ~stock:`SAVE_AS; - GAction.add_action "Save all" ~label:"Sa_ve all" ~callback:(fun _ -> saveall_f ()); - GAction.add_action "Revert all buffers" ~label:"_Revert all buffers" ~callback:(fun _ -> List.iter revert_f session_notebook#pages) ~stock:`REVERT_TO_SAVED; - GAction.add_action "Close buffer" ~label:"_Close buffer" ~callback:(fun _ -> remove_current_view_page ()) ~stock:`CLOSE ~tooltip:"Close current buffer"; - GAction.add_action "Print..." ~label:"_Print..." ~callback:(fun _ -> do_print session_notebook#current_term) ~stock:`PRINT ~accel:"<Ctrl>p"; - GAction.add_action "Rehighlight" ~label:"Reh_ighlight" ~accel:"<Ctrl>l" - ~callback:(fun _ -> force_retag - session_notebook#current_term.script#buffer; - session_notebook#current_term.analyzed_view#recenter_insert) - ~stock:`REFRESH; - GAction.add_action "Quit" ~callback:quit_f ~stock:`QUIT; - ]; - GAction.add_actions export_actions [ - GAction.add_action "Export to" ~label:"E_xport to"; - GAction.add_action "Html" ~label:"_Html" ~callback:(export_f "html"); - GAction.add_action "Latex" ~label:"_LaTeX" ~callback:(export_f "latex"); - GAction.add_action "Dvi" ~label:"_Dvi" ~callback:(export_f "dvi"); - GAction.add_action "Pdf" ~label:"_Pdf" ~callback:(export_f "pdf"); - GAction.add_action "Ps" ~label:"_Ps" ~callback:(export_f "ps"); - ]; - GAction.add_actions edit_actions [ - GAction.add_action "Edit" ~label:"_Edit"; - GAction.add_action "Undo" ~accel:"<Ctrl>u" - ~callback:(fun _ -> - let term = session_notebook#current_term in - do_if_not_computing term "undo" - (fun handle -> - ignore (term.script#undo ()))) ~stock:`UNDO; - GAction.add_action "Redo" ~stock:`REDO - ~callback:(fun _ -> ignore (session_notebook#current_term.script#redo ())); - GAction.add_action "Cut" - ~callback:(fun _ -> emit_to_focus GtkText.View.S.cut_clipboard) ~stock:`CUT; - GAction.add_action "Copy" - ~callback:(fun _ -> emit_to_focus GtkText.View.S.copy_clipboard) ~stock:`COPY; - GAction.add_action "Paste" - ~callback:(fun _ -> emit_to_focus GtkText.View.S.paste_clipboard) ~stock:`PASTE; - GAction.add_action "Find" ~stock:`FIND - ~callback:(fun _ -> session_notebook#current_term.finder#show `FIND); - GAction.add_action "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3" - ~callback:(fun _ -> session_notebook#current_term.finder#find_forward ()); - GAction.add_action "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP ~accel:"<Shift>F3" - ~callback:(fun _ -> session_notebook#current_term.finder#find_backward ()); - GAction.add_action "Replace" ~stock:`FIND_AND_REPLACE - ~callback:(fun _ -> session_notebook#current_term.finder#show `REPLACE); - GAction.add_action "Close Find" ~accel:"Escape" - ~callback:(fun _ -> session_notebook#current_term.finder#hide ()); - GAction.add_action "Complete Word" ~label:"Complete Word" ~callback:(fun _ -> - ignore ( () + + (* begin Preferences *) + let reset_revert_timer () = + disconnect_revert_timer (); + if current.global_auto_revert then + revert_timer := Some + (GMain.Timeout.add ~ms:current.global_auto_revert_delay + ~callback:(fun () -> File.revert_all (); true)) + in reset_revert_timer (); (* to enable statup preferences timer *) + + let reset_auto_save_timer () = + let autosave p = try p.analyzed_view#auto_save with _ -> () in + let autosave_all () = List.iter autosave session_notebook#pages; true in + disconnect_auto_save_timer (); + if current.auto_save then + auto_save_timer := Some + (GMain.Timeout.add ~ms:current.auto_save_delay ~callback:autosave_all) + in reset_auto_save_timer (); (* to enable statup preferences timer *) + (* end Preferences *) + + let file_menu = GAction.action_group ~name:"File" () in + let edit_menu = GAction.action_group ~name:"Edit" () in + let view_menu = GAction.action_group ~name:"View" () in + let export_menu = GAction.action_group ~name:"Export" () in + let navigation_menu = GAction.action_group ~name:"Navigation" () in + let tactics_menu = GAction.action_group ~name:"Tactics" () in + let templates_menu = GAction.action_group ~name:"Templates" () in + let tools_menu = GAction.action_group ~name:"Tools" () in + let queries_menu = GAction.action_group ~name:"Queries" () in + let compile_menu = GAction.action_group ~name:"Compile" () in + let windows_menu = GAction.action_group ~name:"Windows" () in + let help_menu = GAction.action_group ~name:"Help" () in + + menu file_menu [ + item "File" ~label:"_File"; + item "New" ~callback:File.newfile ~stock:`NEW; + item "Open" ~callback:File.load ~stock:`OPEN; + item "Save" ~callback:File.save ~stock:`SAVE ~tooltip:"Save current buffer"; + item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:File.saveas; + item "Save all" ~label:"Sa_ve all" ~callback:File.saveall; + item "Revert all buffers" ~label:"_Revert all buffers" + ~callback:File.revert_all ~stock:`REVERT_TO_SAVED; + item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE + ~callback:File.close_buffer~tooltip:"Close current buffer"; + item "Print..." ~label:"_Print..." + ~callback:File.print ~stock:`PRINT ~accel:"<Ctrl>p"; + item "Rehighlight" ~label:"Reh_ighlight" ~accel:"<Ctrl>l" + ~callback:File.highlight ~stock:`REFRESH; + item "Quit" ~stock:`QUIT ~callback:File.quit; + ]; + + menu export_menu [ + item "Export to" ~label:"E_xport to"; + item "Html" ~label:"_Html" ~callback:(File.export "html"); + item "Latex" ~label:"_LaTeX" ~callback:(File.export "latex"); + item "Dvi" ~label:"_Dvi" ~callback:(File.export "dvi"); + item "Pdf" ~label:"_Pdf" ~callback:(File.export "pdf"); + item "Ps" ~label:"_Ps" ~callback:(File.export "ps"); + ]; + + menu edit_menu [ + item "Edit" ~label:"_Edit"; + item "Undo" ~accel:"<Ctrl>u" ~stock:`UNDO + ~callback:(fun _ -> + let term = session_notebook#current_term in + do_if_not_computing term "undo" + (fun handle -> + ignore (term.script#undo ()))); + item "Redo" ~stock:`REDO + ~callback:(fun _ -> ignore (session_notebook#current_term.script#redo ())); + item "Cut" ~stock:`CUT + ~callback:(fun _ -> emit_to_focus GtkText.View.S.cut_clipboard); + item "Copy" ~stock:`COPY + ~callback:(fun _ -> emit_to_focus GtkText.View.S.copy_clipboard); + item "Paste" ~stock:`PASTE + ~callback:(fun _ -> emit_to_focus GtkText.View.S.paste_clipboard); + item "Find" ~stock:`FIND + ~callback:(fun _ -> session_notebook#current_term.finder#show `FIND); + item "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3" + ~callback:(fun _ -> session_notebook#current_term.finder#find_forward ()); + item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP + ~accel:"<Shift>F3" + ~callback:(fun _ -> session_notebook#current_term.finder#find_backward ()); + item "Replace" ~stock:`FIND_AND_REPLACE + ~callback:(fun _ -> session_notebook#current_term.finder#show `REPLACE); + item "Close Find" ~accel:"Escape" + ~callback:(fun _ -> session_notebook#current_term.finder#hide ()); + item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash" + ~callback:(fun _ -> + ignore ( () (* let av = session_notebook#current_term.analyzed_view in av#complete_at_offset (av#get_insert)#offset*) - )) ~accel:"<Ctrl>slash"; - GAction.add_action "External editor" ~label:"External editor" ~callback:(fun _ -> - let av = session_notebook#current_term.analyzed_view in - match av#filename with - | None -> warning "Call to external editor available only on named files" - | Some f -> - save_f (); - let com = Util.subst_command_placeholder current.cmd_editor (Filename.quote f) in - let _ = CUnix.run_command Ideutils.try_convert av#insert_message com in - av#revert) ~stock:`EDIT; - GAction.add_action "Preferences" ~callback:(fun _ -> - begin + )); + item "External editor" ~label:"External editor" ~stock:`EDIT + ~callback:External.editor; + item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES + ~callback:(fun _ -> + begin try configure ~apply:update_notebook_pos () with _ -> flash_info "Cannot save preferences" - end; - reset_revert_timer ()) ~accel:"<Ctrl>comma" ~stock:`PREFERENCES; - (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ]; - GAction.add_actions view_actions [ - GAction.add_action "View" ~label:"_View"; - GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<Alt>Left") ~stock:`GO_BACK - ~callback:(fun _ -> session_notebook#previous_page ()); - GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<Alt>Right") ~stock:`GO_FORWARD - ~callback:(fun _ -> session_notebook#next_page ()); - GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar" - ~active:(current.show_toolbar) ~callback: - (fun _ -> current.show_toolbar <- not current.show_toolbar; - !refresh_toolbar_hook ()); - GAction.add_toggle_action "Show Query Pane" ~label:"Show _Query Pane" - ~callback:(fun _ -> let ccw = session_notebook#current_term.command in - if ccw#frame#misc#visible - then ccw#frame#misc#hide () - else ccw#frame#misc#show ()) - ~accel:"<Alt>Escape"; - ]; - List.iter - (fun (opts,name,label,key,dflt) -> - GAction.add_toggle_action name ~active:dflt ~label - ~accel:(current.modifier_for_display^key) - ~callback:(fun v -> do_or_activate (fun handle av -> - let () = setopts handle opts v#get_active in - av#show_goals handle) ()) view_actions) - print_items; - GAction.add_actions navigation_actions [ - GAction.add_action "Navigation" ~label:"_Navigation"; - GAction.add_action "Forward" ~label:"_Forward" ~stock:`GO_DOWN - ~callback:(fun _ -> do_or_activate (fun handle a -> a#process_next_phrase handle true) ()) - ~tooltip:"Forward one command" ~accel:(current.modifier_for_navigation^"Down"); - GAction.add_action "Backward" ~label:"_Backward" ~stock:`GO_UP - ~callback:(fun _ -> do_or_activate (fun handle a -> a#backtrack_last_phrase handle) ()) - ~tooltip:"Backward one command" ~accel:(current.modifier_for_navigation^"Up"); - GAction.add_action "Go to" ~label:"_Go to" ~stock:`JUMP_TO - ~callback:(fun _ -> do_or_activate (fun handle a -> a#go_to_insert handle) ()) - ~tooltip:"Go to cursor" ~accel:(current.modifier_for_navigation^"Right"); - GAction.add_action "Start" ~label:"_Start" ~stock:`GOTO_TOP - ~callback:(fun _ -> force_reset_initial ()) - ~tooltip:"Restart coq" ~accel:(current.modifier_for_navigation^"Home"); - GAction.add_action "End" ~label:"_End" ~stock:`GOTO_BOTTOM - ~callback:(fun _ -> do_or_activate (fun handle a -> a#process_until_end_or_error handle) ()) - ~tooltip:"Go to end" ~accel:(current.modifier_for_navigation^"End"); - GAction.add_action "Interrupt" ~label:"_Interrupt" ~stock:`STOP - ~callback:(fun _ -> break ()) ~tooltip:"Interrupt computations" - ~accel:(current.modifier_for_navigation^"Break"); + end; + reset_revert_timer ()); + ]; + + menu view_menu [ + item "View" ~label:"_View"; + item "Previous tab" ~label:"_Previous tab" ~accel:"<Alt>Left" + ~stock:`GO_BACK + ~callback:(fun _ -> session_notebook#previous_page ()); + item "Next tab" ~label:"_Next tab" ~accel:"<Alt>Right" + ~stock:`GO_FORWARD + ~callback:(fun _ -> session_notebook#next_page ()); + toggle_item "Show Toolbar" ~label:"Show _Toolbar" + ~active:(current.show_toolbar) + ~callback:(fun _ -> + current.show_toolbar <- not current.show_toolbar; + !refresh_toolbar_hook ()); + toggle_item "Show Query Pane" ~label:"Show _Query Pane" + ~accel:"<Alt>Escape" + ~callback:(fun _ -> + let ccw = session_notebook#current_term.command in + if ccw#frame#misc#visible + then ccw#frame#misc#hide () + else ccw#frame#misc#show ()) + ]; + toggle_items view_menu print_items; + + menu navigation_menu [ + item "Navigation" ~label:"_Navigation"; + item "Forward" ~label:"_Forward" ~stock:`GO_DOWN ~callback:Nav.forward_one + ~tooltip:"Forward one command" + ~accel:(current.modifier_for_navigation^"Down"); + item "Backward" ~label:"_Backward" ~stock:`GO_UP ~callback:Nav.backward_one + ~tooltip:"Backward one command" + ~accel:(current.modifier_for_navigation^"Up"); + item "Go to" ~label:"_Go to" ~stock:`JUMP_TO ~callback:Nav.goto + ~tooltip:"Go to cursor" + ~accel:(current.modifier_for_navigation^"Right"); + item "Start" ~label:"_Start" ~stock:`GOTO_TOP ~callback:Nav.restart + ~tooltip:"Restart coq" + ~accel:(current.modifier_for_navigation^"Home"); + item "End" ~label:"_End" ~stock:`GOTO_BOTTOM ~callback:Nav.goto_end + ~tooltip:"Go to end" + ~accel:(current.modifier_for_navigation^"End"); + item "Interrupt" ~label:"_Interrupt" ~stock:`STOP ~callback:Nav.interrupt + ~tooltip:"Interrupt computations" + ~accel:(current.modifier_for_navigation^"Break"); (* wait for this available in GtkSourceView ! - GAction.add_action "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE + item "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE ~callback:(fun _ -> let sess = session_notebook#current_term in toggle_proof_visibility sess.script#buffer sess.analyzed_view#get_insert) ~tooltip:"Hide proof" ~accel:(current.modifier_for_navigation^"h");*) - GAction.add_action "Previous" ~label:"_Previous" ~stock:`GO_BACK - ~callback:(fun _ -> do_or_activate (fun _ a -> a#go_to_prev_occ_of_cur_word) ()) - ~tooltip:"Previous occurence" ~accel:(current.modifier_for_navigation^"less"); - GAction.add_action "Next" ~label:"_Next" ~stock:`GO_FORWARD - ~callback:(fun _ -> do_or_activate (fun _ a -> a#go_to_next_occ_of_cur_word) ()) - ~tooltip:"Next occurence" ~accel:(current.modifier_for_navigation^"greater"); - ]; - GAction.add_actions tactics_actions [ - GAction.add_action "Try Tactics" ~label:"_Try Tactics"; - GAction.add_action "Wizard" ~tooltip:"Proof Wizard" ~label:"<Proof Wizard>" - ~stock:`DIALOG_INFO ~callback:(fun _ -> do_if_active (fun handle a -> a#tactic_wizard handle - current.automatic_tactics) ()) - ~accel:(current.modifier_for_tactics^"dollar"); - tactic_shortcut "auto" "a"; - tactic_shortcut "auto with *" "asterisk"; - tactic_shortcut "eauto" "e"; - tactic_shortcut "eauto with *" "ampersand"; - tactic_shortcut "intuition" "i"; - tactic_shortcut "omega" "o"; - tactic_shortcut "simpl" "s"; - tactic_shortcut "tauto" "p"; - tactic_shortcut "trivial" "v"; - ]; - add_gen_actions "Tactic" tactics_actions Coq_commands.tactics; - GAction.add_actions templates_actions [ - GAction.add_action "Templates" ~label:"Te_mplates"; - add_complex_template - ("Lemma", "_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n", - 19, 9, Some "L"); - add_complex_template - ("Theorem", "_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n", - 19, 11, Some "T"); - add_complex_template - ("Definition", "_Definition __", "Definition ident := .\n", - 6, 5, Some "E"); - add_complex_template - ("Inductive", "_Inductive __", "Inductive ident : :=\n | : .\n", - 14, 5, Some "I"); - add_complex_template - ("Fixpoint", "_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", - 29, 5, Some "F"); - add_complex_template ("Scheme", "_Scheme __", - "Scheme new_scheme := Induction for _ Sort _\ -\nwith _ := Induction for _ Sort _.\n",61,10, Some "S"); - GAction.add_action "match" ~label:"match ..." ~callback:match_callback - ~accel:(current.modifier_for_templates^"C"); - ]; - add_gen_actions "Template" templates_actions Coq_commands.commands; - GAction.add_actions queries_actions [ - GAction.add_action "Queries" ~label:"_Queries"; - query_shortcut "SearchAbout" (Some "F2"); - query_shortcut "Check" (Some "F3"); - query_shortcut "Print" (Some "F4"); - query_shortcut "About" (Some "F5"); - query_shortcut "Locate" None; - query_shortcut "Print Assumptions" None; - query_shortcut "Whelp Locate" None; - ]; - GAction.add_actions tools_actions [ - GAction.add_action "Tools" ~label:"_Tools"; - GAction.add_action "Comment" ~label:"_Comment" ~callback:comment_f ~accel:"<CTRL>D"; - GAction.add_action "Uncomment" ~label:"_Uncomment" ~callback:uncomment_f ~accel:"<CTRL><SHIFT>D"; - ]; - GAction.add_actions compile_actions [ - GAction.add_action "Compile" ~label:"_Compile"; - GAction.add_action "Compile buffer" ~label:"_Compile buffer" ~callback:compile_f; - GAction.add_action "Make" ~label:"_Make" ~callback:make_f ~accel:"F6"; - GAction.add_action "Next error" ~label:"_Next error" ~callback:next_error - ~accel:"F7"; - GAction.add_action "Make makefile" ~label:"Make makefile" ~callback:coq_makefile_f; - ]; - GAction.add_actions windows_actions [ - GAction.add_action "Windows" ~label:"_Windows"; - GAction.add_action "Detach View" ~label:"Detach _View" - ~callback:detach_view - ]; - GAction.add_actions help_actions [ - GAction.add_action "Help" ~label:"_Help"; - GAction.add_action "Browse Coq Manual" ~label:"Browse Coq _Manual" - ~callback:(fun _ -> - let av = session_notebook#current_term.analyzed_view in - browse av#insert_message (doc_url ())); - GAction.add_action "Browse Coq Library" ~label:"Browse Coq _Library" - ~callback:(fun _ -> - let av = session_notebook#current_term.analyzed_view in - browse av#insert_message current.library_url); - GAction.add_action "Help for keyword" ~label:"Help for _keyword" - ~callback:(fun _ -> let av = session_notebook#current_term.analyzed_view in - av#help_for_keyword ()) ~stock:`HELP; - GAction.add_action "About Coq" ~label:"_About" ~stock:`ABOUT; - ]; - Coqide_ui.init (); - Coqide_ui.ui_m#insert_action_group file_actions 0; - Coqide_ui.ui_m#insert_action_group export_actions 0; - Coqide_ui.ui_m#insert_action_group edit_actions 0; - Coqide_ui.ui_m#insert_action_group view_actions 0; - Coqide_ui.ui_m#insert_action_group navigation_actions 0; - Coqide_ui.ui_m#insert_action_group tactics_actions 0; - Coqide_ui.ui_m#insert_action_group templates_actions 0; - Coqide_ui.ui_m#insert_action_group tools_actions 0; - Coqide_ui.ui_m#insert_action_group queries_actions 0; - Coqide_ui.ui_m#insert_action_group compile_actions 0; - Coqide_ui.ui_m#insert_action_group windows_actions 0; - Coqide_ui.ui_m#insert_action_group help_actions 0; - w#add_accel_group Coqide_ui.ui_m#get_accel_group ; - GtkMain.Rc.parse_string "gtk-can-change-accels = 1"; - if Coq_config.gtk_platform <> `QUARTZ - then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar"); - let tbar = GtkButton.Toolbar.cast ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget) - in let () = GtkButton.Toolbar.set ~orientation:`HORIZONTAL ~style:`ICONS - ~tooltips:true tbar in - let toolbar = new GObj.widget tbar in - vbox#pack toolbar; - - ignore (w#event#connect#delete ~callback:(fun _ -> quit_f (); true)); + item "Previous" ~label:"_Previous" ~stock:`GO_BACK + ~callback:Nav.previous_occ + ~tooltip:"Previous occurence" + ~accel:(current.modifier_for_navigation^"less"); + item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ + ~tooltip:"Next occurence" + ~accel:(current.modifier_for_navigation^"greater"); + ]; + + let tacitem s sc = + item s ~label:("_"^s) + ~accel:(current.modifier_for_tactics^sc) + ~callback:(tactic_wizard_callback [s]) + in + menu tactics_menu [ + item "Try Tactics" ~label:"_Try Tactics"; + item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO + ~tooltip:"Proof Wizard" ~accel:(current.modifier_for_tactics^"dollar") + ~callback:(tactic_wizard_callback current.automatic_tactics); + tacitem "auto" "a"; + tacitem "auto with *" "asterisk"; + tacitem "eauto" "e"; + tacitem "eauto with *" "ampersand"; + tacitem "intuition" "i"; + tacitem "omega" "o"; + tacitem "simpl" "s"; + tacitem "tauto" "p"; + tacitem "trivial" "v"; + ]; + alpha_items tactics_menu "Tactic" Coq_commands.tactics; + + menu templates_menu [ + item "Templates" ~label:"Te_mplates"; + template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "L"); + 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:(current.modifier_for_templates^"C") + ~callback:match_callback + ]; + alpha_items templates_menu "Template" Coq_commands.commands; + + let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in + menu queries_menu [ + item "Queries" ~label:"_Queries"; + qitem "SearchAbout" (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; + ]; + + menu tools_menu [ + item "Tools" ~label:"_Tools"; + item "Comment" ~label:"_Comment" ~accel:"<CTRL>D" + ~callback:MiscMenu.comment; + item "Uncomment" ~label:"_Uncomment" ~accel:"<CTRL><SHIFT>D" + ~callback:MiscMenu.uncomment; + ]; + + menu compile_menu [ + item "Compile" ~label:"_Compile"; + item "Compile buffer" ~label:"_Compile buffer" ~callback:External.compile; + item "Make" ~label:"_Make" ~accel:"F6" + ~callback:External.make; + item "Next error" ~label:"_Next error" ~accel:"F7" + ~callback:External.next_error; + item "Make makefile" ~label:"Make makefile" ~callback:External.coq_makefile; + ]; + + menu windows_menu [ + item "Windows" ~label:"_Windows"; + item "Detach View" ~label:"Detach _View" ~callback:MiscMenu.detach_view + ]; + + menu help_menu [ + item "Help" ~label:"_Help"; + item "Browse Coq Manual" ~label:"Browse Coq _Manual" + ~callback:(fun _ -> + let av = session_notebook#current_term.analyzed_view in + browse av#insert_message (doc_url ())); + item "Browse Coq Library" ~label:"Browse Coq _Library" + ~callback:(fun _ -> + let av = session_notebook#current_term.analyzed_view in + browse av#insert_message current.library_url); + item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP + ~callback:(fun _ -> + let av = session_notebook#current_term.analyzed_view in + av#help_for_keyword ()); + item "About Coq" ~label:"_About" ~stock:`ABOUT + ~callback:MiscMenu.about + ]; + + Coqide_ui.init (); + Coqide_ui.ui_m#insert_action_group file_menu 0; + Coqide_ui.ui_m#insert_action_group export_menu 0; + Coqide_ui.ui_m#insert_action_group edit_menu 0; + Coqide_ui.ui_m#insert_action_group view_menu 0; + Coqide_ui.ui_m#insert_action_group navigation_menu 0; + Coqide_ui.ui_m#insert_action_group tactics_menu 0; + Coqide_ui.ui_m#insert_action_group templates_menu 0; + Coqide_ui.ui_m#insert_action_group tools_menu 0; + Coqide_ui.ui_m#insert_action_group queries_menu 0; + Coqide_ui.ui_m#insert_action_group compile_menu 0; + Coqide_ui.ui_m#insert_action_group windows_menu 0; + Coqide_ui.ui_m#insert_action_group help_menu 0; + w#add_accel_group Coqide_ui.ui_m#get_accel_group ; + GtkMain.Rc.parse_string "gtk-can-change-accels = 1"; + if Coq_config.gtk_platform <> `QUARTZ + then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar"); + + (* Toolbar *) + let tbar = GtkButton.Toolbar.cast + ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget) + in + let () = GtkButton.Toolbar.set + ~orientation:`HORIZONTAL ~style:`ICONS ~tooltips:true tbar + in + let toolbar = new GObj.widget tbar in + let () = vbox#pack toolbar in (* Reset on tab switch *) - ignore (session_notebook#connect#switch_page - (fun _ -> if current.reset_on_tab_switch then force_reset_initial ())); - (* The vertical Separator between Scripts and Goals *) - vbox#pack ~expand:true session_notebook#coerce; - update_notebook_pos (); + let _ = session_notebook#connect#switch_page + (fun _ -> if current.reset_on_tab_switch then force_reset_initial ()) + in + + (* Vertical Separator between Scripts and Goals *) + let () = vbox#pack ~expand:true session_notebook#coerce in + let () = update_notebook_pos () in let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in - lower_hbox#pack ~expand:true status#coerce; - push_info "Ready"; + let () = lower_hbox#pack ~expand:true status#coerce in + let () = push_info "Ready" in + (* Location display *) let l = GMisc.label ~text:"Line: 1 Char: 1" - ~packing:lower_hbox#pack () in - l#coerce#misc#set_name "location"; - set_location := l#set_text; + ~packing:lower_hbox#pack () + in + let () = l#coerce#misc#set_name "location" in + let () = set_location := l#set_text in + (* Progress Bar *) - lower_hbox#pack pbar#coerce; - pbar#set_text "CoqIde started"; + let pbar = GRange.progress_bar ~pulse_step:0.2 () in + let () = lower_hbox#pack pbar#coerce in + let () = pbar#set_text "CoqIde started" in + let _ = Glib.Timeout.add ~ms:300 ~callback:(fun () -> + let curr_coq = session_notebook#current_term.toplvl in + if Coq.is_computing curr_coq then pbar#pulse (); + true) + in (* Initializing hooks *) - - refresh_toolbar_hook := - (fun () -> if current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ()); - refresh_style_hook := - (fun () -> - let style = style_manager#style_scheme current.source_style in - let iter_page p = p.script#source_buffer#set_style_scheme style in - List.iter iter_page session_notebook#pages; - ); - refresh_editor_hook := - (fun () -> - let wrap_mode = if current.dynamic_word_wrap then `WORD else `NONE in - let show_spaces = - if current.show_spaces then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *) - else 0 - in - let fd = current.text_font in - let clr = Tags.color_of_string current.background_color in - - let iter_page p = - (* Editor settings *) - p.script#set_wrap_mode wrap_mode; - p.script#set_show_line_numbers current.show_line_number; - p.script#set_auto_indent current.auto_indent; - p.script#set_highlight_current_line current.highlight_current_line; - - (* Hack to handle missing binding in lablgtk *) - let conv = { Gobject.name = "draw-spaces"; Gobject.conv = Gobject.Data.int } in - Gobject.set conv p.script#as_widget show_spaces; - - p.script#set_show_right_margin current.show_right_margin; - p.script#set_insert_spaces_instead_of_tabs current.spaces_instead_of_tabs; - p.script#set_tab_width current.tab_length; - p.script#set_auto_complete current.auto_complete; - - (* Fonts *) - p.script#misc#modify_font fd; - p.proof_view#misc#modify_font fd; - p.message_view#misc#modify_font fd; - p.command#refresh_font (); - - (* Colors *) - p.script#misc#modify_base [`NORMAL, `COLOR clr]; - p.proof_view#misc#modify_base [`NORMAL, `COLOR clr]; - p.message_view#misc#modify_base [`NORMAL, `COLOR clr]; - p.command#refresh_color () - - in - List.iter iter_page session_notebook#pages; - ); - resize_window_hook := (fun () -> - w#resize - ~width:current.window_width - ~height:current.window_height); - refresh_tabs_hook := update_notebook_pos; - - let initial_about () = - let initial_string = - "Welcome to CoqIDE, an Integrated Development Environment for Coq" - in - let coq_version = Coq.short_version () in - let version_info = - if Glib.Utf8.validate coq_version then - "\nYou are running " ^ coq_version - else "" - in - let msg = initial_string ^ version_info in - session_notebook#current_term.message_view#push Interface.Notice msg + let refresh_toolbar () = + if current.show_toolbar + then toolbar#misc#show () + else toolbar#misc#hide () in - - let about () = - let dialog = GWindow.about_dialog () in - let _ = dialog#connect#response (fun _ -> dialog#destroy ()) in - let _ = - try - let image = Filename.concat (List.find - (fun x -> Sys.file_exists (Filename.concat x "coq.png")) - (Minilib.coqide_data_dirs ())) "coq.png" in - let startup_image = GdkPixbuf.from_file image in - dialog#set_logo startup_image - with _ -> () - in - let copyright = "Coq is developed by the Coq Development Team\n\ - (INRIA - CNRS - LIX - LRI - PPS)" - in - let authors = [ - "Benjamin Monate"; - "Jean-Christophe Filliâtre"; - "Pierre Letouzey"; - "Claude Marché"; - "Bruno Barras"; - "Pierre Corbineau"; - "Julien Narboux"; - "Hugo Herbelin"; - ] in - dialog#set_name "CoqIDE"; - dialog#set_comments "The Coq Integrated Development Environment"; - dialog#set_website Coq_config.wwwcoq; - dialog#set_version Coq_config.version; - dialog#set_copyright copyright; - dialog#set_authors authors; - dialog#show () + let refresh_style () = + let style = style_manager#style_scheme current.source_style in + let iter_page p = p.script#source_buffer#set_style_scheme style in + List.iter iter_page session_notebook#pages in - (* Remove default pango menu for textviews *) - w#show (); - ignore ((help_actions#get_action "About Coq")#connect#activate about); - -(* Begin Color configuration *) + let resize_window () = + w#resize ~width:current.window_width ~height:current.window_height + in + refresh_toolbar_hook := refresh_toolbar; + refresh_style_hook := refresh_style; + refresh_editor_hook := refresh_editor_prefs; + resize_window_hook := resize_window; + refresh_tabs_hook := update_notebook_pos; + (* Color configuration *) Tags.set_processing_color (Tags.color_of_string current.processing_color); Tags.set_processed_color (Tags.color_of_string current.processed_color); -(* End of color configuration *) + (* Showtime ! *) + w#show () - if List.length files >=1 then - begin - List.iter (fun f -> - if Sys.file_exists f then do_load f else - let f = if Filename.check_suffix f ".v" then f else f^".v" in - load_file (fun s -> print_endline s; exit 1) f) - files; - session_notebook#goto_page 0; - end - else - begin +let main files = + build_ui (); + let do_file f = + if Sys.file_exists f then FileAux.do_load f + else + let f = if Filename.check_suffix f ".v" then f else f^".v" in + FileAux.load_file (fun s -> warning s; exit 1) f + in + begin match files with + |[] -> let session = create_session None in let index = session_notebook#append_term session in !refresh_editor_hook (); session_notebook#goto_page index; - end; - initial_about (); + |_ -> + List.iter do_file files; + session_notebook#goto_page 0; + end; + MiscMenu.initial_about (); !refresh_toolbar_hook (); !refresh_editor_hook (); - session_notebook#current_term.script#misc#grab_focus ();; + session_notebook#current_term.script#misc#grab_focus (); + Minilib.log "End of Coqide.main" (* This function check every half of second if GeoProof has send something on his private clipboard *) @@ -2224,22 +2171,24 @@ let rec check_for_geoproof_input () = let read_coqide_args argv = let rec filter_coqtop coqtop project_files out = function - | "-coqtop" :: prog :: args -> + |"-coqtop" :: prog :: args -> if coqtop = None then filter_coqtop (Some prog) project_files out args - else - (output_string stderr "Error: multiple -coqtop options"; exit 1) - | "-f" :: file :: args -> - filter_coqtop coqtop - ((CUnix.canonical_path_name (Filename.dirname file), - Project_file.read_project_file file) :: project_files) out args - | "-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 - | "-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1 - | "-debug"::args -> Minilib.debug := true; + else (output_string stderr "Error: multiple -coqtop options"; exit 1) + |"-f" :: file :: args -> + let d = CUnix.canonical_path_name (Filename.dirname file) in + let p = Project_file.read_project_file file in + filter_coqtop coqtop ((d,p) :: project_files) out args + |"-f" :: [] -> + output_string stderr "Error: missing project file name"; exit 1 + |"-coqtop" :: [] -> + output_string stderr "Error: missing argument after -coqtop"; exit 1 + |"-debug"::args -> + Minilib.debug := true; filter_coqtop coqtop project_files ("-debug"::out) args - | arg::args -> filter_coqtop coqtop project_files (arg::out) args - | [] -> (coqtop,List.rev project_files,List.rev out) + |arg::args -> filter_coqtop coqtop project_files (arg::out) args + |[] -> (coqtop,List.rev project_files,List.rev out) in let coqtop,project_files,argv = filter_coqtop None [] [] argv in - Ideutils.custom_coqtop := coqtop; - custom_project_files := project_files; + Ideutils.custom_coqtop := coqtop; + custom_project_files := project_files; argv diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 949a8774d..3630de319 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -27,8 +27,6 @@ let flash_info = let set_location = ref (function s -> failwith "not ready") -let pbar = GRange.progress_bar ~pulse_step:0.2 () - let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT let byte_offset_to_char_offset s byte_offset = @@ -52,29 +50,24 @@ let byte_offset_to_char_offset s byte_offset = let print_id id = Minilib.log ("GOT sig id :"^(string_of_int (Obj.magic id))) - let do_convert s = - Utf8_convert.f - (if Glib.Utf8.validate s then begin - Minilib.log "Input is UTF-8";s - end else - let from_loc () = - let _,char_set = Glib.Convert.get_charset () in - flash_info - ("Converting from locale ("^char_set^")"); - Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s - in - let from_manual enc = - flash_info - ("Converting from "^ enc); - Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:enc - in - match current.encoding with - |Preferences.Eutf8 | Preferences.Elocale -> from_loc () - |Emanual enc -> - try - from_manual enc - with _ -> from_loc ()) + let from_loc () = + let _,char_set = Glib.Convert.get_charset () in + flash_info ("Converting from locale ("^char_set^")"); + Glib.Convert.convert_with_fallback + ~to_codeset:"UTF-8" ~from_codeset:char_set s + in + let from_manual enc = + flash_info ("Converting from "^ enc); + Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:enc + in + let s = + if Glib.Utf8.validate s then (Minilib.log "Input is UTF-8"; s) + else match current.encoding with + |Preferences.Eutf8 | Preferences.Elocale -> from_loc () + |Emanual enc -> try from_manual enc with _ -> from_loc () + in + Utf8_convert.f s let try_convert s = try @@ -85,28 +78,31 @@ Please choose a correct encoding in the preference panel.*)";; let try_export file_name s = - try let s = + let s = try match current.encoding with - |Eutf8 -> begin - (Minilib.log "UTF-8 is enforced" ;s) - end - |Elocale -> begin + |Eutf8 -> Minilib.log "UTF-8 is enforced" ; s + |Elocale -> let is_unicode,char_set = Glib.Convert.get_charset () in if is_unicode then - (Minilib.log "Locale is UTF-8" ;s) + (Minilib.log "Locale is UTF-8" ; s) else (Minilib.log ("Locale is "^char_set); - Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s) - end + Glib.Convert.convert_with_fallback + ~from_codeset:"UTF-8" ~to_codeset:char_set s) |Emanual enc -> (Minilib.log ("Manual charset is "^ enc); - Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:enc s) - with e -> (Minilib.log ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s) + Glib.Convert.convert_with_fallback + ~from_codeset:"UTF-8" ~to_codeset:enc s) + with e -> + let str = Printexc.to_string e in + Minilib.log ("Error ("^str^") in transcoding: falling back to UTF-8"); + s in - let oc = open_out file_name in - output_string oc s; - close_out oc; - true + try + let oc = open_out file_name in + output_string oc s; + close_out oc; + true with e -> Minilib.log (Printexc.to_string e);false let my_stat f = try Some (Unix.stat f) with _ -> None @@ -121,19 +117,6 @@ let disconnect_auto_save_timer () = match !auto_save_timer with | None -> () | Some id -> GMain.Timeout.remove id; auto_save_timer := None -let highlight_timer = ref None -let set_highlight_timer f = - match !highlight_timer with - | None -> - revert_timer := - Some (GMain.Timeout.add ~ms:2000 - ~callback:(fun () -> f (); highlight_timer := None; true)) - | Some id -> - GMain.Timeout.remove id; - revert_timer := - Some (GMain.Timeout.add ~ms:2000 - ~callback:(fun () -> f (); highlight_timer := None; true)) - let last_dir = ref "" let filter_all_files () = GFile.filter @@ -144,55 +127,62 @@ let filter_coq_files () = GFile.filter ~name:"Coq source code" ~patterns:[ "*.v"] () -let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () = +let select_file_for_open ~title () = let file = ref None in - let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title () 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 ()); - file_chooser#set_default_response `OPEN; - ignore (file_chooser#set_current_folder !dir); - begin match file_chooser#run () with - | `OPEN -> - begin - file := file_chooser#filename; - match !file with - None -> () - | Some s -> dir := Filename.dirname s; - end - | `DELETE_EVENT | `CANCEL -> () - end ; - file_chooser#destroy (); - !file - - -let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () = + let file_chooser = + GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title () + 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 ()); + file_chooser#set_default_response `OPEN; + ignore (file_chooser#set_current_folder !last_dir); + begin match file_chooser#run () with + | `OPEN -> + begin + file := file_chooser#filename; + match !file with + | None -> () + | Some s -> last_dir := Filename.dirname s; + end + | `DELETE_EVENT | `CANCEL -> () + end ; + file_chooser#destroy (); + !file + +let select_file_for_save ~title ?filename () = let file = ref None in - let file_chooser = GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title () in - file_chooser#add_button_stock `CANCEL `CANCEL ; - 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_default_response `SAVE; - ignore (file_chooser#set_current_folder !dir); - ignore (file_chooser#set_current_name filename); - - begin match file_chooser#run () with - | `SAVE -> - begin - file := file_chooser#filename; - match !file with - None -> () - | Some s -> dir := Filename.dirname s; - end - | `DELETE_EVENT | `CANCEL -> () - end ; - file_chooser#destroy (); - !file + let file_chooser = + GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title () + in + file_chooser#add_button_stock `CANCEL `CANCEL ; + 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_default_response `SAVE; + let dir,filename = match filename with + |None -> !last_dir, "" + |Some f -> Filename.dirname f, Filename.basename f + in + ignore (file_chooser#set_current_folder dir); + ignore (file_chooser#set_current_name filename); + begin match file_chooser#run () with + | `SAVE -> + begin + file := file_chooser#filename; + match !file with + None -> () + | Some s -> last_dir := Filename.dirname s; + end + | `DELETE_EVENT | `CANCEL -> () + end ; + file_chooser#destroy (); + !file let find_tag_start (tag :GText.tag) (it:GText.iter) = let it = it#copy in @@ -257,7 +247,8 @@ let coqtop_path () = let prog = String.copy Sys.executable_name in try let pos = String.length prog - 6 in - let i = Str.search_backward (Str.regexp_string "coqide") prog pos in + let i = Str.search_backward (Str.regexp_string "coqide") prog pos + in String.blit "coqtop" 0 prog i 6; prog with Not_found -> "coqtop" @@ -285,7 +276,9 @@ let browse f url = *) let doc_url () = if current.doc_url = use_default_doc_url || current.doc_url = "" then - let addr = List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";"index.html"] in + let addr = List.fold_left Filename.concat (Coq_config.docdir) + ["html";"refman";"index.html"] + in if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman else current.doc_url diff --git a/ide/ideutils.mli b/ide/ideutils.mli index dd4136dc8..af45fa21b 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -30,13 +30,9 @@ val print_id : 'a -> unit val revert_timer : GMain.Timeout.id option ref val auto_save_timer : GMain.Timeout.id option ref -val select_file_for_open : - title:string -> - ?dir:string ref -> ?filename:string -> unit -> string option +val select_file_for_open : title:string -> unit -> string option val select_file_for_save : - title:string -> - ?dir:string ref -> ?filename:string -> unit -> string option -val set_highlight_timer : (unit -> 'a) -> unit + title:string -> ?filename:string -> unit -> string option val try_convert : string -> string val try_export : string -> string -> bool val stock_to_widget : ?size:Gtk.Tags.icon_size -> GtkStock.id -> GObj.widget @@ -59,8 +55,6 @@ val flash_info : ?delay:int -> string -> unit val set_location : (string -> unit) ref -val pbar : GRange.progress_bar - (* In win32, when a command-line is to be executed via cmd.exe (i.e. Sys.command, Unix.open_process, ...), it cannot contain several quoted "..." zones otherwise some quotes are lost. Solution: we re-quote |