1 files changed, 102 insertions, 140 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a6be77f2..164c837a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ideutils.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 
 open Preferences
 
@@ -18,11 +16,11 @@ exception Forbidden
 let status = GMisc.statusbar ()
 
 let push_info,pop_info =
-  let status_context = status#new_context "Messages" in
+  let status_context = status#new_context ~name:"Messages" in
     (fun s -> ignore (status_context#push s)),status_context#pop
 
 let flash_info =
-  let flash_context = status#new_context "Flash" in
+  let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
 
@@ -31,20 +29,10 @@ let set_location = ref  (function s -> failwith "not ready")
 
 let pbar = GRange.progress_bar ~pulse_step:0.2 ()
 
-(* On a Win32 application with no console, writing to stderr raise
-   a Sys_error "bad file descriptor" *)
-let safe_prerr_endline msg = try prerr_endline msg with _ -> ()
-
-let debug = Flags.debug
+let debug = ref (false)
 
 let prerr_endline s =
-  if !debug then try (prerr_endline s;flush stderr) with _ -> ()
-let prerr_string s =
-  if !debug then try (prerr_string s;flush stderr) with _ -> ()
-
-let lib_ide_file f =
-  let coqlib = Envars.coqlib () in
-  Filename.concat (Filename.concat coqlib "ide") f
+  if !debug then try prerr_endline s;flush stderr with _ -> ()
 
 let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
 
@@ -75,51 +63,51 @@ let print_id id =
 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 _,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 () =
-	 flash_info
-	   ("Converting from "^ !current.encoding_manual);
-	 Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:!current.encoding_manual
-       in
-       if !current.encoding_use_utf8 || !current.encoding_use_locale then begin
-	 try
-	   from_loc ()
-	 with _ -> from_manual ()
-       end else begin
-	 try
-	   from_manual ()
-	 with _ -> from_loc ()
-       end)
+      prerr_endline "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 try_convert s =
   try
     do_convert s
   with _ ->
-    "(* Fatal error: wrong encoding in input.
+    "(* Fatal error: wrong encoding in input. \
 Please choose a correct encoding in the preference panel.*)";;
 
 
 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)
-      else
-	(prerr_endline ("Locale is "^char_set);
-	 Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s)
-    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)
+    try match !current.encoding with
+      |Eutf8 -> begin
+	(prerr_endline "UTF-8 is enforced" ;s)
+      end
+      |Elocale -> begin
+	let is_unicode,char_set = Glib.Convert.get_charset () in
+	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
+      |Emanual enc ->
+	(prerr_endline ("Manual charset is "^ enc);
+       Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:enc s)
     with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s)
   in
   let oc = open_out file_name in
@@ -153,26 +141,6 @@ let set_highlight_timer f =
 	Some (GMain.Timeout.add ~ms:2000
 		~callback:(fun () -> f (); highlight_timer := None; true))
 
-
-(* Get back the standard coq out channels *)
-let init_stdout,read_stdout,clear_stdout =
-  let out_buff = Buffer.create 100 in
-  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 () ->
-    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 ();
-     let r = Buffer.contents out_buff in
-     prerr_endline "Output from Coq is: "; prerr_endline r;
-     Buffer.clear out_buff; r),
-  (fun () ->
-     Format.pp_print_flush out_ft (); Buffer.clear out_buff)
-
-
 let last_dir = ref ""
 
 let filter_all_files () = GFile.filter
@@ -284,14 +252,40 @@ let stock_to_widget ?(size=`DIALOG) s =
   in img#set_stock s;
   img#coerce
 
+let custom_coqtop = ref None
+
+let coqtop_path () =
+  let file = match !custom_coqtop with
+    | Some s -> s
+    | None ->
+      match !current.cmd_coqtop with
+	| Some s -> s
+	| None ->
+	  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
+	    String.blit "coqtop" 0 prog i 6;
+	    prog
+	  with Not_found -> "coqtop"
+  in file
+
 let rec print_list print fmt = function
   | [] -> ()
   | [x] -> print fmt x
   | x :: r -> print fmt x; print_list print fmt r
 
+(* 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
+   everything. Reference: http://ss64.com/nt/cmd.html *)
+
+let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd
+
 (* TODO: allow to report output as soon as it comes (user-fiendlier
    for long commands like make...) *)
 let run_command f c =
+  let c = requote c in
   let result = Buffer.create 127 in
   let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
   let buff = String.make 127 ' ' in
@@ -310,86 +304,54 @@ let run_command f c =
   (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
 let browse f url =
-  let com = Flags.subst_command_placeholder !current.cmd_browse url in
-  let s = Sys.command com in
+  let com = Minilib.subst_command_placeholder !current.cmd_browse url in
+  let _ = Unix.open_process_out com in ()
+(* This beautiful message will wait for twt ...
   if s = 127 then
     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
+    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
 
 let url_for_keyword =
   let ht = Hashtbl.create 97 in
-  lazy (
-  begin try
-    let cin =
-      try open_in (lib_ide_file "index_urls.txt")
+    lazy (
+      begin try
+	let cin =
+	  try let index_urls = Filename.concat (List.find
+            (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt"))
+	    Minilib.xdg_config_dirs) "index_urls.txt" in
+	    open_in index_urls
+	  with Not_found ->
+	    let doc_url = doc_url () in
+	    let n = String.length doc_url in
+	      if n > 8 && String.sub doc_url 0 7 = "file://" then
+		open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt")
+	      else
+		raise Exit
+	in
+	  try while true do
+	    let s = input_line cin in
+	      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 _ ->
+		Minilib.safe_prerr_endline "Warning: Cannot parse documentation index file."
+	  done with End_of_file ->
+	    close_in cin
       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
-	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)
-
+	Minilib.safe_prerr_endline "Warning: Cannot find documentation index file."
+      end;
+      Hashtbl.find ht : string -> string)
 
 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.
-  It seems that under Windows, inode is always 0, so we cannot
-  accurately check if
-
-*)
-(* Optimised for partial application (in case many candidates must be
-   compared to f1). *)
-let same_file f1 =
-  try
-    let s1 = Unix.stat f1 in
-    (fun f2 ->
-      try
-        let s2 = Unix.stat f2 in
-        s1.Unix.st_dev = s2.Unix.st_dev &&
-          if Sys.os_type = "Win32" then f1 = f2
-          else s1.Unix.st_ino = s2.Unix.st_ino
-      with
-          Unix.Unix_error _ -> false)
-  with
-      Unix.Unix_error _ -> (fun _ -> false)
-
-let absolute_filename f =
-  if Filename.is_relative f then
-    Filename.concat (Sys.getcwd ()) f
-  else f
-
+let absolute_filename f = Minilib.correct_path f (Sys.getcwd ())