provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);

merge

minor tweak to error message

tuned;

explicit caret position after replacement;

tuned proofs

observe user preferences;

updated for release;

tuned;

tuned;