- 19 Dec, 2016 1 commit
-
-
Sylvain Dailler authored
-
- 16 Dec, 2016 2 commits
-
-
Sylvain Dailler authored
-
MARCHE Claude authored
-
- 15 Dec, 2016 1 commit
-
-
Sylvain Dailler authored
Split itp_server into itp_server and server_utils for readability. Split why3ide into why3ide and ide_utils for readability.
-
- 14 Dec, 2016 1 commit
-
-
Sylvain Dailler authored
Also do following changes: Changed printer to allow printing from label again. changed callback of transformation so that creating node is always done before updating it. Added a root for coherence and easy Clear the message zone for a demo.
-
- 12 Dec, 2016 1 commit
-
-
Sylvain Dailler authored
-
- 11 Dec, 2016 1 commit
-
-
Sylvain Dailler authored
Ide server compiles. Gtk ide still does not compile.
-
- 09 Dec, 2016 1 commit
-
-
MARCHE Claude authored
-
- 08 Dec, 2016 1 commit
-
-
Sylvain Dailler authored
Factor debug protocol functions. Remade printing work for why3shell. The Zipper was removed.
-
- 07 Dec, 2016 1 commit
-
-
Sylvain Dailler authored
(ide) new_node returns the row_ref of new node. So that we can go to the ggoal generated by transformation (convenience). Changed the update of the proof_status in controller_itp. update_node functions now take a callback called notification which is actually P.notify (node_change). Put type any inside session_itp.ml.
-
- 06 Dec, 2016 2 commits
-
-
Sylvain Dailler authored
Removed duplicated code. Handling of unrecoverable exception in treat_request so that server dont get stuck.
-
Sylvain Dailler authored
Fixed monitor. Moved History.
-
- 05 Dec, 2016 1 commit
-
-
Clément Fumex authored
-
- 01 Dec, 2016 1 commit
-
-
Sylvain Dailler authored
replay_print now takes a formatter. Added messages and message_notification. Added New_node. Changing name of command request for disambiguation. Changed parsing of IDE command line. (function interp).
-
- 29 Nov, 2016 1 commit
-
-
Sylvain Dailler authored
Change many function from gconfig.ml to remove ref to Whyconf. Add protocol file. Add whats needed in an adhoc way. Need cleaning. Compile but fails.
-
- 24 Nov, 2016 1 commit
-
-
Sylvain Dailler authored
Adding a forgeting function for printing variables on exceptions. Should do the same at least for patterns. Adding printing functions from why3printer. Changing exception in transformation so that they return terms not strings.
-
- 23 Nov, 2016 6 commits
-
-
Sylvain Dailler authored
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.
-
Clément Fumex authored
-
Clément Fumex authored
-
Clément Fumex authored
-
Clément Fumex authored
+ complete get_first_unproven_goal_around_pn function.
-
MARCHE Claude authored
-
- 22 Nov, 2016 6 commits
-
-
Clément Fumex authored
-
Clément Fumex authored
-
Sylvain Dailler authored
-
MARCHE Claude authored
-
Clément Fumex authored
-
Clément Fumex authored
-
- 21 Nov, 2016 2 commits
-
-
MARCHE Claude authored
-
Sylvain Dailler authored
-
- 18 Nov, 2016 3 commits
-
-
Sylvain Dailler authored
I added an exception to TSfailed. Also changed the query exceptions.
-
Clément Fumex authored
-
Clément Fumex authored
-
- 17 Nov, 2016 7 commits
-
-
Clément Fumex authored
move current row when attempting to run a prover or a transformation from an other position than a goal
-
Clément Fumex authored
-
Clément Fumex authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Sylvain Dailler authored
-