actually negate "document" (cf. 7483aa690b4f);

clarified no_build vs. verbose;

clarified "document" again, eliminated redundant "no_document";

clarified build -n (no build);

added "document_dump_only" (cf. negated usedir -C);

more precise propagation of options: build, session, theories;

further imitation of ISABELLE_USEDIR_OPTIONS via options;

observe "condition";

observe "quick_and_dirty";

added "browser_info_remote" (cf. usedir -P);

clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;

timing for whole session;

tuned options;

timing is command line options, not system option;

clarified document options;

pass build options to ML; some imitation of usedir Session.init;

added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);

provide explicit ISABELLE_PLATFORM32 as well; discontinued some obsolete platforms; explicit error for unknown platform;

merged

set_vcs now derives prefix from fully qualified procedure / function name

try droppable application using Platypus functionality -- in contrast to earlier AppHack (cf. 9343d4b7c5bf);

updated to Platypus 4.7;

merged

tuned;

clarified init_component: always liberal; reduced divergence of clone from lib/scripts/getsettings;

added system build mode: produce output in ISABELLE_HOME; determine output location more explicitly;

removed redundant check (cf. a8ed41b6280b);

pass ISABELLE_BROWSER_INFO as explicit argument;

removed some old/unused stuff;

updated smlnj settings;