Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 1 Sep 1995 10:28:33 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA210175885;
          Fri, 1 Sep 1995 02:58:05 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA209975869;
          Fri, 1 Sep 1995 02:57:49 -0600
Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Fri, 1 Sep 1995 09:59:33 +0100
X-Mailer: exmh version 1.6.1 5/23/95
X-Uri: <URL:http://www.cl.cam.ac.uk/users/rjb>
To: Kelly Hall <hall@cs.byu.edu>
Cc: info-hol@leopard.cs.byu.edu, Richard.Boulton@cl.cam.ac.uk
Subject: Re: HOL90 error on 'export_theory'
In-Reply-To: Your message of "Thu, 31 Aug 1995 19:14:09 MDT." <199509010114.AA060958050@puma.cs.byu.edu>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Fri, 01 Sep 1995 09:59:26 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:101570:950901085941"@cl.cam.ac.uk>

Kelly Hall <hall@cs.byu.edu> writes:

> Is there a way for me to get a more enlightening error message than
> the uncaught exception (that goes scrolling merrily off the screen)?

There is a function Raise (note the capital `R') that will print out the
HOL_ERR message and then re-raise the exception. Here is an example:

   - mk_comb {Rator = (--`1`--),Rand = (--`0`--)};
   
   uncaught exception HOL_ERR
   - mk_comb {Rator = (--`1`--),Rand = (--`0`--)} handle e => Raise e;
   
   Exception raised at Term.list_mk_comb:
   incompatible types
   
   uncaught exception HOL_ERR
   - 

Richard.