Commit e41a8a2d authored by MARCHE Claude's avatar MARCHE Claude
Browse files

option -I pour whyide

parent b78a1e58
......@@ -27,7 +27,7 @@ type t =
mutable max_running_processes : int;
mutable provers : prover_data list;
mutable default_editor : string;
env : Env.env;
mutable env : Env.env;
mutable config : Whyconf.config;
}
......@@ -87,8 +87,14 @@ let load_config config =
let ide = match get_section config "ide" with
| None -> default_ide
| Some s -> load_ide s in
(*
let provers = get_provers config in
*)
(*
let env = Env.create_env (Lexer.retrieve main.loadpath) in
*)
(* temporary sets env to empty *)
let env = Env.create_env (Lexer.retrieve []) in
{ window_height = ide.ide_window_height;
window_width = ide.ide_window_width;
tree_width = ide.ide_tree_width;
......@@ -97,7 +103,10 @@ let load_config config =
mem_limit = main.Whyconf.memlimit;
verbose = ide.ide_verbose;
max_running_processes = main.Whyconf.running_provers_max;
(*
provers = Mstr.fold (get_prover_data env) provers [];
*)
provers = [];
default_editor = ide.ide_default_editor;
config = config;
env = env
......
......@@ -22,10 +22,14 @@ type t =
mutable max_running_processes : int;
mutable provers : prover_data list;
mutable default_editor : string;
env : Why.Env.env;
mutable env : Why.Env.env;
mutable config : Whyconf.config;
}
val get_prover_data : Why.Env.env ->
string ->
Why.Whyconf.config_prover -> prover_data list -> prover_data list
val save_config : unit -> unit
val config : t
......
......@@ -29,7 +29,10 @@ open Gconfig
(* parsing comand_line *)
(***************************)
let spec = [
let includes = ref []
let spec = Arg.align [
"-I", Arg.String (fun s -> includes := s :: !includes), "<s> add s to loadpath" ;
]
let usage_str = "whyide [options] <file>.why"
......@@ -80,7 +83,13 @@ let source_text fname =
(* loading WhyIDE configuration *)
(********************************)
let gconfig = Gconfig.config
let gconfig =
let c = Gconfig.config in
let loadpath = (get_main ()).loadpath @ List.rev !includes in
c.env <- Env.create_env (Lexer.retrieve loadpath);
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <- Util.Mstr.fold (Gconfig.get_prover_data c.env) provers [];
c
(***********************)
(* Parsing input file *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment