Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE



On 11/14/2015 9:42 AM, Makarius wrote:
Can you say this again in plain words?

Makarius,

Part of its meaning was to say that I won't respond back to anyone who responds back to me. But to show respect, among other reasons, such a rule should be applied with discretion.

There are jokes to be made, but all this is no joking matter. It is also an example of a problem where there is no good solution. The purpose of a "bug tracking" system would be narrowly defined, but this is a forum, and a forum is about engaging with people as humans. (Note: As to "bug tracking" systems, though I don't agree with how you dealt with a particular event, your philosophy sounds reasonable to me. In the end, though, apart from this, I consider "things" like that to be "Isabelle internal politics", and not for me to be concerned with.)

First, I just state another rule of mine about how I operate on the web, where I consider this as part of the web. My rule is not to engage with people privately who aren't personal friends. If something starts in public, I make a point of keeping it in public.

There's this problem that I want to protect my technical interests, by reporting problems, but the traffic is light here, and so I can end up creating a big footprint here. I do want a footprint on the web, but I don't want one here. I do searches on the isabelle-user's page, and there I am, showing up way too much.

Stating a formality was maybe the third iteration of trying to solve this problem.

Isabelle outer syntax is normally written with a bit more space, e.g. like this:

  FOOBAR \<open>test\<close> \<open>test\<close>

Let us consider that your time is more valuable than mine.

You tell me how to do things, but then I don't do it your way. At this point, it has already been a waste of your time to read this, and the last two sentences.

When you can see my ideas as a whole, then it won't be a waste of your time to tell me how I should do things. In a just a few minutes, you'll you be able to say, "Yea, there's a few good ideas here, I see why you're having to do things different", or, "This is worthless, there's no good reason for you to be doing things different.".

The use of no space would be specific to using "FOOBAR" as a text-text-argument markup tag, in a way that's meant to take up as little space as possible. As to two-arg outer syntax tags, there is also text-term and term-text. Below, I say that new additions to releases eliminate any special needs.

You are nonetheless right, that there is a mistake in the scanner for cartouches in Isabelle/ML, and it disagrees with the Isabelle/Scala version. I have changed that 3 weeks ago here: http://isabelle.in.tum.de/repos/isabelle/rev/760e21900b01

And this would be in line with how I think I should operate sometimes, that problems like these have been taken care of, or will eventually get taken care of, so there's no need for me to get involved. But then the flip-side-analogy is 10 people getting served, who came in after me; I assume I'll get served, but I don't, because they lost my order.

Thus the coming winter release should work better in this respect. When the first release candiates are announced, you should definitely try them. There is a good chance that other improvements are in conflict with your way of writing Isabelle documents. See also http://isabelle.in.tum.de/repos/isabelle/file/f1b257607981/NEWS#l85

I continue to welcome new additions, and I see the addition of \<^verbatim> and \<^emph>.

I try to build on what others have done, so to the extent that the new features line up with what I think I need, or to the extent that they only can be used in one way, I use them the normal way. To your chagrin, I may use them differently.

What I do shouldn't undermine anything. For me, it's the real deal. For others, I hope to make it a demo of what could be done, most likely in a more sophisticated way.

I end this mentioning three "features", some outer syntax commands that get interpreted as LaTeX newtheorem environments, where the source that follows is put in a fancyverb environment with line numbers, directly underneath the newtheorem title. The 3rd feature would be "subtle" syntax that gets interpreted as a very specific LaTeX equation environment.

I ask, "Do these features exist?", and, "If they don't, should you make implementing them a priority just for me?"

The answers are no and no. What I want is more textbook style. What you guys needs is more journal style.

I could explain what my ideas are for the two-text argument of FOOBAR above, as a tag, but it would be a waste of your time. If I ever produce something, it'll already have been superseded by a new feature, or you'll very quickly be able to look see at what might interest you.

New features sometimes eliminate a need for what I've done, but sometimes they don't. Given enough time, anything I've done, you'll have done better, but I have to commit now.

With all due respect, I don't respond to those who respond back to me.

Regards,
GB





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