proper SSH operations;

tuned signature: more permissive;

clarified signature: explicit variable is easier to find in source;

proper services for Setup_Tool --- avoid hardwired stuff;

merged

renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal

more robust XML body: allow empty text, as well as arbitrary pro-forma markup (e.g. see XML.blob in Isabelle/ML);

more robust: untyped/unscoped markup elements need to reside in module Markup for minimal static checking (see also 11a1f4d7af51);

misc tuning for release;

merged;