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 such reasons.)

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 MHonArc.