1 files changed, 78 insertions, 25 deletions

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