Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Print mode for fully-qualified names?

view this post on Zulip Email Gateway (Aug 22 2022 at 11:06):

From: Lars Hupel <hupel@in.tum.de>
Dear list,

is there a print mode (or a similar mechanism) which makes the pretty
printer output fully-qualified names for constants? If not, is there any
way I could implement that myself? I'm aware that the printer does it when
there are name collisions, but I want it always. (I need this from within
ML code, not within theory sources.)

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 11:06):

From: Makarius <makarius@sketis.net>
See isar-ref manual for names_long, names_short, names_unique.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 11:06):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,

Have you tried setting the configuration option [[names_long]]?

Hope this helps,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:07):

From: Lars Hupel <hupel@in.tum.de>

See isar-ref manual for names_long, names_short, names_unique.

Makarius, Andreas,

thanks, that did the trick!

Cheers
Lars

Last updated: Apr 26 2024 at 08:19 UTC