Email Gateway (Jun 19 2021 at 10:45): Email Gateway (Jun 19 2021 at 10:45):From: Nicolas Méric <nicolas.meric@lri.fr>
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
Last updated: Jan 04 2025 at 20:18 UTC