Merge branch 'v8.6'

4 files changed, 52 insertions, 8 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 18557ab6b..50b3f2c0a 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -339,8 +339,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
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index f0698a54a..fe69be9e4 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 3a33bbb1d..3241a962d 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 426b0a328..801869d1d 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