Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Add markup to term annotations

view this post on Zulip Email Gateway (Jun 19 2021 at 10:45):

From: Nicolas Méric <>
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: Jul 15 2022 at 23:21 UTC