web tools for s-expressions

[Michael Bogomolny <bogo@cs.utexas.edu>]

It would appear that html does not support nested tags.
I thought maybe someone in this group might have encountered the same
problem and might have some ideas on how to deal with this limitation.

What I'm trying to build is a tutoring system to teach people how to
use theorem provers. Most theorem provers do an awful lot of term
rewriting, and I would like a graphical way to take someone through a
series of term rewrites.

so, for example, if I'm trying to prove that
(app x (app y z)) = (app (app x y) z)
where app is the function append, then
the standard method is to prove it by induction: 
break it up into two cases
  1) x is an atom
  2) x is a pair
and us the recursive definition of app to rewrite each case.

all trivial so far. 

Now, what I'd like to do is have an interface so that if the user
places their mouse over the first "app" in "(app x (app y z))" the
entire s-expression highlights, or if they place it over the second
"app" the sub-s-expression "(app y z)" highlights. When the mouse is
pressed, different events will get fired depending on which region is
active. I'm finding this immensely difficult in html, but perhaps I'm
going about it the wrong way. (I'm trying to make each s-expression a
separate link, but can't do that easily since you can't nest links.)

Please look at
http://austin-ultimate.org/~bogo/mockup4.html 
and
http://austin-ultimate.org/~bogo/mockup15.html 
to see my best attempts so far. 
(There are problems with both of them, however.) 

Does anyone have a suggestion, either along the lines of
1) why don't you try such-and-such-a-method of doing this, or
2) why don't you use <tool x> instead of trying to do it in html?

thanks,
bogo

Michael Bogomolny
Assistant Instructor
University of Texas at Austin