permissive treatment of citations before the theory header: avoid too many changes in AFP;

more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup; more Document_Build.running_script, but display it as "Running XYZ";

clarified documentation: avoid odd speculations about PIDE;

tuned;