gconfig.mli 4.63 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

12
open Why3
Sylvain Dailler's avatar
Sylvain Dailler committed
13
open Itp_server
14

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

Sylvain Dailler's avatar
Sylvain Dailler committed
47
val load_config : infos -> t
48
(** [load_config config original_config env] creates and saves IDE config *)
49

Sylvain Dailler's avatar
Sylvain Dailler committed
50 51
val default_config: t
(** Used as an empty initial config. Should be removed TODO *)
52

Sylvain Dailler's avatar
Sylvain Dailler committed
53 54 55
val init : t -> string -> unit

(*
56
val save_config : unit -> unit
Sylvain Dailler's avatar
Sylvain Dailler committed
57
*)
MARCHE Claude's avatar
MARCHE Claude committed
58

Sylvain Dailler's avatar
Sylvain Dailler committed
59
val config : t -> t -> unit
60 61
(** [config ()] raise [invalid_arg "configuration not yet loaded"]
    if load_config is not called *)
62

Sylvain Dailler's avatar
Sylvain Dailler committed
63
(* val get_main : unit -> Whyconf.main *)
MARCHE Claude's avatar
MARCHE Claude committed
64

MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68 69 70
(*******************)
(*   font size     *)
(*******************)

val add_modifiable_sans_font_view : GObj.misc_ops -> unit
val add_modifiable_mono_font_view : GObj.misc_ops -> unit
Sylvain Dailler's avatar
Sylvain Dailler committed
71 72 73
val enlarge_fonts : t -> unit
val reduce_fonts : t -> unit
val set_fonts : t -> unit
74

MARCHE Claude's avatar
MARCHE Claude committed
75 76 77 78 79
(*****************)
(* images, icons *)
(*****************)

val why_icon : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
80 81 82 83 84

val image_yes : GdkPixbuf.pixbuf ref

(* tree object icons *)
val image_file : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
85 86
val image_theory : GdkPixbuf.pixbuf ref
val image_goal : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
87 88
val image_prover : GdkPixbuf.pixbuf ref
val image_transf : GdkPixbuf.pixbuf ref
François Bobot's avatar
François Bobot committed
89
val image_metas  : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
90
val image_editor : GdkPixbuf.pixbuf ref
91
val image_replay : GdkPixbuf.pixbuf ref
92
val image_cancel : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
93
val image_reload : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
merge  
MARCHE Claude committed
94
val image_remove : GdkPixbuf.pixbuf ref
95
val image_cleaning : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
96 97

(* status icons *)
MARCHE Claude's avatar
MARCHE Claude committed
98
val image_undone : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
99 100 101
val image_scheduled : GdkPixbuf.pixbuf ref
val image_running : GdkPixbuf.pixbuf ref
val image_valid : GdkPixbuf.pixbuf ref
102
val image_invalid : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
103
val image_timeout : GdkPixbuf.pixbuf ref
104
val image_outofmemory : GdkPixbuf.pixbuf ref
105
val image_steplimitexceeded : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
106 107
val image_unknown : GdkPixbuf.pixbuf ref
val image_failure : GdkPixbuf.pixbuf ref
108
val image_valid_obs : GdkPixbuf.pixbuf ref
109
val image_invalid_obs : GdkPixbuf.pixbuf ref
110
val image_timeout_obs : GdkPixbuf.pixbuf ref
111
val image_outofmemory_obs : GdkPixbuf.pixbuf ref
112
val image_steplimitexceeded_obs : GdkPixbuf.pixbuf ref
113 114
val image_unknown_obs : GdkPixbuf.pixbuf ref
val image_failure_obs : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
115 116 117 118 119 120 121

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

val show_legend_window : unit -> unit
val show_about_window : unit -> unit
Sylvain Dailler's avatar
Sylvain Dailler committed
122 123 124 125 126
(* TODO
val preferences : string ->
           Why3.Whyconf.config_prover Why3.Whyconf.Mprover.t ->
           Why3.Whyconf.config_editor Why3.Whyconf.Meditor.t -> t -> unit
*)
127

Sylvain Dailler's avatar
Sylvain Dailler committed
128
(*
129 130
val uninstalled_prover :
  t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover_upgrade_policy
Sylvain Dailler's avatar
Sylvain Dailler committed
131
*)
132 133

(*
134 135
val unknown_prover :
  t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover option
136
*)
MARCHE Claude's avatar
MARCHE Claude committed
137

138
(* obsolete dialog
139 140
val replace_prover :
  t -> 'key Session.proof_attempt -> 'key Session.proof_attempt -> bool
141
*)
MARCHE Claude's avatar
MARCHE Claude committed
142 143


MARCHE Claude's avatar
MARCHE Claude committed
144
(*
145
Local Variables:
146
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
147
End:
MARCHE Claude's avatar
MARCHE Claude committed
148
*)