made SML/NJ happy;

clarified YXML.detect;

retain some terminology of "XML attributes";

more uniform Properties in ML and Scala;

more uniform Term and Term_XML modules;

more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;

tuned signature -- less cryptic ASCII names;

discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;

added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;

added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;

more precise Symbol_Pos.quote_string;

clarified YXML.embed_controls -- this is idempotent and cannot be nested;

allow empty body for raw_message -- important for Invoke_Scala;

Isabelle string syntax allows literal control characters;

glyphs from DejaVu for ASCII control characters 5, 6, 7, 127, which have a special meaning in Isabelle or Poly/ML;

more precise exceptions;

tuned XML modules;

Quotient example: Lists with distinct elements

merged

explicit code equation for equality

tuned error messages;

tuned;

tuned signature -- corresponding to Scala version;

made SML/NJ happy; tuned error;

more uniform padded_markup, which is important for caret visibility despite absence of markup;

merged

merged

tuned proofs