added implicit type mode (cf. Type.mode);
added inner syntax parsers for sort/typ (no term/prop yet);
infer_types: exception TYPE => error;
read_vars: Syntax.parse_typ;
Major:
Complete pgip_types: add PGML and objtypes
Complete pgip_markup: provide markup abstraction for parsing.ML
Minor:
cleanups: signatures & structures, concrete types in XML attrs, etc.
further tests in pgip_tests.ML