Added the show_margin_right option to CoqIDE

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

5 files changed, 41 insertions, 0 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1bb645798..1f6482cbf 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2089,6 +2089,7 @@ let main files =
         let conv = { Gobject.name = "draw-spaces"; Gobject.conv = Gobject.Data.int } in
         Gobject.set conv p.script#as_widget show_spaces;
 
+        p.script#set_show_right_margin current.show_right_margin;
         p.script#set_insert_spaces_instead_of_tabs current.spaces_instead_of_tabs;
         p.script#set_tab_width current.tab_length;
         p.script#set_auto_complete current.auto_complete;
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 68ea907ce..f8f3fe930 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -144,6 +144,7 @@ type pref =
       mutable show_line_number : bool;
       mutable auto_indent : bool;
       mutable show_spaces : bool;
+      mutable show_right_margin : bool;
       mutable spaces_instead_of_tabs : bool;
       mutable tab_length : int;
       mutable highlight_current_line : bool;
@@ -219,6 +220,7 @@ let current = {
     show_line_number = false;
     auto_indent = false;
     show_spaces = true;
+    show_right_margin = false;
     spaces_instead_of_tabs = true;
     tab_length = 2;
     highlight_current_line = false;
@@ -285,6 +287,7 @@ let save_pref () =
     add "show_line_number" [string_of_bool p.show_line_number] ++
     add "auto_indent" [string_of_bool p.auto_indent] ++
     add "show_spaces" [string_of_bool p.show_spaces] ++
+    add "show_right_margin" [string_of_bool p.show_right_margin] ++
     add "spaces_instead_of_tabs" [string_of_bool p.spaces_instead_of_tabs] ++
     add "tab_length" [string_of_int p.tab_length] ++
     add "highlight_current_line" [string_of_bool p.highlight_current_line] ++
@@ -366,6 +369,7 @@ let load_pref () =
     set_bool "show_line_number" (fun v -> np.show_line_number <- v);
     set_bool "auto_indent" (fun v -> np.auto_indent <- v);
     set_bool "show_spaces" (fun v -> np.show_spaces <- v);
+    set_bool "show_right_margin" (fun v -> np.show_right_margin <- v);
     set_bool "spaces_instead_of_tabs" (fun v -> np.spaces_instead_of_tabs <- v);
     set_int "tab_length" (fun v -> np.tab_length <- v);
     set_bool "highlight_current_line" (fun v -> np.highlight_current_line <- v);
@@ -502,6 +506,7 @@ let configure ?(apply=(fun () -> ())) () =
     let auto_indent = gen_button "Auto indentation" current.auto_indent in
     let auto_complete = gen_button "Auto completion" current.auto_complete in
     let show_spaces = gen_button "Show spaces" current.show_spaces in
+    let show_right_margin = gen_button "Show right margin" current.show_right_margin in
     let spaces_instead_of_tabs =
       gen_button "Insert spaces instead of tabs"
       current.spaces_instead_of_tabs
@@ -523,6 +528,7 @@ let configure ?(apply=(fun () -> ())) () =
       current.show_line_number <- line#active;
       current.auto_indent <- auto_indent#active;
       current.show_spaces <- show_spaces#active;
+      current.show_right_margin <- show_right_margin#active;
       current.spaces_instead_of_tabs <- spaces_instead_of_tabs#active;
       current.highlight_current_line <- highlight_current_line#active;
       current.auto_complete <- auto_complete#active;
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 06bf37760..cef4c87e6 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -75,6 +75,7 @@ type pref =
       mutable show_line_number : bool;
       mutable auto_indent : bool;
       mutable show_spaces : bool;
+      mutable show_right_margin : bool;
       mutable spaces_instead_of_tabs : bool;
       mutable tab_length : int;
       mutable highlight_current_line : bool;
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 9bcdc7a3b..03df1ac17 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -225,6 +225,35 @@ object (self)
   method private may_auto_complete () =
     if auto_complete && is_auto_completing then self#do_auto_complete ()
 
+  (* HACK: missing gtksourceview features *)
+  method right_margin_position =
+    let prop = {
+      Gobject.name = "right-margin-position";
+      conv = Gobject.Data.int;
+    } in
+    Gobject.get prop obj
+
+  method set_right_margin_position pos =
+    let prop = {
+      Gobject.name = "right-margin-position";
+      conv = Gobject.Data.int;
+    } in
+    Gobject.set prop obj pos
+
+  method show_right_margin =
+    let prop = {
+      Gobject.name = "show-right-margin";
+      conv = Gobject.Data.boolean;
+    } in
+    Gobject.get prop obj
+
+  method set_show_right_margin show =
+    let prop = {
+      Gobject.name = "show-right-margin";
+      conv = Gobject.Data.boolean;
+    } in
+    Gobject.set prop obj show
+
   initializer
     (* Install undo managing *)
     ignore (self#buffer#connect#insert_text ~callback:self#handle_insert);
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index b229eacfe..ea55de115 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -18,6 +18,10 @@ object
   method clear_undo : unit -> unit
   method auto_complete : bool
   method set_auto_complete : bool -> unit
+  method right_margin_position : int
+  method set_right_margin_position : int -> unit
+  method show_right_margin : bool
+  method set_show_right_margin : bool -> unit
 end
 
 val script_view : Coq.coqtop ->