Question on syntax-propertize-function

[Marco Maggesi <marco.maggesi@gmail.com>]

Hi,

I'm trying to improve an old emacs major mode I wrote some years ago (http://web.math.unifi.it/users/maggesi/holl-mode-2006-10-24.tar.gz) for editing HOL Light proof scripts (HOL Light is a theorem prover http://www.cl.cam.ac.uk/~jrh13/hol-light/, its syntax is close to OCaml and SML but with lots of idiosyncrasies).

I have two problems:

1. Comments are delimited by (* and *).  However, (*) should not open nor close a comment.

2. Anything enclosed in blackquotes `...` is a HOL term and follows a different syntax.

I suppose that this kind of issues are normally solved by setting text properties, but so far my attempts failed miserably.  I left aside problem 2 for now because I'm undecided on what to do exactly (e.g., should I set the syntax-table property for the quoted text or should I use syntax-entry "$   "?).

Here is what I did for problem 1.  I set a syntax table for holl mode which includes the following entries:

    (modify-syntax-entry ?\( "()1" st)
    (modify-syntax-entry ?\) ")(4" st)
    (modify-syntax-entry ?\* ". 23n" st)

This works as expected in most cases, but (*) open and close comments.
Then I defined a "propertize" function:

(defun holl-syntax-propertize (start end)
  (goto-char start)
  (funcall
   (syntax-propertize-rules
    ("\\((\\)\\(\\*\\)\\()\\)"
     (1 "()  ")
     (2 ".   ")
     (3 ")(  "))
    )
   start end))

and I set syntax-propertize-function in the initialization of the major mode:

  (set (make-local-variable 'syntax-propertize-function)
       #'holl-syntax-propertize)

However, this doesn't seems to have any effect.  I also played with syntax-propertize-extend-region-functions but with no success.

Can you see what's wrong with this approach?  Or can you suggest a debugging technique?  E.g., how can I run interactively syntax-property-rules?  I defined an interactive function

(defun holl-propertize (start end)
  (interactive "r")
  (funcall
   (syntax-propertize-rules
    ("\\((\\)\\(\\*\\)\\()\\)"
     (1 "()  ")
     (2 ".   ")
     (3 ")(  "))
    )
   start end))

and if I run it on a region containing (*) I get no effect.

Thanks,
Marco