Granting wish #1781:

	Parenthesis matching on click in all term displays.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16643 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 22 insertions, 12 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 7c4aa3713b..69dd005353 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -252,7 +252,7 @@ let rec print_list print fmt = function
 
 let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd
 
-let textview_width (view : #GText.view) =
+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
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index c22c167ba3..3d950ead8c 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -64,7 +64,7 @@ val set_location : (string -> unit) ref
 
 val requote : string -> string
 
-val textview_width : #GText.view -> int
+val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
 type logger = Interface.message_level -> string -> unit
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index d3513536eb..13c3d4cdbc 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -20,11 +20,16 @@ class type message_view =
   end
 
 let message_view () : message_view =
-  let buffer = GText.buffer ~tag_table:Tags.Message.table () in
+  let buffer = GSourceView2.source_buffer
+    ~highlight_matching_brackets:true
+    ~tag_table:Tags.Message.table ()
+  in
+  let text_buffer = new GText.buffer buffer#as_buffer in
   let box = GPack.vbox () in
   let scroll = GBin.scrolled_window
     ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in
-  let view = GText.view ~buffer ~packing:scroll#add
+  let view = GSourceView2.source_view
+    ~source_buffer:buffer ~packing:scroll#add
     ~editable:false ~cursor_visible:false ~wrap_mode:`WORD ()
   in
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
@@ -49,7 +54,7 @@ let message_view () : message_view =
 
     method set msg = self#clear; self#add msg
 
-    method buffer = buffer
+    method buffer = text_buffer
 
     method modify_font fd = view#misc#modify_font fd
 
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 5da0eecebc..90af0af393 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -43,7 +43,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb =
                      hover_cb start stop; false
                  | _ -> false))
 
-let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
+let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
   | [] -> assert false
   | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals ->
       let on_hover sel_start sel_stop =
@@ -107,7 +107,7 @@ let mode_tactic sel_cb (proof:GText.view) 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) = function
+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";
@@ -124,7 +124,7 @@ let rec flatten = function
   let inner = flatten l in
   List.rev_append lg inner @ rg
 
-let display mode (view:GText.view) goals hints evars =
+let display mode (view : #GText.view_skel) goals hints evars =
   let () = view#buffer#set_text "" in
   match goals with
   | None -> ()
@@ -156,8 +156,13 @@ let display mode (view:GText.view) goals hints evars =
     mode view fg hints
 
 let proof_view () =
-  let buffer = GText.buffer ~tag_table:Tags.Proof.table () in
-  let view = GText.view ~buffer ~editable:false ~wrap_mode:`WORD () in
+  let buffer = GSourceView2.source_buffer
+    ~highlight_matching_brackets:true
+    ~tag_table:Tags.Proof.table ()
+  in
+  let view = GSourceView2.source_view
+    ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD ()
+  in
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
   object
@@ -173,9 +178,9 @@ let proof_view () =
 
     method refresh () =
       let dummy _ () = () in
-      display (mode_tactic dummy) view goals None evars
+      display (mode_tactic dummy) (view :> GText.view_skel) goals None evars
 
-    method width = Ideutils.textview_width view
+    method width = Ideutils.textview_width (view :> GText.view_skel)
   end
 
 (*     ignore (proof_buffer#add_selection_clipboard cb); *)