Stream: Beginner Questions

Topic: Github

Huub Vromen (Jul 24 2020 at 12:17):

Isabelle theory files in Github sometimes use notation like "\<lfloor>\<P> \<N>\<E>\<rfloor>" . Is it possible to convert this into "normal" code, without having to do it manually?

Mathias Fleury (Jul 24 2020 at 12:19):

Isabelle/jEdit should replace it when opening the file. The generated documentation will also have symbols.

Mathias Fleury (Jul 24 2020 at 12:21):

Isabelle/jEdit is internally mapping the symbols like \<P> to the utf8 output, whereas github shows the raw file.

Josh Chen (Jul 24 2020 at 12:22):

Yeah, the whole Isabelle toolchain uses these custom encoding things, so unfortunately it's a thing you have to get used to if your idea of "normal" code is "UTF-8 encoded".

Mathias Fleury (Jul 24 2020 at 12:26):

As a side remark, do not attempt to replace the commands by the associated utf8 symbol. I did it once and it leads to very strange errors (isabelle build did not work, while isabelle jedit worked).

Mathias Fleury (Jul 24 2020 at 12:26):

For my own theories, I have a jenkins instance running to produce the documentation to be able to look at it, if I want to.

Josh Chen (Jul 24 2020 at 12:30):

Mathias Fleury said:

As a side remark, do not attempt to replace the commands by the associated utf8 symbol. I did it once and it leads to very strange errors (isabelle build did not work, while isabelle jedit worked).

I think there was a discussion on these things in an early thread on here. Do you know if it's a parser-related thing?

Huub Vromen (Jul 24 2020 at 12:31):

Thanks for your answers. I hoped there would be a way to get "UTF-8 codes". I do not encounter the problem with theories in the AFP.

Mathias Fleury (Jul 24 2020 at 12:32):

Josh Chen said:

I think there was a discussion on these things in an early thread on here. Do you know if it's a parser-related thing?

I did not try to debug it. I thought that Isabelle/jEdit maps all UTF8 symbols back to their representation, but I have no idea…

Mathias Fleury (Jul 24 2020 at 12:33):

Huub Vromen said:

Thanks for your answers. I hoped there would be a way to get "UTF-8 codes". I do not encounter the problem with theories in the AFP.

Chapter 3 of https://isabelle.in.tum.de/dist/Isabelle2020/doc/system.pdf to produce HTML code…

Huub Vromen (Jul 24 2020 at 12:56):

I have found the answer: when I reload the theory Jedit replaces the backslash-codes with the usual symbols.

Manuel Eberl (Jul 25 2020 at 08:19):

Sometimes, they stay there for no apparent reason, and you have to do "File → Reload with Encoding → UTF8-Isabelle"

Manuel Eberl (Jul 25 2020 at 08:19):

I think this sometimes happens when you load Isabelle theories that have actual UTF8 in them (as opposed to ASCII-encoded Isabelle symbols).

Last updated: Dec 21 2024 at 16:20 UTC