clarified toString operations;

clarified socket connection;

server commands may access Server; Server.stop: proper shutdown; clarified signature;

tuned -- avoid regex matching on potentially large string; clarified message: command name could be malformed;

more robust build: prevent problems seen with Poly/ML eb94e2820013 on Mac OS X;

clarified notion of unknown files: ignore files outside of a Mercurial repository;

more balanced AFP partitioning;

more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);

tuned -- more uniform;

eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;

Drop rewrite rule arguments of sublocale and interpretation implementations.

more balanced AFP partitioning;

clarified signature;

build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;

more robust: normalize potentially symbolic rev;

proxy setup for lrzcloud1;

tuned signature;

support for permissive connections, for odd situations where host keys are not accepted;

proper target directory;

eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation);

document existing Apache2 configuration;

consolidated main cronjob server on virtual machine together with build_log database; eliminated special tricks for Gentoo; import plain_identify logs, export all logs for backup; run build_release, build_history_base in parallel to remote_build_history tasks;

identify closer to main cronjob -- avoid diverging changeset versions;

Drop rewrites after defines in interpretations.

proper remote_mac according to Admin/Release/CHECKLIST;

more Java heap, e.g. relevant for hg.graph on Isabelle repository;

more robust check -- do not rely on return code;

more compact ML_Statistics, to make build_status work with less than 2GB heap;

retain latest ml_stats (amending e76c6cb0d461);

accomodate smaller build machine;

clarified signature;

clarified self_update: imitate visible directory state on remote side;

more operations;

self_update implies push_isabelle_home (see also 4c253e84ae62);

uniform setup_repository (pull/clone without update); tuned signature;

clarified signature: facilitate interactive experimentation;

clarified tasks;

tuned signature;

proper order;

clarified README;

merged

more ssh options;

support for proxy connection, similar to ProxyCommand in ssh config;

prefer https;

avoid hardwired parameters; less ambitious defaults: low memory requirements;

Drop illegitimate optimisation from d5a7f2c54655.

Fall back to reading rewrite morphism first if activation fails without it.

Proper rewrite morphisms in locale instances.

clarified date for presentation vs. formal pull_date;

reveal raw data in CSV format;

support for CSV files;

tuned comment;

clarified syntax: reject formal comments explicitly, instead of ignoring them silently;

merged

generalized lemmas about orthogonal transformation

more explicit infixl (see initial 1edf0f223c6e); clarified name;

clarified use of vec type syntax;

new lemma

dedicated append function for string literals

generalized