Module Why3_session

module Why3_session: sig .. end
Not mutated after the creation

From the original file we kept only the reading of a session. We also discard all the information about how that have been proved (metas, transformation, proof_attempts) or the order of the goals


module S: Datatype.String
module Xml: Why3_xml
type goal = {
   goal_name : string;
   goal_parent : theory;
   mutable goal_verified : bool;
}
type theory = {
   theory_name : string;
   theory_parent : file;
   theory_goals : goal Datatype.String.Hashtbl.t;
   mutable theory_verified : bool;
}
type file = {
   file_name : string;
   file_format : string option;
   file_parent : session;
   file_theories : theory Datatype.String.Hashtbl.t; (*Not mutated after the creationNot mutated after the creation*)
   mutable file_verified : bool;
}
type session = {
   session_files : file Datatype.String.Hashtbl.t;
   session_dir : string;
}
val db_filename : string
2 Create a session
val session_dir_for_save : string Pervasives.ref
val empty_session : string -> session
val raw_add_no_task : theory -> S.Hashtbl.key -> goal
val raw_add_theory : file -> S.Hashtbl.key -> theory
val raw_add_file : session ->
S.Hashtbl.key -> string option -> file
exception LoadError

Read/Write


val bool_attribute : string -> Xml.element -> bool -> bool
val int_attribute_def : string -> Xml.element -> int -> int
val int_attribute : string -> Xml.element -> int
val string_attribute_def : string -> Xml.element -> string -> string
val string_attribute : string -> Xml.element -> string
val load_option : string -> Xml.element -> string option
val load_ident : Xml.element -> string
val load_goal : theory -> Xml.element -> unit
val load_theory : file -> Xml.element -> unit
val load_file : session -> Xml.element -> unit
val load_session : session -> Xml.element -> unit
type notask = unit 
val read_session : string -> session
Read a session stored on the disk. It returns a session without any task attached to goals