Commit 7ea0162a authored by MARCHE Claude's avatar MARCHE Claude

ITP server takes scheduler as argument

parent ee0cf016
......@@ -69,20 +69,19 @@ type request_type =
type ide_request = request_type * node_ID
open Unix_scheduler
open Session_itp
open Controller_itp
open Session_user_interface
open Stdlib
module C = Controller_itp.Make(Unix_Scheduler)
module type Protocol = sig
val get_requests : unit -> ide_request list
val notify : notification -> unit
end
module Make (P:Protocol) = struct
module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
module C = Controller_itp.Make(S)
let debug = Debug.lookup_flag "ide_info" (* TODO register itp_server *)
......@@ -507,7 +506,7 @@ exception Bad_prover_name of prover
List.iter treat_request (P.get_requests ());
true
let _ = Unix_Scheduler.idle ~prio:1 treat_requests
let _ = S.idle ~prio:1 treat_requests
end
......@@ -38,13 +38,21 @@ type error_notification =
type notification =
| Node_change of node_ID * node_info
(* inform that the data of the given node changed *)
| New_subtree of node_ID * session_tree
(* the given node has a new child whose contents is the given tree *)
| Remove of node_ID
(* the given node was removed *)
| Initialized of infos * prover list * transformation list * strategy list
(* initial global data *)
| Saved
(* the session was saved on disk *)
| Session_Tree of session_tree
(* the full session tree is sent *)
| Error of error_notification
(* an error occured *)
| Message of string
(* an informative message *)
type request_type =
| Command of string
......@@ -68,8 +76,10 @@ module type Protocol = sig
end
module Make (P:Protocol) : sig
module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig
val treat_requests: unit -> bool
val get_config: unit -> Whyconf.config
(* Nothing ! *)
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment