Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 100 insertions, 80 deletions

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
-	      
+