Re: [isabelle] Remaining use of {* ... *}

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.


Attachment: 140827__mydoggy horizontal split.png
Description: PNG image

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.