Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: shaw@cs.ucdavis.edu (Rob Shaw)
Date: Thu, 12 Oct 1995 18:05:45 -0700
Message-Id: <199510130105.SAA20745@roma-cafe.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: HOL90 with SML/NJ debbuger?
Content-Length: 973


I'm having trouble using HOL90 with smld, the SML/NJ compiler with 
debugging support. Hopefully, someone out there has already figured out 
how to do this. Here's what's going wrong on my end:

The debugger that comes with the sml distribution in the tools directory 
has some .el files, but these are for emacs 18.xx (in particular, they use
shell code instead of interp code). [aside: no need to send solutions that
involve my going back to emacs 18, I won't do it!] 

If I use the current sml-mode, 3.1, and then (load-file "sml-debug.el") by
hand, I still don't get the *sml-debug-command* window. The debugger starts,
and I get the [dbg]- prompt, but without access to all the Meta-key commands
that are bound in that window, I don't know how to actually run, step, 
continue, and so on...

I don't know if this matters or not, but before starting HOL with M-x sml,
I (setq sml-program-name "<image_file>").

Any help on this is greatly appreciated...

Thanx,

Rob