Coqide: the coqtop to launch is a preference.

If it is AUTO then we keep the heuristic to change coqide by coqtop in Sys.executable_name.
If it fails coqtop location must be given by the users.

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

8 files changed, 95 insertions, 47 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index cf73749a8..3f96e66a3 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -54,23 +54,46 @@ let rec read_all_lines in_chan =
     arg::(read_all_lines in_chan)
   with End_of_file -> []
 
-let filter_coq_opts args =
+let rec filter_coq_opts args =
+  let coqprog = coqtop_path () in
+  let asks_for_coqtop () =
+    let pb_mes = GWindow.message_dialog ~message:"Fail to load coqtop. Reset the preference to default ?"
+      ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
+    match pb_mes#run () with
+      | `YES ->
+ 	let () = !Preferences.current.Preferences.cmd_coqtop  <- None in
+	    let () = custom_coqtop := None in
+	let () = pb_mes#destroy () in
+	filter_coq_opts args
+      | `DELETE_EVENT | `NO ->
+	let () = pb_mes#destroy () in
+	let cmd_sel = GWindow.file_selection ~title:"Coqtop to execute (edit your preference then)"
+	  ~filename:coqprog ~urgency_hint:true () in
+	match cmd_sel#run () with
+	  | `OK ->
+	    let () = custom_coqtop := (Some cmd_sel#filename) in
+	    let () = cmd_sel#destroy () in
+	    filter_coq_opts args
+	  | `HELP -> exit 0
+	  | `CANCEL | `DELETE_EVENT -> exit 0
+  in
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let cmd = Filename.quote !Minilib.coqtop_path ^" -nois -filteropts " ^ argstr in
-  let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
-  let filtered_args = read_all_lines oc in
-  let message = read_all_lines ec in
-  match Unix.close_process_full (oc,ic,ec) with
-    | Unix.WEXITED 0 -> true,filtered_args
-    | Unix.WEXITED 2 -> false,filtered_args
-    | _ -> false,message
+  let cmd = Filename.quote coqprog ^" -nois -filteropts " ^ argstr in
+  try
+    let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
+    let filtered_args = read_all_lines oc in
+    match Unix.close_process_full (oc,ic,ec) with
+      | Unix.WEXITED 0 -> true,filtered_args
+      | Unix.WEXITED 2 -> false,filtered_args
+      | _ -> asks_for_coqtop ()
+  with Sys_error _ -> asks_for_coqtop ()
 
 exception Coqtop_output of string list
 
 let check_connection args =
   try
     let argstr = String.concat " " (List.map Filename.quote args) in
-    let cmd = Filename.quote !Minilib.coqtop_path ^ " -batch " ^ argstr in
+    let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
     let ic = Unix.open_process_in cmd in
     let lines = read_all_lines ic in
     match Unix.close_process_in ic with
@@ -139,7 +162,7 @@ let open_process_pid prog args =
 let spawn_coqtop sup_args =
   Mutex.lock toplvl_ctr_mtx;
   try
-    let prog = !Minilib.coqtop_path in
+    let prog = coqtop_path () in
     let args = Array.of_list (prog :: "-ideslave" :: sup_args) in
     let (pid,ic,oc) = open_process_pid prog args in
     incr toplvl_ctr;
diff --git a/ide/coq.mli b/ide/coq.mli
index 9d64da6c2..f2aa4abad 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -13,11 +13,13 @@
 val short_version : unit -> string
 val version : unit -> string
 
-(** * Initial checks by launching test coqtop processes *)
-
+(** * Launch a test coqtop processes, ask for a correct coqtop if it fails.
+    @return if coqide should go further & the list of arguments that coqtop
+    did not understand. (the files probably ..) *)
 val filter_coq_opts : string list -> bool * string list
 
-(** A mock coqtop launch, checking in particular that initial.coq is found *)
+(** Launch a coqtop with the user args in order to be sure that it works,
+    checking in particular that initial.coq is found *)
 val check_connection : string list -> unit
 
 (** * The structure describing a coqtop sub-process *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b884c5306..dc63de609 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1806,12 +1806,6 @@ let forbid_quit_to_save () =
 	else false)
 
 let main files =
-  (* Statup preferences *)
-  begin
-    try load_pref ()
-    with e ->
-      flash_info ("Could not load preferences ("^Printexc.to_string e^").");
-  end;
 
   (* Main window *)
   let w = GWindow.window
@@ -2946,32 +2940,22 @@ let rec check_for_geoproof_input () =
     in the path. Note that the -coqtop option to coqide allows to override
     this default coqtop path *)
 
-let default_coqtop_path () =
-  let prog = Sys.executable_name in
-  try
-    let pos = String.length prog - 6 in
-    let i = Str.search_backward (Str.regexp_string "coqide") prog pos in
-    String.blit "coqtop" 0 prog i 6;
-    prog
-  with _ -> "coqtop"
-
 let read_coqide_args argv =
   let rec filter_coqtop coqtop project_files out = function
     | "-coqtop" :: prog :: args ->
-      if coqtop = "" then filter_coqtop prog project_files out args
+      if coqtop = None then filter_coqtop (Some prog) project_files out args
       else
-	(output_string stderr "Error: multiple -coqtop options"; exit 1)
+       (output_string stderr "Error: multiple -coqtop options"; exit 1)
     | "-f" :: file :: args ->
 	filter_coqtop coqtop
 	  ((Minilib.canonical_path_name (Filename.dirname file),
 	    Project_file.read_project_file file) :: project_files) out args
     | "-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1
     | arg::args -> filter_coqtop coqtop project_files (arg::out) args
-    | [] -> ((if coqtop = "" then default_coqtop_path () else coqtop),
-	     List.rev project_files,List.rev out)
+    | [] -> (coqtop,List.rev project_files,List.rev out)
   in
-  let coqtop,project_files,argv = filter_coqtop "" [] [] argv in
-    Minilib.coqtop_path := coqtop;
+  let coqtop,project_files,argv = filter_coqtop None [] [] argv in
+    Ideutils.custom_coqtop := coqtop;
     custom_project_files := project_files;
   argv
 
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 3fec06313..5c6034d5c 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -65,12 +65,6 @@ let () =
 END
 
 let () =
-  let argl = Array.to_list Sys.argv in
-  let argl = Coqide.read_coqide_args argl in
-  let files = Coqide.process_argv argl in
-  let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
-  Coq.check_connection args;
-  Coqide.sup_args := args;
   Coqide.ignore_break ();
   (try
      let gtkrcdir = List.find
@@ -78,6 +72,12 @@ let () =
        Minilib.xdg_config_dirs in
      GtkMain.Rc.add_default_file (Filename.concat gtkrcdir "coqide-gtk2rc");
    with Not_found -> ());
+  (* Statup preferences *)
+  begin
+    try Preferences.load_pref ()
+    with e ->
+      Ideutils.flash_info ("Could not load preferences ("^Printexc.to_string e^").");
+  end;
   ignore (GtkMain.Main.init ());
   initmac () ;
 (*    GtkData.AccelGroup.set_default_mod_mask
@@ -89,7 +89,13 @@ let () =
 		  if level land Glib.Message.log_level `WARNING <> 0
 		  then Printf.eprintf "Warning: %s\n" msg
 		  else failwith ("Coqide internal error: " ^ msg)));
-    Coqide.main files;
+  let argl = Array.to_list Sys.argv in
+  let argl = Coqide.read_coqide_args argl in
+  let files = Coqide.process_argv argl in
+  let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
+  Coq.check_connection args;
+  Coqide.sup_args := args;
+  Coqide.main files;
     if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ());
     macready (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar") (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")
              (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help/Abt");
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index db7dcc9f5..ea15bd5f8 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -252,6 +252,24 @@ let stock_to_widget ?(size=`DIALOG) s =
   in img#set_stock s;
   img#coerce
 
+let custom_coqtop = ref None
+
+let coqtop_path () =
+  let file = match !custom_coqtop with
+    | Some s -> s
+    | None ->
+      match !current.cmd_coqtop with
+	| Some s -> s
+	| None ->
+	  let prog = String.copy Sys.executable_name in
+	  try
+	    let pos = String.length prog - 6 in
+	    let i = Str.search_backward (Str.regexp_string "coqide") prog pos in
+	    String.blit "coqtop" 0 prog i 6;
+	    prog
+	  with Not_found -> "coqtop"
+  in file
+
 let rec print_list print fmt = function
   | [] -> ()
   | [x] -> print fmt x
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 1e29d323c..91681d297 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,6 +52,12 @@ val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
 
 val run_command : (string -> unit) -> string -> Unix.process_status*string
 
+val custom_coqtop : string option ref
+(* @return command to call coqtop
+   - custom_coqtop if set
+   - from the prefs is set
+   - try to infer it else *)
+val coqtop_path : unit -> string
 
 
 val status : GMisc.statusbar
diff --git a/ide/preferences.ml b/ide/preferences.ml
index b3804003e..d2a4b291d 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -43,8 +43,8 @@ let project_behavior_of_string s =
 type inputenc = Elocale | Eutf8 | Emanual of string
 
 let string_of_inputenc = function
-  |Elocale -> "UTF-8"
-  |Eutf8 -> "LOCALE"
+  |Elocale -> "LOCALE"
+  |Eutf8 -> "UTF-8"
   |Emanual s -> s
 
 let inputenc_of_string s =
@@ -54,6 +54,7 @@ let inputenc_of_string s =
 
 type pref =
     {
+      mutable cmd_coqtop : string option;
       mutable cmd_coqc : string;
       mutable cmd_make : string;
       mutable cmd_coqmakefile : string;
@@ -113,6 +114,7 @@ let use_default_doc_url = "(automatic)"
 
 let (current:pref ref) =
   ref {
+    cmd_coqtop = None;
     cmd_coqc = "coqc";
     cmd_make = "make";
     cmd_coqmakefile = "coq_makefile -o makefile *.v";
@@ -196,6 +198,7 @@ let save_pref () =
     let add = Minilib.Stringmap.add in
     let (++) x f = f x in
     Minilib.Stringmap.empty ++
+    add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++
     add "cmd_coqc" [p.cmd_coqc] ++
     add "cmd_make" [p.cmd_make] ++
     add "cmd_coqmakefile" [p.cmd_coqmakefile] ++
@@ -260,6 +263,8 @@ let load_pref () =
     let set_command_with_pair_compat k f =
       set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit)
     in
+    let set_option k f = set k (fun v -> f (match v with |[] -> None |h::_ ->  Some h)) in
+    set_option "cmd_coqtop" (fun v -> np.cmd_coqtop <- v);
     set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v);
     set_hd "cmd_make" (fun v -> np.cmd_make <- v);
     set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v);
@@ -321,6 +326,10 @@ let load_pref () =
 *)
 
 let configure ?(apply=(fun () -> ())) () =
+  let cmd_coqtop =
+    string
+      ~f:(fun s -> !current.cmd_coqtop <- if s = "AUTO" then None else Some s)
+      "       coqtop" (match !current.cmd_coqtop with |None -> "AUTO" | Some x -> x) in
   let cmd_coqc =
     string
       ~f:(fun s -> !current.cmd_coqc <- s)
@@ -675,9 +684,8 @@ let configure ?(apply=(fun () -> ())) () =
 	     config_appearance);
 *)
      Section("Externals", None,
-	     [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;
-	      cmd_editor;
-	      cmd_browse;doc_url;library_url]);
+	     [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
+	      cmd_print;cmd_editor;cmd_browse;doc_url;library_url]);
      Section("Tactics Wizard", None,
 	     [automatic_tactics]);
      Section("Shortcuts", Some `PREFERENCES,
diff --git a/ide/preferences.mli b/ide/preferences.mli
index d4eb370f3..d862979fe 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -11,6 +11,7 @@ type inputenc = Elocale | Eutf8 | Emanual of string
 
 type pref =
     {
+      mutable cmd_coqtop : string option;
       mutable cmd_coqc : string;
       mutable cmd_make : string;
       mutable cmd_coqmakefile : string;