2014-08-12 wenzelm 2014-08-12 separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
2014-04-30 wenzelm 2014-04-30 clarified signature: load_file is still required internally;
2014-03-31 wenzelm 2014-03-31 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2014-03-26 wenzelm 2014-03-26 superseded by (provide_)parse_files;
2014-03-18 wenzelm 2014-03-18 clarifed module name;