Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Message-Id: <199510131345.AA18700@ailsa.gmd.de>
To: Rob Shaw <shaw@cs.ucdavis.edu>
Cc: info-hol@cs.uidaho.edu
From: Matthew Morley <morley@gmd.de>
Subject: Re: HOL90 with SML/NJ debbuger? 
In-Reply-To: Your message of "Thu, 12 Oct 1995 18:05:45 MST."
             <199510130105.SAA20745@roma-cafe.cs.ucdavis.edu> 
Date: Fri, 13 Oct 1995 14:45:13 +0100

Rob

if you use sml-mode-3.1 you should (very probably) also pick up the
version of sml-debug that i hacked to go with it. warning: the
keybindings moved -- see:

  ftp://borneo.gmd.de/pub/sks/mjm/sml-mode

the smld command is just like the the sml command, hence:

  C-u M-x smld <RET> hol90 <RET> <RET>

should launch the whale -- no need to set that sml-program variable.
let me know if not.

note that sml-mode is now at 3.2 (better font-lock, and *info*) but i
have not tested sml-debug much. is it even useful?!

another tip: sml-mode needs to read the absolute path of (.sml) files
it loads (automatically), so make sure sml/nj is printing this in
error messages, etc. hol90 sets the variable

  System.Control.Print.pathnames

to 2 in sys01.sml (you'll have a hard time finding it referenced in
the sml/nj docs). set it back to 1000, e.g., in hol-init.sml.

M