Commit d22586e2 authored by François Bobot's avatar François Bobot

whyconf : mli doc rearrangment

Conflicts:

	src/driver/whyconf.mli
parent e35119d5
......@@ -21,28 +21,7 @@
open Util
type config_prover = {
name : string; (* "Alt-Ergo v2.95 (special)" *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string; (* Interative theorem prover *)
}
type main
val libdir: main -> string
val datadir: main -> string
val loadpath: main -> string list
val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
val set_limits: main -> int -> int -> int -> main
val plugins : main -> string list
val pluginsdir : main -> string
val set_plugins : main -> string list -> main
val add_plugin : main -> string -> main
val load_plugins : main -> unit
(** {2 General configuration} *)
type config
(** A configuration linked to an rc file. Whyconf gives access to
......@@ -69,25 +48,55 @@ val default_config : string -> config
(** [ default_config filename ] create a default configuration which is going
to be saved in [ filename ]*)
val get_conf_file : config -> string
(** [get_conf_file config] get the rc file corresponding to this
configuration *)
(* val set_conf_file : config -> string -> config *)
(* (\** [set_conf_file config] set the rc file corresponding to this *)
(* configuration *\) *)
(** {2 Main section} *)
type main
val get_main : config -> main
(** [get_main config] get the main section stored in the Rc file *)
val set_main : config -> main -> config
(** [set_main config main] replace the main section by the given one *)
val libdir: main -> string
val datadir: main -> string
val loadpath: main -> string list
val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
val set_limits: main -> int -> int -> int -> main
val plugins : main -> string list
val pluginsdir : main -> string
val set_plugins : main -> string list -> main
val add_plugin : main -> string -> main
val load_plugins : main -> unit
(** {2 Provers} *)
type config_prover = {
name : string; (* "Alt-Ergo v2.95 (special)" *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string; (* Interative theorem prover *)
}
val get_provers : config -> config_prover Mstr.t
(** [get_main config] get the prover family stored in the Rc file. The
keys are the unique ids of the prover (argument of the family) *)
val set_main : config -> main -> config
(** [set_main config main] replace the main section by the given one *)
val set_provers : config -> config_prover Mstr.t -> config
(** [set_provers config provers] replace all the family prover by the
one given *)
val get_conf_file : config -> string
(** [get_conf_file config] get the rc file corresponding to this
configuration *)
(* val set_conf_file : config -> string -> config *)
(* (\** [set_conf_file config] set the rc file corresponding to this *)
(* configuration *\) *)
(** Access to the Rc.t *)
val get_section : config -> string -> Rc.section option
(** [get_section config name] Same as {!Rc.get_section} except name
......
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