From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- ide/ideutils.ml | 180 +++++++++++++++++++++++++++++++------------------------- 1 file changed, 100 insertions(+), 80 deletions(-) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d9b5e572..14e80389 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml 11749 2009-01-05 14:01:04Z notin $ *) +(* $Id$ *) open Preferences @@ -15,15 +15,21 @@ exception Forbidden (* status bar and locations *) -let status = ref None -let push_info = ref (function s -> failwith "not ready") -let pop_info = ref (function s -> failwith "not ready") -let flash_info = ref (fun ?delay s -> failwith "not ready") +let status = GMisc.statusbar () + +let push_info,pop_info = + let status_context = status#new_context "Messages" in + (fun s -> ignore (status_context#push s)),status_context#pop + +let flash_info = + let flash_context = status#new_context "Flash" in + (fun ?(delay=5000) s -> flash_context#flash ~delay s) -let set_location = ref (function s -> failwith "not ready") -let pulse = ref (function () -> failwith "not ready") +let set_location = ref (function s -> failwith "not ready") + +let pbar = GRange.progress_bar ~pulse_step:0.2 () let debug = Flags.debug @@ -35,12 +41,12 @@ let prerr_string s = let lib_ide_file f = let coqlib = Envars.coqlib () in Filename.concat (Filename.concat coqlib "ide") f - + let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0 -let byte_offset_to_char_offset s byte_offset = +let byte_offset_to_char_offset s byte_offset = if (byte_offset < String.length s) then begin let count_delta = ref 0 in for i = 0 to byte_offset do @@ -62,19 +68,19 @@ let print_id id = prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id))) -let do_convert s = +let do_convert s = Utf8_convert.f (if Glib.Utf8.validate s then begin prerr_endline "Input is UTF-8";s end else - let from_loc () = + let from_loc () = let _,char_set = Glib.Convert.get_charset () in - !flash_info + 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 () = - !flash_info + let from_manual () = + flash_info ("Converting from "^ !current.encoding_manual); Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:!current.encoding_manual in @@ -84,30 +90,30 @@ let do_convert s = with _ -> from_manual () end else begin try - from_manual () + from_manual () with _ -> from_loc () end) -let try_convert s = +let try_convert s = try do_convert s - with _ -> + with _ -> "(* Fatal error: wrong encoding in input. Please choose a correct encoding in the preference panel.*)";; -let try_export file_name s = - try let s = +let try_export file_name s = + try let s = try if !current.encoding_use_utf8 then begin (prerr_endline "UTF-8 is enforced" ;s) end else if !current.encoding_use_locale then begin let is_unicode,char_set = Glib.Convert.get_charset () in - if is_unicode then - (prerr_endline "Locale is UTF-8" ;s) + if is_unicode then + (prerr_endline "Locale is UTF-8" ;s) else (prerr_endline ("Locale is "^char_set); Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s) - end else + end else (prerr_endline ("Manual charset is "^ !current.encoding_manual); Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:!current.encoding_manual s) with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s) @@ -131,16 +137,16 @@ let disconnect_auto_save_timer () = match !auto_save_timer with | 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 +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 -> + | Some id -> GMain.Timeout.remove id; - revert_timer := - Some (GMain.Timeout.add ~ms:2000 + revert_timer := + Some (GMain.Timeout.add ~ms:2000 ~callback:(fun () -> f (); highlight_timer := None; true)) @@ -150,31 +156,31 @@ let init_stdout,read_stdout,clear_stdout = let out_ft = Format.formatter_of_buffer out_buff in let deep_out_ft = Format.formatter_of_buffer out_buff in let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in - (fun () -> + (fun () -> Pp_control.std_ft := out_ft; Pp_control.err_ft := out_ft; Pp_control.deep_ft := deep_out_ft; ), - (fun () -> Format.pp_print_flush out_ft (); + (fun () -> Format.pp_print_flush out_ft (); let r = Buffer.contents out_buff in prerr_endline "Output from Coq is: "; prerr_endline r; Buffer.clear out_buff; r), - (fun () -> + (fun () -> Format.pp_print_flush out_ft (); Buffer.clear out_buff) let last_dir = ref "" -let filter_all_files () = GFile.filter - ~name:"All" - ~patterns:["*"] () - -let filter_coq_files () = GFile.filter - ~name:"Coq source code" +let filter_all_files () = GFile.filter + ~name:"All" + ~patterns:["*"] () + +let filter_coq_files () = GFile.filter + ~name:"Coq source code" ~patterns:[ "*.v"] () let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () = - let file = ref None in + 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 ; @@ -183,8 +189,8 @@ let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () = file_chooser#set_default_response `OPEN; ignore (file_chooser#set_current_folder !dir); begin match file_chooser#run () with - | `OPEN -> - begin + | `OPEN -> + begin file := file_chooser#filename; match !file with None -> () @@ -192,27 +198,27 @@ let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () = end | `DELETE_EVENT | `CANCEL -> () end ; - file_chooser#destroy (); + file_chooser#destroy (); !file let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () = - let file = ref None in + 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 + (* 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 + | `SAVE -> + begin file := file_chooser#filename; match !file with None -> () @@ -220,7 +226,7 @@ let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () = end | `DELETE_EVENT | `CANCEL -> () end ; - file_chooser#destroy (); + file_chooser#destroy (); !file let find_tag_start (tag :GText.tag) (it:GText.iter) = @@ -237,7 +243,7 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) = () done; it -let find_tag_limits (tag :GText.tag) (it:GText.iter) = +let find_tag_limits (tag :GText.tag) (it:GText.iter) = (find_tag_start tag it , find_tag_stop tag it) (* explanations: Win32 threads won't work if events are produced @@ -245,16 +251,16 @@ let find_tag_limits (tag :GText.tag) (it:GText.iter) = case we must use GtkThread.async to push a callback in the main thread. Beware that the synchronus version may produce deadlocks. *) -let async = +let async = if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x) -let sync = +let sync = if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x) let mutex text f = let m = Mutex.create() in fun x -> if Mutex.try_lock m - then + then (try prerr_endline ("Got lock on "^text); f x; @@ -269,8 +275,8 @@ let mutex text f = ("Discarded call for "^text^": computations ongoing") -let stock_to_widget ?(size=`DIALOG) s = - let img = GMisc.image () +let stock_to_widget ?(size=`DIALOG) s = + let img = GMisc.image () in img#set_stock s; img#coerce @@ -290,12 +296,12 @@ let run_command f c = let ne = ref 0 in while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0 do - let r = try_convert (String.sub buff 0 !n) in + let r = try_convert (String.sub buff 0 !n) in f r; Buffer.add_string result r; - let r = try_convert (String.sub buffe 0 !ne) in + let r = try_convert (String.sub buffe 0 !ne) in f r; - Buffer.add_string result r + Buffer.add_string result r done; (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) @@ -306,46 +312,60 @@ let browse f url = f ("Could not execute\n\""^com^ "\"\ncheck your preferences for setting a valid browser command\n") +let doc_url () = + if !current.doc_url = use_default_doc_url || !current.doc_url = "" then + if Sys.file_exists + (String.sub Coq_config.localwwwrefman 7 + (String.length Coq_config.localwwwrefman - 7)) + then + Coq_config.localwwwrefman + else + Coq_config.wwwrefman + else !current.doc_url + let url_for_keyword = let ht = Hashtbl.create 97 in + lazy ( begin try - let cin = open_in (lib_ide_file "index_urls.txt") in + let cin = + try open_in (lib_ide_file "index_urls.txt") + with _ -> + let doc_url = doc_url () in + let n = String.length doc_url in + if n > 8 && String.sub doc_url 0 7 = "file://" then + open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt") + else + raise Exit + in try while true do let s = input_line cin in - try + try let i = String.index s ',' in let k = String.sub s 0 i in let u = String.sub s (i + 1) (String.length s - i - 1) in Hashtbl.add ht k u with _ -> - () + Printf.eprintf "Warning: Cannot parse documentation index file.\n"; + flush stderr done with End_of_file -> close_in cin with _ -> - () + Printf.eprintf "Warning: Cannot find documentation index file.\n"; + flush stderr end; - (Hashtbl.find ht : string -> string) + Hashtbl.find ht : string -> string) -let browse_keyword f text = - try let u = url_for_keyword text in browse f (!current.doc_url ^ u) - with Not_found -> f ("No documentation found for "^text) - - -let underscore = Glib.Utf8.to_unichar "_" (ref 0) - -let arobase = Glib.Utf8.to_unichar "@" (ref 0) -let prime = Glib.Utf8.to_unichar "'" (ref 0) -let bn = Glib.Utf8.to_unichar "\n" (ref 0) -let space = Glib.Utf8.to_unichar " " (ref 0) -let tab = Glib.Utf8.to_unichar "\t" (ref 0) +let browse_keyword f text = + try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u) + with Not_found -> f ("No documentation found for \""^text^"\".\n") (* checks if two file names refer to the same (existing) file by - comparing their device and inode. + comparing their device and inode. It seems that under Windows, inode is always 0, so we cannot - accurately check if + accurately check if *) (* Optimised for partial application (in case many candidates must be @@ -357,7 +377,7 @@ let same_file f1 = try let s2 = Unix.stat f2 in s1.Unix.st_dev = s2.Unix.st_dev && - if Sys.os_type = "Win32" then f1 = f2 + if Sys.os_type = "Win32" then f1 = f2 else s1.Unix.st_ino = s2.Unix.st_ino with Unix.Unix_error _ -> false) @@ -365,7 +385,7 @@ let same_file f1 = Unix.Unix_error _ -> (fun _ -> false) let absolute_filename f = - if Filename.is_relative f then + if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f - + -- cgit v1.2.3