[isabelle] Add markup to term annotations

Dear all,

let's suppose I have a pseudo term annotation declared as abstract type, and
that I defined a term* command which mimics the term command and adds
the possibility to check the argument passed to the term annotation
as a string. Here is an example:

term*‹@{thm ‹HOL.refl›}›

I'd like to be able to add a markup to have the possibility to be redirected
to the HOL.refl definition when I click on it.

It seems that I need to find a method to compute positions
inside a ML string depicting a term parsed by the parse_term function,
which is called by the read_term function.

Do you have any idea how I can do it?

Or maybe you have another approach to suggest?

Best regards.

Nicolas Méric

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.