itp_server.mli 1.5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
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.                           *)
(*                                                                  *)
(********************************************************************)
11

12 13
(** Server for a client/server communication with an external graphical interface *)

14
open Itp_communication
Clément Fumex's avatar
Clément Fumex committed
15

16
(* The server part of the protocol *)
Clément Fumex's avatar
Clément Fumex committed
17 18
module type Protocol = sig

Clément Fumex's avatar
Clément Fumex committed
19 20
  val get_requests : unit -> ide_request list
  val notify : notification -> unit
Clément Fumex's avatar
Clément Fumex committed
21 22 23

end

24
module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig
25

26 27 28 29
  (* This function is used to change the registered function for
     focus_on_loading. It focuses on the first goal that satisfies the given
     predicate. *)
  val focus_on_loading: (Task.task -> bool) -> unit
30

31 32 33 34 35
  (* Initialize server with the given config, env and filename for the session.
     If send_source is set to true the source mlw files will be sent to the ide
     as notifications. *)
  val init_server:
      ?send_source:bool -> Whyconf.config -> Env.env -> string -> unit
36 37

end