<no subject>

[<mark@proof-technologies.com>]

Thanks for the quick reply, David.

> What precisely do you mean by a problem - an exception or a syntax error?

An exception, a syntax error, any directive failing, or any other problem
(can't think of other examples at the moment).  I think #use aborts on all
these things, but not in a nested way.

> Assuming that it's syntax errors which you're trying to trap, then the
> neatest way would be to use ocamlc and ocamldep with a Makefile
> ....
>
> The toploop's directives are not part of the OCaml language - the toploop
is
> basically intended for debugging (or teaching, or experimenting). What
> exactly are you trying to do with the toploop?

Well my program is a classic LCF-style theorem prover.  Not sure if you know
what this is, but basically it's system for performing mathematical proof
that has a special architecture that allows the user to add their own source
code in a way that is guaranteed to be mathematically sound.

I want this to be a simple classic LCF-style system, and the top loop is the
traditional way in which such systems are used.  (In fact that was the
original purpose of ML!)  So I want to keep using the top loop.

> You could file a feature-request in Mantis for the behaviour of #use to be
> changed - I don't expect it would be that hard to change.

This sounds like a good idea, so long as it's a step in the right direction.
 I can't think why anyone would not want the behaviour I suggest.  How do I
file a feature request in Mantis?

I would also be interested in a neat shorter term solution that works in the
top loop.

Mark.