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?
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
Isabelle outer syntax is normally written with a bit more space, e.g.
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:
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and