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



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




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