From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 ide/wg_ProofView.ml | 41 ++++++++++++++++++++---------------------
 1 file changed, 20 insertions(+), 21 deletions(-)

(limited to 'ide/wg_ProofView.ml')

diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 0007203e..47c86045 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -7,6 +7,8 @@
 (************************************************************************)
 
 open Util
+open Preferences
+open Ideutils
 
 class type proof_view =
   object
@@ -82,26 +84,28 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           let () = hook_tag_cb tag hint sel_cb on_hover in
           [tag], hints
         in
-        let () = proof#buffer#insert ~tags (hyp ^ "\n") in
+        let () = insert_xml ~tags proof#buffer hyp in
+        proof#buffer#insert "\n";
         insert_hyp rem_hints hs
       in
       let () = proof#buffer#insert head_str in
       let () = insert_hyp hyps_hints hyps in
       let () =
-        let tags = Tags.Proof.goal :: if goal_hints <> [] then
+        let _ = if goal_hints <> [] then
           let tag = proof#buffer#create_tag [] in
           let () = hook_tag_cb tag goal_hints sel_cb on_hover in
           [tag]
           else []
         in
         proof#buffer#insert (goal_str 1 goals_cnt);
-        proof#buffer#insert ~tags cur_goal;
+        insert_xml proof#buffer cur_goal;
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
       let fold_goal i _ { Interface.goal_ccl = g } =
         proof#buffer#insert (goal_str i goals_cnt);
-        proof#buffer#insert (g ^ "\n")
+        insert_xml proof#buffer g;
+        proof#buffer#insert "\n"
       in
       let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
 
@@ -110,17 +114,6 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
                          (Some Tags.Proof.goal)));
       ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT)
 
-let mode_cesar (proof : #GText.view_skel) = function
-  | [] -> assert false
-  | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ ->
-      proof#buffer#insert "    *** Declarative Mode ***\n";
-      List.iter
-        (fun hyp -> proof#buffer#insert (hyp^"\n"))
-        hyps;
-      proof#buffer#insert "______________________________________\n";
-      proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
-      ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
-
 let rec flatten = function
 | [] -> []
 | (lg, rg) :: l ->
@@ -151,8 +144,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* The proof is finished, with the exception of given up goals. *)
       view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iter iter given_up_goals;
       view#buffer#insert "\nYou need to go back and solve them."
@@ -160,8 +153,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
       let iter goal =
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iter iter shelved_goals
     | _, _, _, _ ->
@@ -173,8 +166,8 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
       let iter i goal =
         let () = view#buffer#insert (goal_str (succ i)) in
-        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-        view#buffer#insert msg
+        insert_xml view#buffer goal.Interface.goal_ccl;
+        view#buffer#insert "\n"
       in
       List.iteri iter bg
     end
@@ -193,6 +186,12 @@ let proof_view () =
   let () = Gtk_parsing.fix_double_click view in
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
+  let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
+  let _ = background_color#connect#changed cb in
+  let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
+  let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
+  stick text_font view cb;
+
   object
     inherit GObj.widget view#as_widget
     val mutable goals = None
-- 
cgit v1.2.3