Ca m'apprendra a commiter/pusher trop vite...

grants a long-standing feature wish by Andrei

this is a contribution of Laurent Théry

predicates permut over maps and arrays are given new semantics, as follows:
- MapPermut: permut m1 m2 l u means that m1[l..u[ is a permutation of
  m2[l..u[ and values outside the interval [l..u[ are *ignored*.
- ArrayPermut: permut_sub a1 a2 l u means that a1[l..u[ is a permutation
  of a2[l..u[ and other meaningful values are *identical*.
- ArrayPermut: another predicate map_permut_sub has the same semantics as
  MapPermut.permut_sub, that is values outside of the interval [l..u[
  are ignored

missing proper executable rights

Support for Isabelle in "server" mode, to avoid start-up time

- Properly indent comments placed after a symbol (à la ocamldoc).
- Handle tabulations as spaces.
- Remove spurious blank lines with (***.
- Avoid the costlier fprintf whenever possible.

clarified jEdit server mode: start "isabelle why3_jedit" first and let why3ide connect to via "isabelle why3 -i jedit"