Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
f5efdfc0
Commit
f5efdfc0
authored
Jan 03, 2012
by
François Bobot
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
documentation spellchecking
parent
96b4c615
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
9 additions
and
26 deletions
+9
-26
src/session/session.mli
src/session/session.mli
+6
-6
src/session/session_scheduler.mli
src/session/session_scheduler.mli
+2
-19
src/session/session_tools.mli
src/session/session_tools.mli
+1
-1
No files found.
src/session/session.mli
View file @
f5efdfc0
...
...
@@ -18,7 +18,7 @@
(**************************************************************************)
(** Proof sessions *)
(** Define all the f
o
nction needed for managing a session :
(** Define all the f
u
nction needed for managing a session :
Creation, saving, loading, modification, ...
All the operation are immediately done.
Use session_scheduler if you want to queue the operations
...
...
@@ -171,7 +171,7 @@ val save_session : 'key session -> unit
(** {2 Context of a session} *)
(** A session which contains task and proof_attempt depends on an
environ
ne
ment and a prover configuration.
environment and a prover configuration.
Loaded provers are cached in order to load drivers once *)
type
loaded_prover
=
...
...
@@ -206,13 +206,13 @@ val update_session : keygen:'a keygen ->
allow_obsolete
:
bool
->
'
b
session
->
Env
.
env
->
Whyconf
.
config
->
'
a
env_session
*
bool
(** reload the given session with the given environnement :
- the file are reloaded
- the file
s
are reloaded
- apply again the transformation
- if some goals appear
s
try to find to which goal
- if some goals appear try to find to which goal
in the given session it corresponds.
The last case meant that the session was obsolete.
It is autorized if [allow_obsolete] is [true],
It is aut
h
orized if [allow_obsolete] is [true],
otherwise the exception [OutdatedSession] is raised.
If the session was obsolete is indicated by
the second result.
...
...
@@ -354,7 +354,7 @@ val goal_iter_leaf_goal :
(** iter all the goals which are a leaf
(no transformations are applied on it) *)
(** {3 not rec
c
ursive} *)
(** {3 not recursive} *)
val
iter_goal
:
(
'
key
proof_attempt
->
unit
)
->
(
'
key
transf
->
unit
)
->
'
key
goal
->
unit
...
...
src/session/session_scheduler.mli
View file @
f5efdfc0
...
...
@@ -68,7 +68,7 @@ end
module
Make
(
O
:
OBSERVER
)
:
sig
(** A session, with the environ
ne
ment, and the configuration *)
(** A session, with the environment, and the configuration *)
type
t
(** the scheduler environment *)
val
set_maximum_running_proofs
:
int
->
t
->
unit
...
...
@@ -87,7 +87,7 @@ module Make(O: OBSERVER) : sig
Env
.
env
->
Whyconf
.
config
->
O
.
key
env_session
*
bool
(**
Same as {!Session.update_session} except initiali
s
ation is done.
Same as {!Session.update_session} except initiali
z
ation is done.
*)
val
add_file
:
O
.
key
env_session
->
string
->
O
.
key
Session
.
file
...
...
@@ -166,24 +166,7 @@ module Make(O: OBSERVER) : sig
val
convert_unknown_prover
:
O
.
key
env_session
->
unit
(** Same as {!Session_tools.convert_unknown_prover} *)
(*
val reload_all: bool -> bool
(** reloads all the files
If for one of the file, the parsing or typing fails, then
the complete old session state is kept, and an exception
is raised
raises [OutdatedSession] if [allow_obsolete] is false and any obsolete
data for a goal is found in the session database
returns true if some obsolete goal was found (and
[allow_obsolete] is true), false otherwise
*)
val smoke_detector : smoke_detector ref
(** Define if the smoke detector is used *)
*)
end
...
...
src/session/session_tools.mli
View file @
f5efdfc0
...
...
@@ -23,7 +23,7 @@ open Session
val
convert_unknown_prover
:
keygen
:
'
a
keygen
->
'
a
env_session
->
unit
(** try to add new proof_attempt with known provers for all proof
attempt with unkn
w
on provers *)
attempt with unkno
w
n provers *)
val
filter_proof_attempt
:
?
notify
:
'
key
notify
->
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment