Major: proof_general_emacs.ML fixups/PG compatibility: ongoing Complete pgip_types: add PGML and objtypes Complete pgip_markup: provide markup abstraction for parsing.ML Minor: <pgipquit> broken cleanups: signatures & structures further tests in pgip_tests.ML