Re: [isabelle] 0::'a




Am 20/11/2013 13:14, schrieb Makarius:
> 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.

I recommend PRISM to identify offenders.

Tobias

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




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