Email Gateway (Aug 19 2022 at 09:06): Email Gateway (Aug 19 2022 at 09:06):From: Makarius <makarius@sketis.net>
In such cases the correct answer on this list is like "the issue has been
addressed recently, so it will probably be in the next release", without
specific references to certain changesets.
isabelle-dev is the mailing list for following the ongoing development
process (usually with changeset ids).
isabelle-users for everything else, including Isabelle/ML in user space
(without changeset ids).
Makarius
Email Gateway (Aug 19 2022 at 09:06):From: Lars Noschinski <noschinl@in.tum.de>
Which is just what Johannes did in his first mail.
-- Lars
Email Gateway (Aug 19 2022 at 09:06):From: Makarius <makarius@sketis.net>
Yes, you are right. Only later he got confused by my anseer and added the
changeset id to the thread on isabelle-users, probably because I always
insist in doing this on isabelle-dev.
Let's hope we all get more proficient in the semantic models behind of the
two mailing lists.
Makarius
Email Gateway (Aug 19 2022 at 09:18):From: Joachim Breitner <mail@joachim-breitner.de>
Dear List,
I often use sorry when doing my proofs top-down; and then I later need
to find them again. I found out about Ctrl-, to search, but it would be
more convenient if sorry were prominently highlighted, e.g. in red. This
would give me continuous feedback about how far I am with my proof.
Can I easily configure that myself? Also, please consider making that
the default, I’d say others profit from that as well.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 09:18):From: Lars Noschinski <noschinl@in.tum.de>
There is the highlighter plugin which you can use to highlight arbitrary
text in colors of your choosing.
-- Lars
Email Gateway (Aug 19 2022 at 09:19):From: Johannes Hölzl <hoelzl@in.tum.de>
In the development version of Isabelle is sorry already highlighted with
a light red background. It is not (yet?) reflected at the scrollbar like
it is done with errors and warnings.
- Johannes
Email Gateway (Aug 19 2022 at 09:22):From: Makarius <makarius@sketis.net>
I am still working on what will become the next official release of
Isabelle/jEdit eventually.
There is not "the" development version, and its change history is not
necessarily monotonic in the semantic sense, so "yet" above also does not
apply. One needs to understand that being hooked on Isabelle repository
versions means that you follow the waves of changes of the day or the
week.
You are welcome to do so and report anything you observe on the
isabelle-dev mailing list -- with proper changeset ids (abbreviated SHA1
keys) since this is the only thing that does not change over time, and
tells unambigously what is your "current" version.
Makarius
Email Gateway (Aug 19 2022 at 09:24):From: Makarius <makarius@sketis.net>
On Fri, 16 Nov 2012, Johannes Hölzl wrote:
Ah, my statement was not intended to be an actual observation of the
Isabelle repository. As the question was asked on isabelle-users I
assumed that Joachim does not run the development version of Isabelle
and I wanted to give him an glimpse of a possible future release of
Isabelle.
"Possible future" is the historically correct term, but predictions are
hard, especicially about the future. Here on isabelle-users the
assumption is that people are working with real releases, and are not
engaging in the painful path between them, where things might come and go
in non-monotonic ways.
But to store the information for the archive: in revision a3bede207a04
of the repository Isabelle/jEdit nicely marks "sorry" in red :-)
Quotation of changeset ids only makes sense on the isabelle-dev list,
which is about ongoing moves. The most basic syntactic criterion to
distinguish the two mailing lists (approximatvively) is this:
* isabelle-users: everything you ever wanted to know, but were afraid to
ask, about working with official Isabelle releases (lets say approx. the
2-3 most recent ones for serious work, older ones for historical
anecdotes)
* isabelle-dev: discussion over changes (with proper changeset ids) and
administrative chores around the development process etc.
Makarius
Email Gateway (Aug 19 2022 at 09:24):From: Makarius <makarius@sketis.net>
I also want to add something productive here: the Highlighter (and
Hypersearch) are big assets of jEdit. I use them all the time for many
things.
The regex language accepted here is that of Java, see
http://docs.oracle.com/javase/6/docs/api/java/util/regex/Pattern.html
This allows very nice things like word context \b. So for 'sorry' the
pattern would be like this:
\bsorry\b
Makarius
Email Gateway (Aug 19 2022 at 09:25):From: Tobias Nipkow <nipkow@in.tum.de>
Just to be clear on that: reports from the development front are welcome here,
in particular as a reply to a question/suggestion.
Tobias
Last updated: Apr 30 2024 at 04:19 UTC