undoable_view is a source_view

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

3 files changed, 39 insertions, 32 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index dae237660b..b42651bdc7 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1417,7 +1417,7 @@ let search_next_error () =
 let create_session file =
   let script =
     Undo.undoable_view
-      ~buffer:(GText.buffer ~tag_table:Tags.Script.table ())
+      ~source_buffer:(GSourceView2.source_buffer ~tag_table:Tags.Script.table ())
       ~wrap_mode:`NONE () in
   let proof =
     GText.view
diff --git a/ide/undo.ml b/ide/undo.ml
index 57724297dc..cb3f455d1e 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -16,10 +16,10 @@ let neg act = match act with
   | Insert (s,i,l) -> Delete (s,i,l)
   | Delete (s,i,l) -> Insert (s,i,l)
 
-class undoable_view (tv:[>Gtk.text_view] Gtk.obj) =
+class undoable_view (tv:GtkSourceView2_types.source_view Gtk.obj) =
   let undo_lock = ref true in
 object(self)
-  inherit GText.view tv as super
+  inherit GSourceView2.source_view tv as super
   val history = (Stack.create () : action Stack.t)
   val redo = (Queue.create () : action Queue.t)
   val nredo = (Stack.create () : action Stack.t)
@@ -162,14 +162,14 @@ object(self)
 	      ))
 end
 
-let undoable_view ?(buffer:GText.buffer option) =
-  GtkText.View.make_params []
-    ~cont:(GContainer.pack_container
-	     ~create:
-	     (fun pl -> let w = match buffer with
-	      | None -> GtkText.View.create []
-	      | Some b -> GtkText.View.create_with_buffer b#as_buffer
-	      in
-	      Gobject.set_params w pl; ((new undoable_view w):undoable_view)))
-
-
+let undoable_view ?(source_buffer:GSourceView2.source_buffer option)  ?draw_spaces =
+  GtkSourceView2.SourceView.make_params [] ~cont:(
+    GtkText.View.make_params ~cont:(
+      GContainer.pack_container ~create:
+	(fun pl -> let w = match source_buffer with
+	  | None -> GtkSourceView2.SourceView.new_ ()
+	  | Some buf -> GtkSourceView2.SourceView.new_with_buffer
+            (Gobject.try_cast buf#as_buffer "GtkSourceBuffer") in
+		   Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
+		   Gaux.may (GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
+		   ((new undoable_view w):undoable_view))))
diff --git a/ide/undo.mli b/ide/undo.mli
index d9451fd1ae..03e2885cde 100644
--- a/ide/undo.mli
+++ b/ide/undo.mli
@@ -8,28 +8,35 @@
 
 (* An undoable view class *)
 
-class undoable_view : ([> Gtk.text_view] as 'a) Gtk.obj ->
+class undoable_view : GtkSourceView2_types.source_view Gtk.obj ->
 object
-  inherit GText.view
-  val obj : 'a Gtk.obj
+  inherit GSourceView2.source_view
   method undo : bool
   method redo : bool
   method clear_undo : unit
 end
 
 val undoable_view :
-    ?buffer:GText.buffer ->
-    ?editable:bool ->
-    ?cursor_visible:bool ->
-    ?justification:GtkEnums.justification ->
-    ?wrap_mode:GtkEnums.wrap_mode ->
-    ?accepts_tab:bool ->
-    ?border_width:int ->
-    ?width:int ->
-    ?height:int ->
-    ?packing:(GObj.widget -> unit) ->
-    ?show:bool ->
-    unit ->
-  undoable_view
-
-
+           ?source_buffer:GSourceView2.source_buffer ->
+           ?draw_spaces:SourceView2Enums.source_draw_spaces_flags list ->
+           ?auto_indent:bool ->
+           ?highlight_current_line:bool ->
+           ?indent_on_tab:bool ->
+           ?indent_width:int ->
+           ?insert_spaces_instead_of_tabs:bool ->
+           ?right_margin_position:int ->
+           ?show_line_marks:bool ->
+           ?show_line_numbers:bool ->
+           ?show_right_margin:bool ->
+           ?smart_home_end:SourceView2Enums.source_smart_home_end_type ->
+           ?tab_width:int ->
+           ?editable:bool ->
+           ?cursor_visible:bool ->
+           ?justification:GtkEnums.justification ->
+           ?wrap_mode:GtkEnums.wrap_mode ->
+           ?accepts_tab:bool ->
+           ?border_width:int ->
+           ?width:int ->
+           ?height:int ->
+           ?packing:(GObj.widget -> unit) ->
+           ?show:bool -> unit -> undoable_view