From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 62FDEBC57 for ; Thu, 7 Oct 2010 20:25:02 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhEHAC+srUxV6aAZUmdsb2JhbACDH5EmjgALARYJCgYEECK5Z5JEDYEVgzF0BIpAgwI X-IronPort-AV: E=Sophos;i="4.57,298,1283724000"; d="scan'208";a="72002025" Received: from outgoing-smtp.namesco.net ([85.233.160.25]) by mail2-smtp-roc.national.inria.fr with ESMTP; 07 Oct 2010 20:25:02 +0200 Received: from [192.168.0.17] (helo=venus) by outgoing-smtp.namesco.net with esmtp (Exim 4.67) (envelope-from ) id 1P3v9H-0006Dn-Dv for caml-list@yquem.inria.fr; Thu, 07 Oct 2010 19:25:00 +0100 Received: from root by venus with local (Exim 4.69) (envelope-from ) id 1P3v9J-0004Ps-54 for caml-list@yquem.inria.fr; Thu, 07 Oct 2010 19:25:01 +0100 To: From: Reply-To: Subject: MIME-Version: 1.0 X-Mailer: Namesco Webmail v3.0 Message-ID: <1286475900848@names.co.uk> Date: Thu, 07 Oct 2010 19:25:00 +0100 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-namescosender: 0 2002 X-namesco: 192.168.0.171 X-Spam-Score: -1.0 (-) X-Spam: no; 0.00; syntax:01 syntax:01 ocamlc:01 ocamldep:01 makefile:01 ocaml:01 toploop:01 toploop:01 exception:01 exception:01 precisely:01 behaviour:01 behaviour:01 theorem:02 failing:02 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.