summaryrefslogtreecommitdiff
path: root/ide/ideutils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r--ide/ideutils.ml242
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 ())
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 22:31:00 +0000