Commit bd4c34c0 authored by Clément Fumex's avatar Clément Fumex

first working version of save_session; still missing transformation's arguments

parent 8f1f33b5
......@@ -60,7 +60,7 @@ let provers =
eprintf "Failed to load driver for %s %s: %a@."
p.Whyconf.prover_name p.Whyconf.prover_version
Exn_printer.exn_printer e;
exit 1)
acc)
provers
[]
......@@ -78,7 +78,7 @@ let alt_ergo : Whyconf.config_prover =
(** Testing Session_itp *)
let (s,b) = Session_itp.load_session "../bitwalker/why3session.xml"
let s = Session_itp.load_session "../bitwalker/why3session.xml"
let id =
match Session_itp.get_theories s with
......@@ -94,7 +94,16 @@ let () =
printf "%a@." (Session_itp.print_tree s) (Session_itp.get_tree s id)
(** Testing Controller_itp *)
let () = Session_itp.save_session "../bitwalker/testsession.xml" s
let s' = Session_itp.load_session "../bitwalker/testsession.xml"
let id' =
match Session_itp.get_theories s' with
| (n, (thn, _::_::x::_)::_)::_ -> x
| _ -> assert false
let () =
printf "%a@." (Session_itp.print_tree s') (Session_itp.get_tree s' id')
(** testing Controller_itp *)
let my_session = Session_itp.empty_session ()
......
This diff is collapsed.
......@@ -80,12 +80,11 @@ val remove_proof_attempt : session -> proofNodeID -> Whyconf.prover -> unit
val remove_transformation : session -> transID -> unit
(** [remove_transformation s id] removes the transformation [id]
from the session [s] *)
(*
val save_session : string -> session -> unit
*)
(** [save_session f s] Save the session [s] in file [f] *)
val load_session : string -> session * bool
val load_session : string -> session
(** [load_session f] load a session from a file [f]; all the tasks are
initialised to None *)
......
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