Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 14 Jun 1994 16:31:27 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02086; Tue, 14 Jun 1994 09:26:56 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA02082; Tue, 14 Jun 1994 09:26:45 -0600 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 14 Jun 1994 16:23:46 +0100 To: hol2000@leopard.cs.byu.edu Subject: Re: Improved error messages Date: Tue, 14 Jun 94 16:23:34 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:182270:940614152350"@cl.cam.ac.uk> Here is a variation on David Shepherd's suggestion. It occurred to me recently that exceptions in SML can have an exception as part of their data. So, redefining the standard exception in hol90 with an extra field, `previous_exception': exception HOL_ERR of {origin_structure : string, origin_function : string, message : string, previous_exception : exn}; would allow a full backtrace to be given in the error message, e.g.: Struct3.fun3: message3 caused by: Struct2.fun2: message2 caused by: Struct1.fun1: message1 When writing code I often find it difficult to decide whether to let a lower-level exception propagate, or to replace it with an exception for the function I am writing. The former usually gives a good idea about why the exception was raised but doesn't make it easy to locate. The latter makes location easy but one may have to single-step through the function to determine the exact cause. The above approach gives the advantages of both. Richard.