Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

gconfig.mli 3.83 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

12
open Why3
13

14
type t =
MARCHE Claude's avatar
MARCHE Claude committed
15 16 17
    { mutable window_width : int;
      mutable window_height : int;
      mutable tree_width : int;
18
      mutable task_height : int;
MARCHE Claude's avatar
MARCHE Claude committed
19
      mutable verbose : int;
20
      mutable default_prover : string;
21
      mutable default_editor : string;
22
      mutable intro_premises : bool;
MARCHE Claude's avatar
MARCHE Claude committed
23
      mutable show_labels : bool;
24
      mutable show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
25
      mutable show_time_limit : bool;
26
      mutable saving_policy : int;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
27 28
      mutable premise_color : string;
      mutable goal_color : string;
29
      mutable error_color : string;
MARCHE Claude's avatar
MARCHE Claude committed
30
      mutable iconset : string;
31
      mutable env : Why3.Env.env;
32
      mutable config : Whyconf.config;
33
      original_config : Whyconf.config;
34
      (* mutable altern_provers : prover option Mprover.t; *)
35
      (* mutable replace_prover : conf_replace_prover; *)
36
      mutable hidden_provers : string list;
37 38 39
      mutable session_time_limit : int;
      mutable session_mem_limit : int;
      mutable session_nb_processes : int;
MARCHE Claude's avatar
MARCHE Claude committed
40 41
    }

42
val read_config : string option -> string list -> unit
43 44
(** None use the default config *)

45 46
val init : unit -> unit

47
val save_config : unit -> unit
MARCHE Claude's avatar
MARCHE Claude committed
48

49 50 51
val config : unit -> t
(** [config ()] raise [invalid_arg "configuration not yet loaded"]
    if load_config is not called *)
52 53

val get_main : unit -> Whyconf.main
MARCHE Claude's avatar
MARCHE Claude committed
54

MARCHE Claude's avatar
MARCHE Claude committed
55 56 57 58 59
(*****************)
(* images, icons *)
(*****************)

val why_icon : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
60 61 62 63 64

val image_yes : GdkPixbuf.pixbuf ref

(* tree object icons *)
val image_file : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
65 66
val image_theory : GdkPixbuf.pixbuf ref
val image_goal : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
67 68
val image_prover : GdkPixbuf.pixbuf ref
val image_transf : GdkPixbuf.pixbuf ref
François Bobot's avatar
François Bobot committed
69
val image_metas  : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
70
val image_editor : GdkPixbuf.pixbuf ref
71
val image_replay : GdkPixbuf.pixbuf ref
72
val image_cancel : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
73
val image_reload : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
merge  
MARCHE Claude committed
74
val image_remove : GdkPixbuf.pixbuf ref
75
val image_cleaning : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
76 77

(* status icons *)
MARCHE Claude's avatar
MARCHE Claude committed
78
val image_undone : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
79 80 81
val image_scheduled : GdkPixbuf.pixbuf ref
val image_running : GdkPixbuf.pixbuf ref
val image_valid : GdkPixbuf.pixbuf ref
82
val image_invalid : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
83
val image_timeout : GdkPixbuf.pixbuf ref
84
val image_outofmemory : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
85 86
val image_unknown : GdkPixbuf.pixbuf ref
val image_failure : GdkPixbuf.pixbuf ref
87
val image_valid_obs : GdkPixbuf.pixbuf ref
88
val image_invalid_obs : GdkPixbuf.pixbuf ref
89
val image_timeout_obs : GdkPixbuf.pixbuf ref
90
val image_outofmemory_obs : GdkPixbuf.pixbuf ref
91 92
val image_unknown_obs : GdkPixbuf.pixbuf ref
val image_failure_obs : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
93 94 95 96 97 98 99

(*************************)
(* miscellaneous dialogs *)
(*************************)

val show_legend_window : unit -> unit
val show_about_window : unit -> unit
100
val preferences : t -> unit
101 102 103 104 105

val uninstalled_prover :
  t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover_upgrade_policy

(*
106 107
val unknown_prover :
  t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover option
108
*)
MARCHE Claude's avatar
MARCHE Claude committed
109

110
(* obsolete dialog
111 112
val replace_prover :
  t -> 'key Session.proof_attempt -> 'key Session.proof_attempt -> bool
113
*)
MARCHE Claude's avatar
MARCHE Claude committed
114 115


MARCHE Claude's avatar
MARCHE Claude committed
116
(*
117
Local Variables:
118
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
119
End:
MARCHE Claude's avatar
MARCHE Claude committed
120
*)