Email Gateway (Aug 19 2022 at 15:37): Email Gateway (Aug 19 2022 at 15:37):From: Makarius <makarius@sketis.net>
Just the canonical question: What is the remaining use of {* ... *} here?
It won't go away, but might eventually be superseded by \<open> ...
\<close> (which is rendered in Unicode as as ‹...› with some input method
in the Prover IDE via single backquote).
I am myself using mainly ‹...› since a few months and it should be easy to
make an Isabelle/Scala function to replace outer syntax {* ... *}
systematically in existing Isabelle projects.
At UITP 2014, Andrew Butterfield briefly referred to Isabelle/UTP
http://www-users.cs.york.ac.uk/~simonf/utp-isabelle in comparison to his
own UTP proof assistant. He made a funny rant about "terms in double
quotes with double single quotes to quote UTP within HOL". Moving more
and more towards cartouches ‹...› would make the nesting of Isabelle
languages more regular.
Makarius
Email Gateway (Aug 19 2022 at 15:37):From: Gottfried Barrow <igbi@gmx.com>
On 14-08-27 04:17, Makarius wrote:
On Tue, 26 Aug 2014, Gottfried Barrow wrote:
There is one huge surface addition, and that's \<open> and \<closed>.
Those are huge, because they're subtle and graphical, and they help
to clearly delimit the beginning and end of text, better than {* and
*}, though those have their use.Just the canonical question: What is the remaining use of {* ... *} here?
I was just playing it safe. It might come in useful to be able to
visually differentiate something, or someone else may live and die by
it, for some reason.
One problem with graphical characters is they don't align good in
columns with ASCII characters, so I set up my notation many times to
give myself an ASCII-only version, if I also have one with graphical
characters in it.
Just now testing out \<open>, it has the same spacing as an ASCII
character. Most non-ASCII symbols don't, though a few do, such as \<bar>.
He made a funny rant about "terms in double quotes with double single
quotes to quote UTP within HOL"...
I take your word that if you didn't use some sort of delimiters for
terms, that it would come back to haunt you. It seems that the
architects of new languages such as Scala and Rust would have abandoned
the use of "{" and "}", like Haskell, but they didn't, so I guess they
had good reason not to.
Here are a maintenance question and comment I've held off on.
Is there a way to keep PIDE from loading Scratch.thy? I don't use it. In
the past, I think I tried to mess with the command line options for
jEdit, though Isabelle, but couldn't force it to not load Scratch.thy.
That brings up the MyDoggy plugin, which has some quirks, but I've
figured workarounds. After I close Scratch.thy, MyDoggy won't parse any
other buffer view, so I have to shift-mouse-click on the Sidekick tab to
eliminate it, and then shift-mouse-click on it to bring it back.
The reason I specifically use MyDoggy is to be able to do horizontal
splits on the plugin panels. Using MyDoggy is the only way I know of to
do that, and it's very important for me to be able to do that. I can
split buffer views horizontally, but I can't normally split plugin
panels, you can only move them to the top, left, right, and bottom.
I attach a screenshort to show my normal, one-window setup for the PIDE.
I normally permanently have two non-buffer views, sidekick and output,
in addition to two vertical buffer views. The other tabs, I have them
set up in pin mode. I click on them, they expand out without eliminating
sidekick and output, then I click on them to eliminate them. With 10 or
so plugin views, floating windows don't work, except for temporarily
detaching a view.
I understand that MyDoggy is not being actively developed, so it makes
sense for you not to officially use it. But without MyDoggy, I would be
in a constant state of annoyance, trying to find some PIDE view that
works for me, but never does.
Regards,
GB
140827__mydoggy horizontal split.png
Email Gateway (Aug 19 2022 at 15:38):From: Makarius <makarius@sketis.net>
On Wed, 27 Aug 2014, Gottfried Barrow wrote:
He made a funny rant about "terms in double quotes with double single
quotes to quote UTP within HOL"...I take your word that if you didn't use some sort of delimiters for
terms, that it would come back to haunt you. It seems that the
architects of new languages such as Scala and Rust would have abandoned
the use of "{" and "}", like Haskell, but they didn't, so I guess they
had good reason not to.
There is no plan to remove delimiters, but to simplify them. The Coq guys
made the mistake a long time ago to assume that everything fits into just
one formal syntax, and got a lot of problems over the years. Coq PIDE is
still very crude in its command-span parsing, for example.
In Isabelle we've had systematic inner syntax that is delimited within the
outer syntax for uncounted years, but the different kinds of quotes make
things a bit complicated and unesthetic. With cartouches there is a
chance to improve that. See also ~~/src/HOL/ex/Cartouche_Examples.thy in
Isabelle2014 -- it is just playground of possibilities.
Is there a way to keep PIDE from loading Scratch.thy? I don't use it. In
the past, I think I tried to mess with the command line options for
jEdit, though Isabelle, but couldn't force it to not load Scratch.thy.
Scratch.thy is not opened if you specify other files to open.
On Windows the main Isabelle.exe application wrapper accepts normal
arguments according to that platform, e.g. via drag-and-drop. You can
also create a Windows alias for the exe and give it some arguments via the
Windows Properties dialog. Using the special argument "--" (the
end-of-options indicator of jEdit) seems to do the trick to imitate a
semantically empty command-line that looks syntactically non-empty.
I understand that MyDoggy is not being actively developed, so it makes
sense for you not to officially use it. But without MyDoggy, I would be
in a constant state of annoyance, trying to find some PIDE view that
works for me, but never does.
There was a recent initiative on the jedit-devel mailing list to re-assign
maintainers to some unmaintained plugins. MyDoggy was one of them. It
has the additional problem that the underlying MyDoggy project is
inactive.
Anybody with notable Java/Swing skills should be able to revive that. See
also http://mydoggy.sourceforge.net/
Makarius
Last updated: Nov 21 2024 at 12:39 UTC