Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 21 Sep 1993 12:55:08 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA17789;
          Tue, 21 Sep 93 04:37:46 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA17785; Tue, 21 Sep 93 04:37:44 -0700
Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 21 Sep 1993 12:37:41 +0100
To: info-hol@cs.uidaho.edu
Subject: Re: "hol90.el" (emacs for hol90)
Date: Tue, 21 Sep 93 12:37:35 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:055720:930921113743"@cl.cam.ac.uk>

On the subject of emacs modes for hol90, I have some functions for making
entering of quotations easier (at least in my opinion). These modify the
binding of the backquote key so that it generates (--` the first time it is
hit and `--) on the second time. I'm no emacs-lisp hacker, so the code is
fairly naive. In particular, it just works on a simple parity basis, so if
you hit backquote by mistake, you'll need to hit it again to get back to the
right state.

Backquote can be bound to term quotes using the emacs command:

   M-x HOL90-quote <CR> term <CR>

Similarly for type quotes:

   M-x HOL90-quote <CR> type <CR>

If you have your own parser for an embedded language, you can introduce new
quotes for it. For example, if you have a parsing function parse_foo for a
language FOO:

   parse_foo : term frag list -> term

then you might make the following SML declarations:

   fun BEGIN_FOO frags x = parse_foo frags;
   val END_FOO = <anything>;

and give emacs the commands:

   M-x HOL90-new-quote <CR> FOO <CR> BEGIN_FOO <CR> END_FOO <CR>
   M-x HOL90-quote <CR> FOO <CR>

You can then enter FOO quotations as:

   (BEGIN_FOO` ... `END_FOO)

without having to type the parentheses or the BEGIN_FOO and END_FOO.

I've used BEGIN_FOO and END_FOO to illustrate the functions. I'd probably just
use FOO for both delimiters.

Finally, if you want to return to the normal operation of the backquote key,
just enter an empty language name:

   M-x HOL90-quote <CR> <CR>

The code follows. Feel free to modify it and/or include it in any hol90 emacs
modes.

Richard.



(setq HOL90-languages '(("term".("--"."--")) ("type".("=="."=="))))
(defun HOL90-new-quote (name left right)
  (interactive "sLanguage: \nsLeft string: \nsRight string: ")
  (setq HOL90-languages (cons (cons name (cons left right)) HOL90-languages)))

(setq HOL90-quote-name nil)
(defun HOL90-quote (name)
  (interactive "sLanguage: ")
  (if (assoc name HOL90-languages)
      (setq HOL90-quote-name name)
      (setq HOL90-quote-name nil)))

(setq HOL90-quote-parity nil)
(defun HOL90-insert-quote ()
  (interactive)
  (let ((brackets (assoc HOL90-quote-name HOL90-languages)))
       (if brackets
           (progn (setq HOL90-quote-parity (not HOL90-quote-parity))
	          (if HOL90-quote-parity
                      (insert (concat "(" (car (cdr brackets)) "`"))
                      (insert (concat "`" (cdr (cdr brackets)) ")"))))
           (insert "`"))))
(global-set-key "`" 'HOL90-insert-quote)