gconfig.mli 3.6 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    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
19

MARCHE Claude's avatar
MARCHE Claude committed
20 21
open Why

22 23
type prover_data = Session.prover_data
(*
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27
    { prover_id : string;
      prover_name : string;
      prover_version : string;
      command : string;
28
      driver_name : string;
MARCHE Claude's avatar
MARCHE Claude committed
29
      driver : Driver.driver;
30
      mutable editor : string;
MARCHE Claude's avatar
MARCHE Claude committed
31
    }
32
*)
MARCHE Claude's avatar
MARCHE Claude committed
33

34
type t =
MARCHE Claude's avatar
MARCHE Claude committed
35 36 37
    { mutable window_width : int;
      mutable window_height : int;
      mutable tree_width : int;
38
      mutable task_height : int;
39
      mutable time_limit : int;
40
      mutable mem_limit : int;
MARCHE Claude's avatar
MARCHE Claude committed
41
      mutable verbose : int;
42
      mutable max_running_processes : int;
43
      mutable provers : prover_data Util.Mstr.t;
44
      mutable default_editor : string;
MARCHE Claude's avatar
MARCHE Claude committed
45
      mutable show_labels : bool;
MARCHE Claude's avatar
MARCHE Claude committed
46
      mutable env : Why.Env.env;
47
      mutable config : Whyconf.config;
MARCHE Claude's avatar
MARCHE Claude committed
48 49
    }

50
(*
51
val get_prover_data : Why.Env.env -> string ->
52
  Why.Whyconf.config_prover ->
53
  prover_data Why.Util.Mstr.t -> prover_data Why.Util.Mstr.t
54
*)
MARCHE Claude's avatar
MARCHE Claude committed
55

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

58
val config : t
59 60

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

MARCHE Claude's avatar
MARCHE Claude committed
62 63 64 65 66 67 68 69 70 71 72
(***************)
(* boomy icons *)
(***************)

val image_yes : GdkPixbuf.pixbuf ref

(* tree object icons *)
val image_directory : GdkPixbuf.pixbuf ref
val image_file : GdkPixbuf.pixbuf ref
val image_prover : GdkPixbuf.pixbuf ref
val image_transf : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
73
val image_editor : GdkPixbuf.pixbuf ref
74
val image_replay : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
merge  
MARCHE Claude committed
75
val image_remove : GdkPixbuf.pixbuf ref
76
val image_cleaning : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
77 78

(* status icons *)
MARCHE Claude's avatar
MARCHE Claude committed
79
val image_undone : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
80 81 82
val image_scheduled : GdkPixbuf.pixbuf ref
val image_running : GdkPixbuf.pixbuf ref
val image_valid : GdkPixbuf.pixbuf ref
83
val image_invalid : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
84 85 86
val image_timeout : GdkPixbuf.pixbuf ref
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 90 91
val image_timeout_obs : GdkPixbuf.pixbuf ref
val image_unknown_obs : GdkPixbuf.pixbuf ref
val image_failure_obs : GdkPixbuf.pixbuf ref
MARCHE Claude's avatar
MARCHE Claude committed
92 93 94 95 96 97 98

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

val show_legend_window : unit -> unit
val show_about_window : unit -> unit
99
val preferences : t -> unit
MARCHE Claude's avatar
MARCHE Claude committed
100

101
val run_auto_detection : t -> unit
MARCHE Claude's avatar
MARCHE Claude committed
102

MARCHE Claude's avatar
MARCHE Claude committed
103
(*
104
Local Variables:
105
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
106
End:
MARCHE Claude's avatar
MARCHE Claude committed
107
*)