Handle (and pretty print) elaborator error messages in the lean default frontend

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Improve elaborator interface. Now, the metavariables are created inside the elaborator. The elaborator-user only needs to create placeholders. Motivaton: the placeholders are meaningful independently of the elaborator. On the other hand, the metavariables depend on the elaborator state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add test script

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add more tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>