1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: ideutils.ml 11749 2009-01-05 14:01:04Z notin $ *)
16
(* status bar and locations *)
19
let push_info = ref (function s -> failwith "not ready")
20
let pop_info = ref (function s -> failwith "not ready")
21
let flash_info = ref (fun ?delay s -> failwith "not ready")
23
let set_location = ref (function s -> failwith "not ready")
25
let pulse = ref (function () -> failwith "not ready")
28
let debug = Flags.debug
31
if !debug then (prerr_endline s;flush stderr)
33
if !debug then (prerr_string s;flush stderr)
36
let coqlib = Envars.coqlib () in
37
Filename.concat (Filename.concat coqlib "ide") f
39
let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
41
let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0
43
let byte_offset_to_char_offset s byte_offset =
44
if (byte_offset < String.length s) then begin
45
let count_delta = ref 0 in
46
for i = 0 to byte_offset do
47
let code = Char.code s.[i] in
48
if code >= 0x80 && code < 0xc0 then incr count_delta
50
byte_offset - !count_delta
53
let count_delta = ref 0 in
54
for i = 0 to String.length s - 1 do
55
let code = Char.code s.[i] in
56
if code >= 0x80 && code < 0xc0 then incr count_delta
58
byte_offset - !count_delta
62
prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id)))
67
(if Glib.Utf8.validate s then begin
68
prerr_endline "Input is UTF-8";s
71
let _,char_set = Glib.Convert.get_charset () in
73
("Converting from locale ("^char_set^")");
74
Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s
78
("Converting from "^ !current.encoding_manual);
79
Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:!current.encoding_manual
81
if !current.encoding_use_utf8 || !current.encoding_use_locale then begin
84
with _ -> from_manual ()
95
"(* Fatal error: wrong encoding in input.
96
Please choose a correct encoding in the preference panel.*)";;
99
let try_export file_name s =
101
try if !current.encoding_use_utf8 then begin
102
(prerr_endline "UTF-8 is enforced" ;s)
103
end else if !current.encoding_use_locale then begin
104
let is_unicode,char_set = Glib.Convert.get_charset () in
106
(prerr_endline "Locale is UTF-8" ;s)
108
(prerr_endline ("Locale is "^char_set);
109
Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s)
111
(prerr_endline ("Manual charset is "^ !current.encoding_manual);
112
Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:!current.encoding_manual s)
113
with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s)
115
let oc = open_out file_name in
119
with e -> prerr_endline (Printexc.to_string e);false
121
let my_stat f = try Some (Unix.stat f) with _ -> None
123
let revert_timer = ref None
124
let disconnect_revert_timer () = match !revert_timer with
126
| Some id -> GMain.Timeout.remove id; revert_timer := None
128
let auto_save_timer = ref None
129
let disconnect_auto_save_timer () = match !auto_save_timer with
131
| Some id -> GMain.Timeout.remove id; auto_save_timer := None
133
let highlight_timer = ref None
134
let set_highlight_timer f =
135
match !highlight_timer with
138
Some (GMain.Timeout.add ~ms:2000
139
~callback:(fun () -> f (); highlight_timer := None; true))
141
GMain.Timeout.remove id;
143
Some (GMain.Timeout.add ~ms:2000
144
~callback:(fun () -> f (); highlight_timer := None; true))
147
(* Get back the standard coq out channels *)
148
let init_stdout,read_stdout,clear_stdout =
149
let out_buff = Buffer.create 100 in
150
let out_ft = Format.formatter_of_buffer out_buff in
151
let deep_out_ft = Format.formatter_of_buffer out_buff in
152
let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in
154
Pp_control.std_ft := out_ft;
155
Pp_control.err_ft := out_ft;
156
Pp_control.deep_ft := deep_out_ft;
158
(fun () -> Format.pp_print_flush out_ft ();
159
let r = Buffer.contents out_buff in
160
prerr_endline "Output from Coq is: "; prerr_endline r;
161
Buffer.clear out_buff; r),
163
Format.pp_print_flush out_ft (); Buffer.clear out_buff)
166
let last_dir = ref ""
168
let filter_all_files () = GFile.filter
172
let filter_coq_files () = GFile.filter
173
~name:"Coq source code"
174
~patterns:[ "*.v"] ()
176
let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () =
177
let file = ref None in
178
let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title () in
179
file_chooser#add_button_stock `CANCEL `CANCEL ;
180
file_chooser#add_select_button_stock `OPEN `OPEN ;
181
file_chooser#add_filter (filter_coq_files ());
182
file_chooser#add_filter (filter_all_files ());
183
file_chooser#set_default_response `OPEN;
184
ignore (file_chooser#set_current_folder !dir);
185
begin match file_chooser#run () with
188
file := file_chooser#filename;
191
| Some s -> dir := Filename.dirname s;
193
| `DELETE_EVENT | `CANCEL -> ()
195
file_chooser#destroy ();
199
let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () =
200
let file = ref None in
201
let file_chooser = GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title () in
202
file_chooser#add_button_stock `CANCEL `CANCEL ;
203
file_chooser#add_select_button_stock `SAVE `SAVE ;
204
file_chooser#add_filter (filter_coq_files ());
205
file_chooser#add_filter (filter_all_files ());
206
(* this line will be used when a lablgtk >= 2.10.0 is the default on most distributions
207
file_chooser#set_do_overwrite_confirmation true;
209
file_chooser#set_default_response `SAVE;
210
ignore (file_chooser#set_current_folder !dir);
211
ignore (file_chooser#set_current_name filename);
213
begin match file_chooser#run () with
216
file := file_chooser#filename;
219
| Some s -> dir := Filename.dirname s;
221
| `DELETE_EVENT | `CANCEL -> ()
223
file_chooser#destroy ();
226
let find_tag_start (tag :GText.tag) (it:GText.iter) =
228
let tag = Some tag in
229
while not (it#begins_tag tag) && it#nocopy#backward_char do
233
let find_tag_stop (tag :GText.tag) (it:GText.iter) =
235
let tag = Some tag in
236
while not (it#ends_tag tag) && it#nocopy#forward_char do
240
let find_tag_limits (tag :GText.tag) (it:GText.iter) =
241
(find_tag_start tag it , find_tag_stop tag it)
243
(* explanations: Win32 threads won't work if events are produced
244
in a thread different from the thread of the Gtk loop. In this
245
case we must use GtkThread.async to push a callback in the
246
main thread. Beware that the synchronus version may produce
249
if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x)
251
if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x)
254
let m = Mutex.create() in
259
prerr_endline ("Got lock on "^text);
262
prerr_endline ("Released lock on "^text)
265
prerr_endline ("Released lock on "^text^" (on error)");
269
("Discarded call for "^text^": computations ongoing")
272
let stock_to_widget ?(size=`DIALOG) s =
273
let img = GMisc.image ()
277
let rec print_list print fmt = function
280
| x :: r -> print fmt x; print_list print fmt r
282
(* TODO: allow to report output as soon as it comes (user-fiendlier
283
for long commands like make...) *)
284
let run_command f c =
285
let result = Buffer.create 127 in
286
let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
287
let buff = String.make 127 ' ' in
288
let buffe = String.make 127 ' ' in
291
while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0
293
let r = try_convert (String.sub buff 0 !n) in
295
Buffer.add_string result r;
296
let r = try_convert (String.sub buffe 0 !ne) in
298
Buffer.add_string result r
300
(Unix.close_process_full (cin,cout,cerr), Buffer.contents result)
303
let com = Flags.subst_command_placeholder !current.cmd_browse url in
304
let s = Sys.command com in
306
f ("Could not execute\n\""^com^
307
"\"\ncheck your preferences for setting a valid browser command\n")
309
let url_for_keyword =
310
let ht = Hashtbl.create 97 in
312
let cin = open_in (lib_ide_file "index_urls.txt") in
314
let s = input_line cin in
316
let i = String.index s ',' in
317
let k = String.sub s 0 i in
318
let u = String.sub s (i + 1) (String.length s - i - 1) in
322
done with End_of_file ->
327
(Hashtbl.find ht : string -> string)
330
let browse_keyword f text =
331
try let u = url_for_keyword text in browse f (!current.doc_url ^ u)
332
with Not_found -> f ("No documentation found for "^text)
335
let underscore = Glib.Utf8.to_unichar "_" (ref 0)
337
let arobase = Glib.Utf8.to_unichar "@" (ref 0)
338
let prime = Glib.Utf8.to_unichar "'" (ref 0)
339
let bn = Glib.Utf8.to_unichar "\n" (ref 0)
340
let space = Glib.Utf8.to_unichar " " (ref 0)
341
let tab = Glib.Utf8.to_unichar "\t" (ref 0)
345
checks if two file names refer to the same (existing) file by
346
comparing their device and inode.
347
It seems that under Windows, inode is always 0, so we cannot
351
(* Optimised for partial application (in case many candidates must be
355
let s1 = Unix.stat f1 in
358
let s2 = Unix.stat f2 in
359
s1.Unix.st_dev = s2.Unix.st_dev &&
360
if Sys.os_type = "Win32" then f1 = f2
361
else s1.Unix.st_ino = s2.Unix.st_ino
363
Unix.Unix_error _ -> false)
365
Unix.Unix_error _ -> (fun _ -> false)
367
let absolute_filename f =
368
if Filename.is_relative f then
369
Filename.concat (Sys.getcwd ()) f
added
removed
ide/ideutils.ml
