Michael Moeller (Apr 12 2024 at 22:29): Michael Moeller (Apr 12 2024 at 22:29):Hi,
this is a beginners question regarding the Isabelle 2023 IDE.
It's about operation only. I'm quite familiar with other provers.
No matter which of the examples from the docs I copy to the
editor, I get nothing but nice coloration. Supposedly it should
respond unasked. Whether the docs tell half the truth or the
examples are mere snippets remains unclear.
Since the IDE is not exactly self-explanatory, a simple step by
step example would be much appreciated.
Thanks for your help.
Kind regards
Michael
Lukas Stevens (Apr 12 2024 at 22:34):You probably don't have proof state enabled in your output window. Therefore, you only see diagnostic messages in the output, which can be empty depending on the command. You can either check "Proof State" in the output panel or look at the dedicated proof state output panel on the right instead.
Lukas Stevens (Apr 12 2024 at 22:35):At the least that's my guess because you said that syntax highlighting is working.
Michael Moeller (Apr 12 2024 at 23:52):@Lukas Stevens
Thanks. This works. In addition I just realized copy and paste from the docs may work
or not, depending on the PDF in question. If not, input must be edited manually.
Things only work after restarting the IDE. Is this really mandatory or is there a button
which clears everything I've done so far?
Lukas Stevens (Apr 14 2024 at 16:30):I am not sure what you mean. If you copy code from somewhere else and want it probably set in UTF-8 you can save your file and then refresh (F5 should work). Other than that, deleting the text in the buffer is the same clearing.
Michael Moeller (Apr 14 2024 at 20:14):This charset thing is really annoying. Especially if you can't tell sytax errors from others yet.
Anyway, if I understand right this means if 20 files have been loaded and I turn to another unrelated
problem I have to remove anything file by file manually? I'm asking this because working with
software having some kind of 'top-level -like' behaviour often shows the strangest results by
re-loading, adding or deleting things.
Lukas Stevens (Apr 15 2024 at 10:55):I think that I don't really understand what you are trying to do. You need to be more specific in what you are doing, what you expect to happen and what actually happens. Furthermore, it is not necessary to reload the file. You only need to do that to display the UTF-8 correctly.
Mathias Fleury (Apr 15 2024 at 11:53):I know that I have in passed accidentally deactivated the "continuous checking" (in the theories panel) which is reactivated when restarting Isabelle/jEdit
Mathias Fleury (Apr 15 2024 at 11:53):But you should put an example here of what you are copy-pasting that is not working…
Michael Moeller (Apr 15 2024 at 14:58):I see. I'm talking about two different things. Please forget
about UTF-8 problems. At all times PDF files contained special
characters like ", < and > which get invalid by means of copy
and paste. It's neither new nor specific to Isabelle.
An example regarding the other question would be the following:
Load some files from the documentation box (upper left). Then
click 'New' and pick an example from sledgehammer.pdf, say
"First Steps" from page 5. Copy and paste it to Isabelle.
You may delete the other files in advance or afterwards or
check/uncheck whichever box you like. Unless you restart
Isabelle and get "First Steps" again, it triggers nothing. It
doesn't even get colorized.
That's why I asked whether to restart is the only way to get
rid of anything done so far.
Fabian Huch (Apr 15 2024 at 15:05):Copying from PDFs may or may not work as you have noted. If you're creating a new theory file, you'll have to save the file with appropriate file ending first, this has nothing to do with copying.
Michael Moeller (Apr 15 2024 at 21:13):Thank you. This works.
Last updated: Dec 21 2024 at 16:20 UTC