From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- ide/ideutils.ml | 103 ++++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 78 insertions(+), 25 deletions(-) (limited to 'ide/ideutils.ml') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 44a86556..06a13273 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -9,8 +9,6 @@ open Preferences -exception Forbidden - let warn_image () = let img = GMisc.image () in img#set_stock `DIALOG_WARNING; @@ -31,13 +29,54 @@ let push_info,pop_info,clear_info = 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) + (fun () -> for _i = 1 to !size do status_context#pop () done; size := 0) let flash_info = let flash_context = status#new_context ~name:"Flash" in (fun ?(delay=5000) s -> flash_context#flash ~delay s) - +let xml_to_string xml = + let open Xml_datatype in + let buf = Buffer.create 1024 in + let rec iter = function + | PCData s -> Buffer.add_string buf s + | Element (_, _, children) -> + List.iter iter children + in + let () = iter (Richpp.repr xml) in + Buffer.contents buf + +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 tags + +let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = + let open Xml_datatype 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 + let rec insert tags = function + | PCData s -> insert_with_tags buf mark rmark tags s + | Element (t, _, children) -> + let tags = try tag t :: tags with Not_found -> tags in + List.iter (fun xml -> insert tags xml) children + in + let () = try insert tags (Richpp.repr msg) with _ -> () in + buf#delete_mark rmark let set_location = ref (function s -> failwith "not ready") @@ -74,7 +113,7 @@ let do_convert s = in let s = if Glib.Utf8.validate s then (Minilib.log "Input is UTF-8"; s) - else match current.encoding with + else match encoding#get with |Preferences.Eutf8 | Preferences.Elocale -> from_loc () |Emanual enc -> try from_manual enc with _ -> from_loc () in @@ -87,10 +126,28 @@ let try_convert s = "(* 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 current.encoding with + try match encoding#get with |Eutf8 -> Minilib.log "UTF-8 is enforced" ; s |Elocale -> let is_unicode,char_set = Glib.Convert.get_charset () in @@ -109,11 +166,7 @@ let try_export file_name s = Minilib.log ("Error ("^str^") in transcoding: falling back to UTF-8"); s in - try - let oc = open_out file_name in - output_string oc s; - close_out oc; - true + try export file_name s; true with e -> Minilib.log (Printexc.to_string e);false type timer = { run : ms:int -> callback:(unit->bool) -> unit; @@ -140,7 +193,7 @@ let filter_coq_files () = GFile.filter ~name:"Coq source code" ~patterns:[ "*.v"] () -let current_dir () = match current.project_path with +let current_dir () = match project_path#get with | None -> "" | Some dir -> dir @@ -164,7 +217,7 @@ let select_file_for_open ~title ?filename () = match file_chooser#filename with | None -> None | Some _ as f -> - current.project_path <- file_chooser#current_folder; f + project_path#set file_chooser#current_folder; f end | `DELETE_EVENT | `CANCEL -> None in file_chooser#destroy (); @@ -193,7 +246,7 @@ let select_file_for_save ~title ?filename () = file := file_chooser#filename; match !file with None -> () - | Some s -> current.project_path <- file_chooser#current_folder + | Some s -> project_path#set file_chooser#current_folder end | `DELETE_EVENT | `CANCEL -> () end ; @@ -238,7 +291,7 @@ let coqtop_path () = let file = match !custom_coqtop with | Some s -> s | None -> - match current.cmd_coqtop with + match cmd_coqtop#get with | Some s -> s | None -> let prog = String.copy Sys.executable_name in @@ -272,17 +325,17 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Pp.message_level -> string -> unit +type logger = Feedback.level -> Richpp.richpp -> unit let default_logger level message = let level = match level with - | Pp.Debug _ -> `DEBUG - | Pp.Info -> `INFO - | Pp.Notice -> `NOTICE - | Pp.Warning -> `WARNING - | Pp.Error -> `ERROR + | Feedback.Debug -> `DEBUG + | Feedback.Info -> `INFO + | Feedback.Notice -> `NOTICE + | Feedback.Warning -> `WARNING + | Feedback.Error -> `ERROR in - Minilib.log ~level message + Minilib.log ~level (xml_to_string message) (** {6 File operations} *) @@ -364,7 +417,7 @@ let run_command display finally cmd = (** Web browsing *) let browse prerr url = - let com = Util.subst_command_placeholder current.cmd_browse url in + let com = Util.subst_command_placeholder cmd_browse#get url in let finally = function | Unix.WEXITED 127 -> prerr @@ -375,13 +428,13 @@ let browse prerr url = run_command (fun _ -> ()) finally com let doc_url () = - if current.doc_url = use_default_doc_url || current.doc_url = "" + if doc_url#get = use_default_doc_url || doc_url#get = "" then 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 + else doc_url#get let url_for_keyword = let ht = Hashtbl.create 97 in -- cgit v1.2.3