refined activate_notes: simultaneous transformation before activation; actually export all_registrations_of;

tuned headers;

merged

Structured proofs in ZF

refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);

updated polyml/build option to prefer included libffi;

tuned signature;

clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;

merged

renewing Executable_Relation