Re: [isabelle] 0::'a
On Mon, 18 Nov 2013, Tobias Nipkow wrote:
You mean Isabelle/jEdit, or rather the Isabelle/Scala document model
behind it; jEdit is just a plain text editor.
You may observe that I intentionally wrote "with jedit" (rather than,
eg, "in jedit"). The word "with" indicates a contextual dependence, just
like in Isar. Anybody on this mailing list will immediately deduce from
my previous mention of PG that I am talking about the user interface to
Isabelle. This is known as natural language. Luckily you had no problem
to follow it, as the rest of your email clearly shows.
See also the introductory section of the new Isabelle/jEdit manual:
The subtle differences of Isabelle/ML versus Standard ML,
Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
taken into account when discussing any of these PIDE building blocks
in public forums, mailing lists, or even scientific publications.
Right now we still have the situation that people on this mailing list use
"jedit" as a sloppy shorthand for anything after Isabelle Proof General.
If this habit is continued, it will cause a lot of confusion.
For example, questions on Stackoverflow are occasionally tagged as
"isabelle" and "jedit". In the context of that forum, the natural
language wording of the text needs to be right, or people out there will
not understand what it is about. (Postings are occasionally removed for
Even just in the context of the isabelle-users mailing list, we should
soon see users of Isabelle/Eclipse and CLIDE (web front-end from Bremen),
which both use the underlying Isabelle/Scala document model. In that
sense Isabelle/jEdit is just an example application.
Not every user is required to understand all the details of the overall
PIDE architecture. Just sticking to certain names by habit is sufficient.
And the author has the natural authority to determine name and title of
his own work.
This archive was generated by a fusion of
Pipermail (Mailman edition) and