Le 19/10/2016 à 19:37, Per Lindgren a écrit : > Dear Claude > > Thanks for your prompt answer. I will look into this. > > The version I’ve been working with is the one checked out through > opam (0.87.2). Is this the same version as the master branch, or?
No it is not. the git master branch contains the future release 0.88. The release 0.87.2 corresponds to the branch bugfix-0.87 > Indeed, simply c/i/s works (I believe I tried all key combinations, > just not the plain keystrokes ;) > >> I'm not sure about what you ask exactly. Strategies are not >> "officially" supported in the release 0.87.2, but they are if you >> follow the git master branch. In that case you will find >> information in the documentation, section 10.6. > > I mean the list of buttons (Compute, Inline, Split). These occur also > in the drop down under Tools/Strategies (0.87.2). Maybe you mean some > other type of strategies (referring to the git master branch). I see. I did not remember these where called "strategies" in the menu in the 0.87. As far as I know, in 0.87 you cannot customize these. It will be possible in the next release, or again, try the git master if you want. >>> And perhaps most importantly: 4. Is there a simple way to undo a >>> ... >> >> Unfortunately it is not possible. If you are lucky and just loaded >> the session, or just saved the session into disk, then you have >> the possibility to exit without saving and reload. > Would it be possible to implement this as a stack (or possibly two > stacks, for redo), storing the “session” information, and then on > e.g. Cmd-Z/Cmd-Shift-Z (undo/redo) push current session to the redo > stack, and pop the undo, and on the result call the function that > processes the “session” information. Perhaps that would essentially > amount to restarting the whole Why3 on undo/redo, but at least it > would be more convenient than the suggested exit/restart. Good suggestion but not so easy because implementation of sessions involve imperative/mutable/non-persistent aspects, and also asynchronous aspects (external prover calls). - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
