Pluging in tag preferences into buffer printing.

2 files changed, 52 insertions, 4 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 053bba805..88a8486f4 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,7 +37,25 @@ let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
+module StringMap = Map.Make(String)
 
+let translate s = s
+
+let insert_xml ?(tags = []) (buf : #GText.buffer_skel) xml =
+  let open Xml_datatype in
+  let tag name =
+    let name = translate name in
+    match GtkText.TagTable.lookup buf#tag_table name with
+    | None -> raise Not_found
+    | Some tag -> new GText.tag tag
+  in
+  let rec insert tags = function
+  | PCData s -> buf#insert ~tags:(List.rev 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
+  insert tags xml
 
 let set_location = ref  (function s -> failwith "not ready")
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 743f6e2a6..dedd62902 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -398,11 +398,41 @@ let tags = ref Util.String.Map.empty
 
 let list_tags () = !tags
 
-let () =
-  let iter name =
-    let pref = new preference ~name:[name] ~init:default_tag ~repr:Repr.(tag) in
-    tags := Util.String.Map.add name pref !tags
+let create_tag name default =
+  let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in
+  let set_tag tag =
+    begin match pref#get.tag_bg_color with
+    | None -> ()
+    | Some c -> tag#set_property (`BACKGROUND c)
+    end;
+    begin match pref#get.tag_fg_color with
+    | None -> ()
+    | Some c -> tag#set_property (`FOREGROUND c)
+    end;
+    begin match pref#get.tag_bold with
+    | false -> ()
+    | true -> tag#set_property (`WEIGHT `BOLD)
+    end;
+    begin match pref#get.tag_italic with
+    | false -> ()
+    | true -> tag#set_property (`STYLE `ITALIC)
+    end;
+    begin match pref#get.tag_underline with
+    | false -> ()
+    | true -> tag#set_property (`UNDERLINE `SINGLE)
+    end;
+  in
+  let iter table =
+    let tag = GText.tag ~name () in
+    table#add tag#as_tag;
+    pref#connect#changed (fun _ -> set_tag tag);
+    set_tag tag;
   in
+  List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
+  tags := Util.String.Map.add name pref !tags
+
+let () =
+  let iter name = create_tag name default_tag in
   List.iter iter [
     "constr.evar";
     "constr.keyword";