gconfig.mli 4.54 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
MARCHE Claude's avatar
MARCHE Claude committed
8 9 10 11 12 13 14 15 16 17 18 19
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
20

21
open Why3
22 23
open Whyconf

24
type t =
MARCHE Claude's avatar
MARCHE Claude committed
25 26 27
    { mutable window_width : int;
      mutable window_height : int;
      mutable tree_width : int;
28
      mutable task_height : int;
MARCHE Claude's avatar
MARCHE Claude committed
29
      mutable verbose : int;
30
      mutable default_editor : string;
31
      mutable intro_premises : bool;
MARCHE Claude's avatar
MARCHE Claude committed
32
      mutable show_labels : bool;
33
      mutable show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
34
      mutable show_time_limit : bool;
35
      mutable saving_policy : int;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
36 37
      mutable premise_color : string;
      mutable goal_color : string;
38
      mutable error_color : string;
MARCHE Claude's avatar
MARCHE Claude committed
39
      mutable iconset : string;
40
      mutable env : Why3.Env.env;
41
      mutable config : Whyconf.config;
42
      original_config : Whyconf.config;
43
      (* mutable altern_provers : prover option Mprover.t; *)
44
      (* mutable replace_prover : conf_replace_prover; *)
45
      mutable hidden_provers : string list;
46 47 48
      mutable session_time_limit : int;
      mutable session_mem_limit : int;
      mutable session_nb_processes : int;
MARCHE Claude's avatar
MARCHE Claude committed
49 50
    }

51
val read_config : string option -> string list -> unit
52 53
(** None use the default config *)

54 55
val init : unit -> unit

56
val save_config : unit -> unit
MARCHE Claude's avatar
MARCHE Claude committed
57

58 59 60
val config : unit -> t
(** [config ()] raise [invalid_arg "configuration not yet loaded"]
    if load_config is not called *)
61 62

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

MARCHE Claude's avatar
MARCHE Claude committed
64 65 66 67 68
(*****************)
(* images, icons *)
(*****************)

val why_icon : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
69 70 71 72 73

val image_yes : GdkPixbuf.pixbuf ref

(* tree object icons *)
val image_file : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
74 75
val image_theory : GdkPixbuf.pixbuf ref
val image_goal : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
76 77
val image_prover : GdkPixbuf.pixbuf ref
val image_transf : GdkPixbuf.pixbuf ref
François Bobot's avatar
François Bobot committed
78
val image_metas  : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
79
val image_editor : GdkPixbuf.pixbuf ref
80
val image_replay : GdkPixbuf.pixbuf ref
81
val image_cancel : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
82
val image_reload : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
merge  
MARCHE Claude committed
83
val image_remove : GdkPixbuf.pixbuf ref
84
val image_cleaning : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
85 86

(* status icons *)
MARCHE Claude's avatar
MARCHE Claude committed
87
val image_undone : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
88 89 90
val image_scheduled : GdkPixbuf.pixbuf ref
val image_running : GdkPixbuf.pixbuf ref
val image_valid : GdkPixbuf.pixbuf ref
91
val image_invalid : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
92
val image_timeout : GdkPixbuf.pixbuf ref
93
val image_outofmemory : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
94 95
val image_unknown : GdkPixbuf.pixbuf ref
val image_failure : GdkPixbuf.pixbuf ref
96
val image_valid_obs : GdkPixbuf.pixbuf ref
97
val image_invalid_obs : GdkPixbuf.pixbuf ref
98
val image_timeout_obs : GdkPixbuf.pixbuf ref
99
val image_outofmemory_obs : GdkPixbuf.pixbuf ref
100 101
val image_unknown_obs : GdkPixbuf.pixbuf ref
val image_failure_obs : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
102 103 104 105 106 107 108

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

val show_legend_window : unit -> unit
val show_about_window : unit -> unit
109
val preferences : t -> unit
110 111 112 113 114

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

(*
115 116
val unknown_prover :
  t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover option
117
*)
MARCHE Claude's avatar
MARCHE Claude committed
118

119
(* obsolete dialog
120 121
val replace_prover :
  t -> 'key Session.proof_attempt -> 'key Session.proof_attempt -> bool
122
*)
MARCHE Claude's avatar
MARCHE Claude committed
123 124


MARCHE Claude's avatar
MARCHE Claude committed
125
(*
126
Local Variables:
127
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
128
End:
MARCHE Claude's avatar
MARCHE Claude committed
129
*)