Mentions légales du service

Skip to content
Snippets Groups Projects
Commit e3f2cb50 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Recovered remove_subtree. Easier to use Why3's API with this in

controller.
parent 8c747092
No related branches found
No related tags found
1 merge request!2Isabelle configure realization1
...@@ -90,6 +90,7 @@ let create_controller config env ses = ...@@ -90,6 +90,7 @@ let create_controller config env ses =
provers; provers;
c c
let remove_subtree = Session_itp.remove_subtree
(* Get children of any without proofattempts *) (* Get children of any without proofattempts *)
let get_undetached_children_no_pa s any : any list = let get_undetached_children_no_pa s any : any list =
......
...@@ -131,6 +131,10 @@ val add_file : controller -> ?format:Env.fformat -> string -> unit ...@@ -131,6 +131,10 @@ val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_fil cont ?fmt fname] parses the source file (** [add_fil cont ?fmt fname] parses the source file
[fname] and add the resulting theories to the session of [cont] *) [fname] and add the resulting theories to the session of [cont] *)
val remove_subtree: controller -> any -> removed:notifier ->
notification:notifier -> unit
(** Mapping to Session_itp.remove_subtree. Used for code using Why3's API *)
val get_undetached_children_no_pa: Session_itp.session -> any -> any list val get_undetached_children_no_pa: Session_itp.session -> any -> any list
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment