ide : add options -L, --loadpath, -C, --config

src/ide/gconfig.ml

@@ -155,14 +155,6 @@ let load_config config =
     env            = env
   }
 
-let read_config () =
-  try
-    let config = Whyconf.read_config None in
-    load_config config
-  with e when not (Debug.test_flag Debug.stack_trace) ->
-    eprintf "@.%a@." Exn_printer.exn_printer e;
-    exit 1
-
 let save_config t =
   let _save_prover _ pr acc =
     Mstr.add pr.Session.prover_id
@@ -200,15 +192,29 @@ let save_config t =
 *)
   save_config config
 
-let config =
-  eprintf "[Info] reading IDE config file...@?";
-  let c = read_config () in
-  eprintf " done.@.";
-  c
+let read_config conf_file =
+  try
+    let config = Whyconf.read_config conf_file in
+    load_config config
+  with e when not (Debug.test_flag Debug.stack_trace) ->
+    eprintf "@.%a@." Exn_printer.exn_printer e;
+    exit 1
+
+let config,read_config =
+  let config = ref None in
+  (fun () ->
+    match !config with
+      | None -> invalid_arg "configuration not yet loaded"
+      | Some conf -> conf),
+  (fun conf_file ->
+    eprintf "[Info] reading IDE config file...@?";
+    let c = read_config conf_file in
+    eprintf " done.@.";
+    config := Some c)
 
-let save_config () = save_config config
+let save_config () = save_config (config ())
 
-let get_main () = (get_main config.config)
+let get_main () = (get_main (config ()).config)
 
 
 (*
@@ -254,7 +260,7 @@ let iconname_reload = "movefile32"
 let iconname_remove = "deletefile32"
 let iconname_cleaning = "trashb32"
 
-let image_default = ref (image ~size:20 iconname_default)
+let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ()) (** dumb pixbuf *)
 let image_undone = ref !image_default
 let image_scheduled = ref !image_default
 let image_running = ref !image_default
@@ -312,7 +318,7 @@ let resize_images size =
   image_cleaning := image ~size iconname_cleaning;
   ()
 
-let () =
+let init () =
   eprintf "[Info] reading icons...@?";
   why_icon := image "logo-why";
   resize_images 20;
@@ -563,12 +569,15 @@ let run_auto_detection gconfig =
   gconfig.config <- config;
   let _provers = get_provers config in
 (* TODO: store the result differently
-  gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers Mstr.empty
+  gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers
+  Mstr.empty
 *)
   ()
 *)
 
-let () = eprintf "[Info] end of configuration initialization@."
+(* let () = eprintf "[Info] end of configuration initialization@." *)
+
+let read_config conf_file = read_config conf_file; init ()
 
 (*
 Local Variables:

src/ide/gconfig.mli

@@ -40,9 +40,14 @@ type t =
       mutable config : Whyconf.config;
     }
 
+val read_config : string option -> unit
+(** None use the default config *)
+
 val save_config : unit -> unit
 
-val config : t
+val config : unit -> t
+(** [config ()] raise [invalid_arg "configuration not yet loaded"]
+    if load_config is not called *)
 
 val get_main : unit -> Whyconf.main
 

src/ide/gmain.ml

@@ -37,11 +37,22 @@ open Gconfig
 let includes = ref []
 let file = ref None
 let opt_version = ref false
+let opt_config = ref None
 
 let spec = Arg.align [
-  ("-I",
+  ("-L",
    Arg.String (fun s -> includes := s :: !includes),
    "<s> add s to loadpath") ;
+  ("--library",
+   Arg.String (fun s -> includes := s :: !includes),
+   " same as -L") ;
+  ("-I",
+   Arg.String (fun s -> includes := s :: !includes),
+   " same as -L (obsolete)") ;
+  "-C", Arg.String (fun s -> opt_config := Some s),
+      "<file> Read configuration from <file>";
+  "--config", Arg.String (fun s -> opt_config := Some s),
+      " same as -C";
 (*
   ("-f",
    Arg.String (fun s -> input_files := s :: !input_files),
@@ -73,6 +84,8 @@ let () =
     exit 0
   end
 
+let () = Gconfig.read_config !opt_config
+
 let fname = match !file with
   | None ->
       Arg.usage spec usage_str;
@@ -114,7 +127,7 @@ let source_text fname =
 (********************************)
 
 let gconfig =
-  let c = Gconfig.config in
+  let c = Gconfig.config () in
   let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
   c.env <- Env.create_env loadpath;
 (*
@@ -825,7 +838,7 @@ let exit_function ?(destroy=false) () =
   let ret = Sys.command "xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in
   if ret = 0 then eprintf "DTD validation succeeded, good!@.";
   *)
-  match config.saving_policy with
+  match (Gconfig.config ()).saving_policy with
     | 0 -> save_session (); GMain.quit ()
     | 1 -> GMain.quit ()
     | 2 ->
@@ -1530,7 +1543,7 @@ let select_row r =
   let a = get_any_from_row_reference r in
   match a with
     | M.Goal g ->
-        if config.intro_premises then
+        if (Gconfig.config ()).intro_premises then
           let callback = function
             | [t] -> display_task g t
             | _ -> assert false