publish a private function

tuned names

re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;

more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;

prefer standard Isabelle/ML operations;

some system options as context-sensitive config options;

load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;

support for system options as context-sensitive config options;

tuned signature;

tuned comments;

support for options as preferences;

more operations in accordance to Scala version;

more systematic access to options default;

full default options for Isabelle_Process and Build;

decentralized historic settings;

removed obsolete test_markup; tuned;

Proof General interaction always uses Isar loop; pass Isabelle/Scala options to Proof General process as well;

proper context;

merged

more direct PGIP/Emacs processing and output;

more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;

removed redundant modules;

removed some obsolete PGIP/PGEclipse material;

never open structure Unsynchronized (cf. "implementation" manual);

prefer explicitly qualified exceptions, which is particular important for robust handlers;

avoid PolyML.makestring, even in dead code;

fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"

don't apply an unnecessary morphism