From e3faeb71580f85394042028499bbc9573efc23cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 Jul 2016 02:24:42 +0200 Subject: Adding a flag in CoqIDE to configure UNIX/Windows line ending. Fixes both bugs #4924 and #4437. --- ide/ideutils.ml | 24 +++++++++++++++++++----- ide/preferences.ml | 27 ++++++++++++++++++++++++++- ide/preferences.mli | 2 ++ 3 files changed, 47 insertions(+), 6 deletions(-) (limited to 'ide') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index f0698a54a3..fe69be9e48 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -112,6 +112,24 @@ let try_convert s = "(* Fatal error: wrong encoding in input. \ Please choose a correct encoding in the preference panel.*)";; +let export file_name s = + let oc = open_out_bin file_name in + let ending = line_ending#get in + let is_windows = ref false in + for i = 0 to String.length s - 1 do + match s.[i] with + | '\r' -> is_windows := true + | '\n' -> + begin match ending with + | `DEFAULT -> + if !is_windows then (output_char oc '\r'; output_char oc '\n') + else output_char oc '\n' + | `WINDOWS -> output_char oc '\r'; output_char oc '\n' + | `UNIX -> output_char oc '\n' + end + | c -> output_char oc c + done; + close_out oc let try_export file_name s = let s = @@ -134,11 +152,7 @@ let try_export file_name s = Minilib.log ("Error ("^str^") in transcoding: falling back to UTF-8"); s in - try - let oc = open_out file_name in - output_string oc s; - close_out oc; - true + try export file_name s; true with e -> Minilib.log (Printexc.to_string e);false type timer = { run : ms:int -> callback:(unit->bool) -> unit; diff --git a/ide/preferences.ml b/ide/preferences.ml index 3a33bbb1d8..3241a962dc 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -121,6 +121,18 @@ let inputenc_of_string s = else if s = "LOCALE" then Elocale else Emanual s) +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] + +let line_end_of_string = function +| "unix" -> `UNIX +| "windows" -> `WINDOWS +| _ -> `DEFAULT + +let line_end_to_string = function +| `UNIX -> "unix" +| `WINDOWS -> "windows" +| `DEFAULT -> "default" + let use_default_doc_url = "(automatic)" module Repr = @@ -381,6 +393,10 @@ let stop_before = let reset_on_tab_switch = new preference ~name:["reset_on_tab_switch"] ~init:false ~repr:Repr.(bool) +let line_ending = + let repr = Repr.custom line_end_to_string line_end_of_string in + new preference ~name:["line_ending"] ~init:`DEFAULT ~repr + let vertical_tabs = new preference ~name:["vertical_tabs"] ~init:false ~repr:Repr.(bool) @@ -818,6 +834,15 @@ let configure ?(apply=(fun () -> ())) () = (string_of_inputenc encoding#get) in + let line_ending = + combo + "EOL character" + ~f:(fun s -> line_ending#set (line_end_of_string s)) + ~new_allowed:false + ["unix"; "windows"; "default"] + (line_end_to_string line_ending#get) + in + let source_style = combo "Highlighting style:" ~f:source_style#set ~new_allowed:false @@ -973,7 +998,7 @@ let configure ?(apply=(fun () -> ())) () = Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) - encodings; + encodings; line_ending; ]); Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; diff --git a/ide/preferences.mli b/ide/preferences.mli index 426b0a328e..801869d1dc 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -11,6 +11,7 @@ val style_manager : GSourceView2.source_style_scheme_manager type project_behavior = Ignore_args | Append_args | Subst_args type inputenc = Elocale | Eutf8 | Emanual of string +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] type tag = { tag_fg_color : string option; @@ -79,6 +80,7 @@ val window_height : int preference val auto_complete : bool preference val stop_before : bool preference val reset_on_tab_switch : bool preference +val line_ending : line_ending preference val vertical_tabs : bool preference val opposite_tabs : bool preference val background_color : string preference -- cgit v1.2.3 From 6d1e0f80d215678559ada3d5b32c22c0d015454e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 14 Aug 2016 18:03:22 +0200 Subject: Fix regression in Coqide's "forward one command" command In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".". In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed. I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command". --- ide/coqOps.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 80ce99a69e..e12fda9141 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -338,8 +338,11 @@ object(self) method private show_goals_aux ?(move_insert=false) () = Coq.PrintOpt.set_printing_width proof#width; if move_insert then begin - buffer#place_cursor ~where:self#get_start_of_input; - script#recenter_insert; + let dest = self#get_start_of_input in + if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin + buffer#place_cursor ~where:dest; + script#recenter_insert + end end; Coq.bind (Coq.goals ~logger:messages#push ()) (function | Fail x -> self#handle_failure_aux ~move_insert x -- cgit v1.2.3