GitLab

Controller is now dummy until the first open request is given.

Add a name_table in printer_args.
Put the definition of name_table in task.ml.
Build_name_tables only called once in proof_node creation.
Modified the rest accordingly.

+ complete get_first_unproven_goal_around_pn function.

* call_provers.ml
(prover_update): Adding unimplemented errors that reflects the cases of
proof_attempt_status. Otherwise, proof_attempt_status is a list of cases
that are never reached.
* controller_itp.ml
(proof_attempt_status): Added Uninstalled case in proof_attempt_status.
Launched in replay when asked to replay something not installed.
(print_trans_status): Adding a ! when proof is valid for debugging
reasons.
(report): Added a report type for replay reporting of differences.
(print_report): printing function for report.
(replay_print): callback used with replay to print the report at the end.
(replay): Function that replays all proof attempts of the session.

* session_itp.ml
(session_iter_proof_attempt): Added the proofNodeID the fold function
for convenience.
* why3shell.ml
(test_replay): Added to test replay.

- add session directory and restore old session file mechanism

Added proof_state and functions to control it in controller_itp.
Tried to add a test case for it inside the command p to put a big
P next to a goal that is proved.
It is currently buggy. Needs investigating and cleaning.

+ modify the command that print the sessino tree to specify where we are in the tree with "**"
+ add some more comprehensible error messages to wraper function for parsing

"parsing" of these strings is delayed in the transformations themselves,
because in case such an argument must be interpreted as a term, the
task itself is needed do perform name resolution.

Incidentally, saving transformations with arguments in sessions is not an
issue anymore

Adapted work on nearest_goal_right to be able to use it why3shell.
Now should be able to apply transformation and proof on current goal. Also
able to print the current tree and goal. Requires testing.

It finished for why3prove but not finishedfor why3ide yet.

If these are set, the prover is asked for counter-example and if the counter-example is got, it is displayed.

characters '. ", <, > and &