diff options
| -rw-r--r-- | ide/coqide.ml | 1 | ||||
| -rw-r--r-- | ide/preferences.ml | 6 | ||||
| -rw-r--r-- | ide/preferences.mli | 1 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 29 | ||||
| -rw-r--r-- | ide/wg_ScriptView.mli | 4 |
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 -> |