Commit 91d0b149 authored by François Bobot's avatar François Bobot

whyconf : libdir, datadir, loadpath, ... are not written in why.conf

   if they correspond to the default value.

   But the problem for drivers remain.
parent e245c1e9
......@@ -7,9 +7,12 @@
* fix problems with .why.conf
** if we distribute the current state, users who already have a ~/.why.conf
will get a error message because of missing loadpath to modules
Done? - the magic number will force to not use the old ~/.why.conf of
the user
** generally speaking, we should rethink the design of that .why.conf: avoid
absolute paths,
Partially done - libdir, datadir, loadpath, ... are not written in why.conf
if they correspond to the default value.
* proof replay
** in IDE: replay all obsolete but previously successful proofs
** in whybench
......
......@@ -142,9 +142,12 @@ let default_main =
let set_main rc main =
let section = empty_section in
let section = set_int section "magicnumber" magicnumber in
let section = set_string section "libdir" main.private_libdir in
let section = set_string section "datadir" main.private_datadir in
let section = set_stringl section "loadpath" main.loadpath in
let section = set_string ~default:default_main.private_libdir
section "libdir" main.private_libdir in
let section = set_string ~default:default_main.private_datadir
section "datadir" main.private_datadir in
let section = set_stringl ~default:default_main.loadpath
section "loadpath" main.loadpath in
let section = set_int section "timelimit" main.timelimit in
let section = set_int section "memlimit" main.memlimit in
let section =
......
......@@ -116,15 +116,16 @@ val get_intl : ?default:int list -> section -> string -> int list
associated to [key]
*)
val set_int : section -> string -> int -> section
(** [set_int section key value] add the association [key] to [value]
in the section. Remove all former associations with this [key]
val set_int :?default:int -> section -> string -> int -> section
(** [set_int ?default section key value] add the association [key] to [value]
in the section if value is not default.
Remove all former associations with this [key]
*)
val set_intl : section -> string -> int list -> section
(** [set_int section key lvalue] add the associations [key] to all the
[lvalue] in the section. Remove all former associations with this
[key]
val set_intl : ?default:int list -> section -> string -> int list -> section
(** [set_int ?default section key lvalue] add the associations [key] to all the
[lvalue] in the section if value is not default.
Remove all former associations with this [key]
*)
val get_bool : ?default:bool -> section -> string -> bool
......@@ -135,10 +136,10 @@ val get_booll : ?default:bool list -> section -> string -> bool list
val get_boolo : section -> string -> bool option
val set_bool : section -> string -> bool -> section
val set_bool : ?default:bool -> section -> string -> bool -> section
(** Same as {!set_int} but on bool *)
val set_booll : section -> string -> bool list -> section
val set_booll : ?default:bool list -> section -> string -> bool list -> section
(** Same as {!set_intl} but on bool *)
......@@ -150,10 +151,11 @@ val get_stringl : ?default:string list -> section -> string -> string list
val get_stringo : section -> string -> string option
val set_string : section -> string -> string -> section
val set_string : ?default:string -> section -> string -> string -> section
(** Same as {!set_int} but on string *)
val set_stringl : section -> string -> string list -> section
val set_stringl : ?default:string list ->
section -> string -> string list -> section
(** Same as {!set_intl} but on string *)
(* val ident : ?default:string -> section -> string -> string *)
......
......@@ -177,12 +177,22 @@ let get_valuel read ?default section key =
| None -> raise (MissingField key)
| Some v -> v
let set_value write section key value =
Mstr.add key [write value] section
let set_valuel write section key valuel =
let set_value write ?default section key value =
let actually_write = match default with
| None -> true
| Some default -> default <> value in
if actually_write
then Mstr.add key [write value] section
else section
let set_valuel write ?default section key valuel =
if valuel = [] then Mstr.remove key section else
Mstr.add key (List.map write valuel) section
let actually_write = match default with
| None -> true
| Some default -> default <> valuel in
if actually_write
then Mstr.add key (List.map write valuel) section
else Mstr.remove key section
let rint k = function
| RCint n -> n
......
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