Email Gateway (Aug 22 2022 at 20:24): Email Gateway (Aug 22 2022 at 20:24):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear list,
I would like to have a nice setup for the syntax of our framework without
destroying Isabelle features such as the ability of clicking on the syntax
to jump to the definition and the ability of hovering over the syntax to
see the types. Namely syntax translation package is not what I really want.
For example, in our framework we have an algebraic structure with some
algebraic operators such as:
"X ;; Y" the operator is ";;"
Now if I have the following definition:
FG X f = "f(X)" (It is just a naive optimisation of the definition)
I would like to have the following syntax for FG:
"X:[f]"
Also I would like to be able to write:
"X;;Y:[f]"
How could I do that in a way where I still be able to click and hover on
";;" and on "..:[..]". Namely, how could I do that without loosing syntax
highlight offered by Isabelle.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 20:24):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Yakoub,
Plain mixfix notation preserves the Ctrl-click behaviour. Your examples can for example be
encoded as follows:
consts operator :: "'a ⇒ 'a ⇒ 'a" (infix ";;" 100)
consts FG :: "'a ⇒ 'b ⇒ 'c" ("_:[_]" [99,0] 99)
term "X ;; Y"
term "X ;; Y :[f]"
You can put such mixifx syntax after the types of most definitional commands, not just
"consts". By changing the precedence numbers, you can control how strong the operators
bind. See the Isabelle/Isar reference manual for the details of "mixifx syntax".
Best,
Andreas
Email Gateway (Aug 22 2022 at 20:26):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi Andreas,
Sorry for the delay, your email went to spam for some reason. I just read
it.
Thank you for the tip. It looks like Mixfix is what I want.
Do you think that there is a way to make other syntax translation work with
clicking.
For example any chance to make something like the following clickable:
f(x:=v1, y:=v2)
l[x:=v1, y:=v2]
{2,1,3,5}
[a,b ,c ,d]
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 20:27):From: Dominique Unruh <unruh@ut.ee>
Hi,
it seems that only syntax set up with the notation command (or its
derivatives such as the notation declaration in "definition" etc.)
becomes clickable/annotated, but not syntax set up with "syntax".
The best trick that I found to make things like ⟦x,y⟧ clickable is to
define dummy constants with appropriate notation, and then use those in
syntax declarations (translations can be defined on these dummy
constants, not just on syntactic constants). Then you can hover/click on
the ⟦ part of the formula, and it leads you to the definition of the
dummy constant (and if you place that constant next to the actual
relevant definition, it's almost as good as linking to the relevant
definition itself.)
The attached theory file illustrates this.
Unfortunately, this is a bit of a hack. I would be interested to know
whether it is possible to do the same while using syntactic constants
(defined with the "syntax" command). It would be great if one could
"link" syntactic constants to an existing constant for the purposes of
highlighting, for example.
Best wishes,
Dominique.
Scratch.thy
Last updated: Apr 20 2024 at 08:16 UTC