Email Gateway (Aug 19 2022 at 12:32): Email Gateway (Aug 19 2022 at 12:32):From: Tobias Nipkow <nipkow@in.tum.de>
In ProofGeneral, numerals of type 'a are explicitly flagged with their type in
the output. It is an incredibly useful little feature, not just but in
particular for novices. Which is why we introduced it. Any reason not to have it
with jedit as well?
Tobias
Email Gateway (Aug 19 2022 at 12:32):From: Makarius <makarius@sketis.net>
On Mon, 18 Nov 2013, Tobias Nipkow wrote:
In ProofGeneral, numerals of type 'a are explicitly flagged with their
type in the output. It is an incredibly useful little feature, not just
but in particular for novices. Which is why we introduced it.
I introduced that feature many years ago, and even the idea to make a
constraint as "inlined warning" to give it the proper syntactic context.
(An explicit warning message within syntax translations technically does
not work, even today, and even though I've seen this occasionally in other
syntax translations over the years.)
Any reason not to have it with jedit as well?
You mean Isabelle/jEdit, or rather the Isabelle/Scala document model
behind it; jEdit is just a plain text editor.
The reason why the constraint is not immediately visible in the output is
the much richer term markup introduced in Isabelle2013:
* Configuration option show_markup controls direct inlining of markup
into the printed representation of formal entities --- notably type
and sort constraints. This enables Prover IDE users to retrieve that
information via tooltips in the output window, for example.
The old TTY / ProofGeneral behaviour can be recovered by something like
this:
declare [[show_markup = false]]
but this also looses the benefit of constraints that can be retrieved as
tooltips on demand.
To make further progress, without looking back on old features, there are
two things in the pipeline for quite some time (and with some priority):
* Highlighting of places in terms where extra polymorphism is
introduced. (Users are more often confused about basic type-inference
than just the special case of 0, 1, etc.)
* Routine printing of terms with just the right amount of type/sort
constraints, such that the result is uniquely determined.
Makarius
Email Gateway (Aug 19 2022 at 12:33):From: Tobias Nipkow <nipkow@in.tum.de>
Am 18/11/2013 12:12, schrieb Makarius:
On Mon, 18 Nov 2013, Tobias Nipkow wrote:
In ProofGeneral, numerals of type 'a are explicitly flagged with their type in
the output. It is an incredibly useful little feature, not just but in
particular for novices. Which is why we introduced it.I introduced that feature many years ago, and even the idea to make a constraint
as "inlined warning" to give it the proper syntactic context. (An explicit
warning message within syntax translations technically does not work, even
today, and even though I've seen this occasionally in other syntax translations
over the years.)Any reason not to have it with jedit as well?
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.
Tobias
The reason why the constraint is not immediately visible in the output is the
much richer term markup introduced in Isabelle2013:* Configuration option show_markup controls direct inlining of markup
into the printed representation of formal entities --- notably type
and sort constraints. This enables Prover IDE users to retrieve that
information via tooltips in the output window, for example.The old TTY / ProofGeneral behaviour can be recovered by something like this:
declare [[show_markup = false]]
but this also looses the benefit of constraints that can be retrieved as
tooltips on demand.To make further progress, without looking back on old features, there are two
things in the pipeline for quite some time (and with some priority):* Highlighting of places in terms where extra polymorphism is
introduced. (Users are more often confused about basic type-inference
than just the special case of 0, 1, etc.)* Routine printing of terms with just the right amount of type/sort
constraints, such that the result is uniquely determined.Makarius
Email Gateway (Aug 19 2022 at 12:35):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 19 2022 at 12:35):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 19 2022 at 12:36):From: Makarius <makarius@sketis.net>
This is getting a bit ridiculous.
I have already seen papers related to the Prover IDE efforts, where
"jedit" was used in a non-sensical way, even more non-sensical then on
this thread so far.
Is this the end of proper science?
Makarius
Email Gateway (Aug 19 2022 at 12:36):From: Tobias Nipkow <nipkow@in.tum.de>
Am 20/11/2013 16:20, schrieb Makarius:
On Wed, 20 Nov 2013, Tobias Nipkow wrote:
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.
This is getting a bit ridiculous.
I am so glad we finally agree :-)
Tobias
I have already seen papers related to the Prover IDE efforts, where "jedit" was
used in a non-sensical way, even more non-sensical then on this thread so far.Is this the end of proper science?
Makarius
Last updated: Nov 21 2024 at 12:39 UTC