diff options
Diffstat (limited to 'ide/coqide/ideutils.ml')
| -rw-r--r-- | ide/coqide/ideutils.ml | 607 |
1 files changed, 607 insertions, 0 deletions
diff --git a/ide/coqide/ideutils.ml b/ide/coqide/ideutils.ml new file mode 100644 index 0000000000..482cecc1f8 --- /dev/null +++ b/ide/coqide/ideutils.ml @@ -0,0 +1,607 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Preferences + +let _ = GtkMain.Main.init () + +let warn_image () = + let img = GMisc.image () in + img#set_stock `DIALOG_WARNING; + img#set_icon_size `DIALOG; + img + +let warning msg = + GToolbox.message_box ~title:"Warning" ~icon:(warn_image ())#coerce msg + +let cb = GData.clipboard Gdk.Atom.primary + +(* status bar and locations *) + +let status = GMisc.statusbar () + +let push_info,pop_info,clear_info = + let status_context = status#new_context ~name:"Messages" in + let size = ref 0 in + (fun s -> incr size; ignore (status_context#push s)), + (fun () -> decr size; status_context#pop ()), + (fun () -> for _i = 1 to !size do status_context#pop () done; size := 0) + +type 'a mlist = Nil | Cons of { hd : 'a ; mutable tl : 'a mlist } + +let enqueue a x = + let rec aux x = match x with + | Nil -> assert false + | Cons p -> + match p.tl with + | Nil -> p.tl <- Cons { hd = a ; tl = Nil } + | _ -> aux p.tl in + match !x with + | Nil -> x := Cons { hd = a ; tl = Nil } + | _ -> aux !x + +let pop = function + | Cons p -> p.tl + | Nil -> assert false + +let flash_info = + let queue = ref Nil in + let flash_context = status#new_context ~name:"Flash" in + let rec process () = match !queue with + | Cons { hd = (delay,text) } -> + let msg = flash_context#push text in + ignore (Glib.Timeout.add ~ms:delay ~callback:(fun () -> + flash_context#remove msg; + queue := pop !queue; + process (); false)) + | Nil -> () in + fun ?(delay=5000) text -> + let processing = !queue <> Nil in + enqueue (delay,text) queue; + if not processing then process () + +(* Note: Setting the same attribute with two separate tags appears to use +the first value applied and not the second. I saw this trying to set the background +color on Windows. A clean fix, if ever needed, would be to combine the attributes +of the tags into a single composite tag before applying. This is left as an +exercise for the reader. *) +let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = + (* FIXME: LablGTK2 does not export the C insert_with_tags function, so that + it has to reimplement its own helper function. Unluckily, it relies on + a slow algorithm, so that we have to have our own quicker version here. + Alas, it is still much slower than the native version... *) + if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) text + else + let it = buf#get_iter_at_mark mark in + let () = buf#move_mark rmark ~where:it in + let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in + let start = buf#get_iter_at_mark mark in + let stop = buf#get_iter_at_mark rmark in + let iter tag = buf#apply_tag tag ~start ~stop in + List.iter iter (List.rev tags) + +let nl_white_regex = Str.regexp "^\\( *\n *\\)" +let diff_regex = Str.regexp "^diff." + +let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = + let open Xml_datatype in + let dtags = ref [] in + let tag name = + match GtkText.TagTable.lookup buf#tag_table name with + | None -> raise Not_found + | Some tag -> new GText.tag tag + in + let rmark = `MARK (buf#create_mark buf#start_iter) in + (* insert the string, but don't apply diff highlights to white space at the begin/end of line *) + let rec insert_str tags s = + let etags = try List.hd !dtags :: tags with hd -> tags in + try + let start = Str.search_forward nl_white_regex s 0 in + insert_with_tags buf mark rmark etags (String.sub s 0 start); + insert_with_tags buf mark rmark tags (Str.matched_group 1 s); + let mend = Str.match_end () in + insert_str tags (String.sub s mend (String.length s - mend)) + with Not_found -> + insert_with_tags buf mark rmark etags s + in + let rec insert tags = function + | PCData s -> insert_str tags s + | Element (t, _, children) -> + let (pfx, tname) = Pp.split_tag t in + let is_diff = try let _ = Str.search_forward diff_regex tname 0 in true with Not_found -> false in + let (tags, have_tag) = + try + let t = tag tname in + if is_diff && pfx <> Pp.end_pfx then + dtags := t :: !dtags; + if pfx = "" then + ((if is_diff then tags else t :: tags), true) + else + (tags, true) + with Not_found -> (tags, false) + in + List.iter (fun xml -> insert tags xml) children; + if have_tag && is_diff && pfx <> Pp.start_pfx then + dtags := (try List.tl !dtags with tl -> []); + in + let () = try insert tags msg with _ -> () in + buf#delete_mark rmark + +let set_location = ref (function s -> failwith "not ready") + +let display_location ins = + let line = ins#line + 1 in + let off = ins#line_offset + 1 in + let msg = Printf.sprintf "Line: %5d Char: %3d" line off in + !set_location msg + +(** A utf8 char is either a single byte (ascii char, 0xxxxxxx) + or multi-byte (with a leading byte 11xxxxxx and extra bytes 10xxxxxx) *) + +let is_extra_byte c = ((Char.code c) lsr 6 = 2) + +(** For a string buffer that may contain utf8 chars, + we convert a byte offset into a char offset + by only counting char-starting bytes. + Normally the string buffer starts with a char-starting byte + (buffer produced by a [#get_text]) *) + +let byte_offset_to_char_offset s byte_offset = + let extra_bytes = ref 0 in + for i = 0 to min byte_offset (String.length s - 1) do + if is_extra_byte s.[i] then incr extra_bytes + done; + byte_offset - !extra_bytes + +let glib_utf8_pos_to_offset s ~off = byte_offset_to_char_offset s off + +let do_convert s = + 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 + let s = + if Glib.Utf8.validate s then (Minilib.log "Input is UTF-8"; s) + else match encoding#get with + |Preferences.Eutf8 | Preferences.Elocale -> from_loc () + |Emanual enc -> try from_manual enc with _ -> from_loc () + in + Utf8_convert.f s + +let try_convert s = + try + do_convert s + with _ -> + "(* Fatal error: wrong encoding in input. \ +Please choose a correct encoding in the preference panel.*)";; + +let export file_name s = + let oc = open_out_bin file_name in + let ending = line_ending#get in + let is_windows = ref false in + for i = 0 to String.length s - 1 do + match s.[i] with + | '\r' -> is_windows := true + | '\n' -> + begin match ending with + | `DEFAULT -> + if !is_windows then (output_char oc '\r'; output_char oc '\n') + else output_char oc '\n' + | `WINDOWS -> output_char oc '\r'; output_char oc '\n' + | `UNIX -> output_char oc '\n' + end + | c -> output_char oc c + done; + close_out oc + +let try_export file_name s = + let s = + try match encoding#get with + |Eutf8 -> Minilib.log "UTF-8 is enforced" ; s + |Elocale -> + let is_unicode,char_set = Glib.Convert.get_charset () in + if is_unicode then + (Minilib.log "Locale is UTF-8" ; s) + else + (Minilib.log ("Locale is "^char_set); + Glib.Convert.convert_with_fallback + ~from_codeset:"UTF-8" ~to_codeset:char_set s) + |Emanual enc -> + (Minilib.log ("Manual charset is "^ enc); + Glib.Convert.convert_with_fallback + ~from_codeset:"UTF-8" ~to_codeset:enc s) + with e -> + let str = Printexc.to_string e in + Minilib.log ("Error ("^str^") in transcoding: falling back to UTF-8"); + s + in + try export file_name s; true + with e -> Minilib.log (Printexc.to_string e);false + +type timer = { run : ms:int -> callback:(unit->bool) -> unit; + kill : unit -> unit } + +let mktimer () = + let timer = ref None in + { run = + (fun ~ms ~callback -> + timer := Some (GMain.Timeout.add ~ms ~callback)); + kill = + (fun () -> match !timer with + | None -> () + | Some id -> + (try GMain.Timeout.remove id + with Glib.GError _ -> ()); + timer := None) } + +let filter_all_files () = GFile.filter + ~name:"All" + ~patterns:["*"] () + +let filter_coq_files () = GFile.filter + ~name:"Coq source code" + ~patterns:[ "*.v"] () + +let current_dir () = match project_path#get with +| None -> "" +| Some dir -> dir + +let select_file_for_open ~title ?(filter=true) ?(multiple=false) ?parent ?filename () = + let file_chooser = + GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ?parent () + in + file_chooser#add_button_stock `CANCEL `CANCEL ; + file_chooser#add_select_button_stock `OPEN `OPEN ; + if filter then + begin + file_chooser#add_filter (filter_coq_files ()); + file_chooser#add_filter (filter_all_files ()) + end; + file_chooser#set_default_response `OPEN; + file_chooser#set_select_multiple multiple; + let dir = match filename with + | None -> current_dir () + | Some f -> Filename.dirname f in + ignore (file_chooser#set_current_folder dir); + let file = + match file_chooser#run () with + | `OPEN -> + begin + let filenames = file_chooser#get_filenames in + (if filenames <> [] then + project_path#set file_chooser#current_folder); + filenames + end + | `DELETE_EVENT | `CANCEL -> [] in + file_chooser#destroy (); + file + +let select_file_for_save ~title ?parent ?filename () = + let file = ref None in + let file_chooser = + GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title ?parent () + 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 ()); + file_chooser#set_do_overwrite_confirmation true; + file_chooser#set_default_response `SAVE; + let dir,filename = match filename with + |None -> current_dir (), "" + |Some f -> Filename.dirname f, Filename.basename f + in + ignore (file_chooser#set_current_folder dir); + ignore (file_chooser#set_current_name filename); + begin match file_chooser#run () with + | `SAVE -> + begin + file := file_chooser#filename; + match !file with + None -> () + | Some s -> project_path#set file_chooser#current_folder + end + | `DELETE_EVENT | `CANCEL -> () + end ; + file_chooser#destroy (); + !file + +let find_tag_start (tag :GText.tag) (it:GText.iter) = + let it = it#copy in + let tag = Some tag in + while not (it#begins_tag tag) && it#nocopy#backward_char do + () + done; + it +let find_tag_stop (tag :GText.tag) (it:GText.iter) = + let it = it#copy in + let tag = Some tag in + while not (it#ends_tag tag) && it#nocopy#forward_char do + () + done; + it +let find_tag_limits (tag :GText.tag) (it:GText.iter) = + (find_tag_start tag it , find_tag_stop tag it) + +let stock_to_widget ?(size=`BUTTON) s = + let img = GMisc.image () in + (match size with + | `CUSTOM(width,height) -> + let opb = img#misc#render_icon ~size:`BUTTON s in + let pb = GdkPixbuf.create ~width ~height + ~bits:(GdkPixbuf.get_bits_per_sample opb) + ~has_alpha:(GdkPixbuf.get_has_alpha opb) () in + GdkPixbuf.scale ~width ~height ~dest:pb opb; + img#set_pixbuf pb + | #Gtk.Tags.icon_size as icon_size -> + img#set_stock s; + img#set_icon_size icon_size); + img#coerce + +let custom_coqtop = ref None + +let coqtop_path () = + let file = match !custom_coqtop with + | Some s -> s + | None -> + match cmd_coqtop#get with + | Some s -> s + | None -> + try + let new_prog = System.get_toplevel_path "coqidetop" in + (* The file exists or it is to be found by path *) + if Sys.file_exists new_prog || + CString.equal Filename.(basename new_prog) new_prog + then new_prog + else + let in_macos_bundle = + Filename.concat + (Filename.dirname new_prog) + (Filename.concat "../Resources/bin" (Filename.basename new_prog)) + in if Sys.file_exists in_macos_bundle then in_macos_bundle + else "coqidetop.opt" + with Not_found -> "coqidetop.opt" + in file + +(* 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 + +let textview_width (view : #GText.view_skel) = + let rect = view#visible_rect in + let pixel_width = Gdk.Rectangle.width rect in + let metrics = view#misc#pango_context#get_metrics () in + let char_width = GPango.to_pixels metrics#approx_char_width in + pixel_width / char_width + +type logger = Feedback.level -> Pp.t -> unit + +let default_logger level message = + let level = match level with + | Feedback.Debug -> `DEBUG + | Feedback.Info -> `INFO + | Feedback.Notice -> `NOTICE + | Feedback.Warning -> `WARNING + | Feedback.Error -> `ERROR + in + Minilib.log_pp ~level message + + +(** {6 File operations} *) + +(** A customized [stat] function. Exceptions are caught. *) + +type stats = MTime of float | NoSuchFile | OtherError + +let stat f = + try MTime (Unix.stat f).Unix.st_mtime + with + | Unix.Unix_error (Unix.ENOENT,_,_) -> NoSuchFile + | _ -> OtherError + +(** I/O utilities + + Note: In a mono-thread coqide, we use the same buffer for + different read operations *) + +let maxread = 4096 + +let read_string = Bytes.create maxread +let read_buffer = Buffer.create maxread + +(** Read the content of file [f] and add it to buffer [b]. + I/O Exceptions are propagated. *) + +let read_file name buf = + let ic = Util.open_utf8_file_in name in + let len = ref 0 in + try + while len := input ic read_string 0 maxread; !len > 0 do + Buffer.add_subbytes buf read_string 0 !len + done; + close_in ic + with e -> close_in ic; raise e + +(** Read what is available on a gtk channel. This channel should have been + set as non-blocking. When there's nothing more to read, the inner loop + will be exited via a GError exception concerning a EAGAIN unix error. + Anyway, any other exception also stops the read. *) + +let io_read_all chan = + Buffer.clear read_buffer; + let read_once () = + let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in + Buffer.add_subbytes read_buffer read_string 0 len + in + begin + try while true do read_once () done + with Glib.GError _ -> () + end; + Buffer.contents read_buffer + +(** Run an external command asynchronously *) + +let run_command display finally cmd = + let cin = Unix.open_process_in cmd in + let fd = Unix.descr_of_in_channel cin in + let () = Unix.set_nonblock fd in + let io_chan = Glib.Io.channel_of_descr fd in + let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *) + let rec has_errors = function + | [] -> false + | (`IN | `PRI) :: conds -> has_errors conds + | e :: _ -> true + in + let handle_end () = finally (Unix.close_process_in cin); false + in + let handle_input conds = + if has_errors conds then handle_end () + else + let s = io_read_all io_chan in + if s = "" then handle_end () + else (display (try_convert s); true) + in + ignore (Glib.Io.add_watch ~cond:all_conds ~callback:handle_input io_chan) + +(** Web browsing *) + +let browse prerr url = + let com = Util.subst_command_placeholder cmd_browse#get url in + let finally = function + | Unix.WEXITED 127 -> + prerr + ("Could not execute:\n"^com^"\n"^ + "check your preferences for setting a valid browser command\n") + | _ -> () + in + run_command (fun _ -> ()) finally com + +let url_for_keyword = + let ht = Hashtbl.create 97 in + 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.coqide_data_dirs ())) "index_urls.txt" in + open_in index_urls + with Not_found -> 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.log "Warning: Cannot parse documentation index file." + done with End_of_file -> + close_in cin + with _ -> + Minilib.log "Warning: Cannot find documentation index file." + end; + Hashtbl.find ht : string -> string) + +let browse_keyword prerr text = + try + let u = Lazy.force url_for_keyword text in + browse prerr (Coq_config.wwwrefman ^ u) + with Not_found -> prerr ("No documentation found for \""^text^"\".\n") + +let rec is_valid (s : Pp.t) = match Pp.repr s with + | Pp.Ppcmd_empty + | Pp.Ppcmd_print_break _ + | Pp.Ppcmd_force_newline -> true + | Pp.Ppcmd_glue l -> List.for_all is_valid l + | Pp.Ppcmd_string s -> Glib.Utf8.validate s + | Pp.Ppcmd_box (_,s) + | Pp.Ppcmd_tag (_,s) -> is_valid s + | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s +let validate s = + if is_valid s then s else Pp.str "This error massage can't be printed." + +(** encoding list of strings as a string in a shell-like compatible way: + string with spaces and no ' -> '...' + string with spaces and ' -> split string into substrings separated with \' + ' -> \' + \ -> \\ + *) + +let decode_string_list s = + let l = String.length s in + let fail_backslash () = + failwith "Backslash is used to quote single quotes in quoted strings; it should otherwise be doubled" in + let rec find_word quoted b i = + if i = l then + if quoted then failwith "Unmatched single quote" + else i + else + let c = s.[i] in + if c = ' ' && not quoted then i+1 + else if c = '\'' then find_word (not quoted) b (i+1) + else if c = '\\' && not quoted then + if i = l-1 then fail_backslash () + else + let c = s.[i+1] in + if c = '\'' || c = '\\' then + (Buffer.add_char b c; find_word quoted b (i+2)) + else fail_backslash () + else + (Buffer.add_char b c; + find_word quoted b (i+1)) in + let rec collect_words i = + if i = l then [] else + let b = Buffer.create l in + let i = find_word false b i in + Buffer.contents b :: collect_words i in + collect_words 0 + +let needs_quote s i = + (* Tells if there is a space and if a space, before the next single quote *) + match CString.index_from_opt s i ' ', CString.index_from_opt s i '\'' with + | Some _, None -> true + | Some i, Some j -> i < j + | _ -> false + +let encode_string s = + (* Could be optimized so that "a b'c" is "'a b'\'c" rather than "'a b'\''c'" *) + let l = String.length s in + let b = Buffer.create (l + 10) in + let close quoted = if quoted then Buffer.add_char b '\'' in + let rec aux quoted i = + if i = l then close quoted + else + let c = s.[i] in + if c = '\'' then + (close quoted; + Buffer.add_string b "\\'"; + start (i+1)) + else if c = '\\' && not quoted then + (Buffer.add_string b "\\\\"; aux quoted (i+1)) + else + (Buffer.add_char b c; aux quoted (i+1)) + and start i = + let q = needs_quote s i in + if q then Buffer.add_char b '\''; + aux q i in + start 0; + Buffer.contents b + +let encode_string_list l = String.concat " " (List.map encode_string l) |