On Sun, 2 Mar 2008, Rob Arthan wrote:
If you write your own read-eval-print loop using PolyML.compiler, you may want to treat exceptions raised during the eval stage specially. However you can't currently stop Poly/ML printing out the exception.
In Isabelle we do have our own toplevel loop (for the Isar theory and proof language). ML is also embedded here, and passed down via PolyML.compiler. Exceptions are handled the regular way, and printed with General.exnMessage (more specific output for one of our key exceptions). We also managed to get PolyML.exception_trace, PolyML.profiling, and interrupt management through our toplevel.
If you are curious see Isabelle/src/Pure/ML-Systems/polyml.ML and Isabelle/src/Pure/Isar/toplevel.ML for the gory details.
Makarius