Email Gateway (Aug 19 2022 at 08:46): Email Gateway (Aug 19 2022 at 08:46):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
For subscripts I never use \<^bsub> and \<^esub>. They don't work on
Cygwin anyway, and I'm too lazy to fire up the VirtualBox Linux to find
out if that's true in Linux.
It actually turns out for the better, because subscripting more than two
letters is to be minimized, which means I only normally use two \<...>
commands anyway, plus \<^isub> works everywhere, and "-_" is easier to type.
However, I am now using \<^bold> in the notes of my comments, or in
section headings. To move fast, I'm writing notes using the Isar \<...>
symbols to get some better formatting in jEdit, which make my notes more
readable for me.
Consider this heading:
section{*\<paragraph> T\<^bold>h\<^bold>e
\<^bold>A\<^bold>x\<^bold>i\<^bold>o\<^bold>m \<^bold>o\<^bold>f
\<^bold>E\<^bold>x\<^bold>t\<^bold>e\<^bold>n\<^bold>s\<^bold>i\<^bold>o\<^bold>n
\<paragraph>*}
That says, "The Axiom of Extension". The bold makes it stand out when
I'm scrolling down through a THY, but the additional characters make it
hard to read in the Sidekick panel.
At this very moment, I have a bulleted list, and I would like the first
phrase of my bulleted item to be bold. To do that, I have to go into my
other editor, go to the line, highlight the text, and use a script to
put a \<^bold> in front of every letter.
It's just an idea, this \<^bbold> and \<^ebold>. Wants are insatiable.
Editors which already have lots of features are very tolerable.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:49):From: Makarius <makarius@sketis.net>
On Mon, 10 Sep 2012, Gottfried Barrow wrote:
For subscripts I never use \<^bsub> and \<^esub>. They don't work on
Cygwin anyway, and I'm too lazy to fire up the VirtualBox Linux to find
out if that's true in Linux.
What exactly means "don't work" here? In Isabelle/jEdit these control
symbols should be shown uniformly as diagonal arrows, without any attempt
to make any sub- or superscripting.
It actually turns out for the better, because subscripting more than two
letters is to be minimized, which means I only normally use two \<...>
commands anyway, plus \<^isub> works everywhere, and "-_" is easier to
type.
BTW, there is also C-e DOWN. Next time I will make that operate on the
text selection as well, for convient superscripting of text ranges,
without the conceptual problems of \<^bsub> and \<^esub>.
However, I am now using \<^bold> in the notes of my comments, or in
section headings. To move fast, I'm writing notes using the Isar \<...>
symbols to get some better formatting in jEdit, which make my notes more
readable for me.Consider this heading:
section{*\<paragraph> T\<^bold>h\<^bold>e
\<^bold>A\<^bold>x\<^bold>i\<^bold>o\<^bold>m \<^bold>o\<^bold>f
\<^bold>E\<^bold>x\<^bold>t\<^bold>e\<^bold>n\<^bold>s\<^bold>i\<^bold>o\<^bold>n
\<paragraph>*}That says, "The Axiom of Extension". The bold makes it stand out when I'm
scrolling down through a THY, but the additional characters make it hard to
read in the Sidekick panel.At this very moment, I have a bulleted list, and I would like the first
phrase of my bulleted item to be bold. To do that, I have to go into my other
editor, go to the line, highlight the text, and use a script to put a
\<^bold> in front of every letter.It's just an idea, this \<^bbold> and \<^ebold>. Wants are insatiable.
Editors which already have lots of features are very tolerable.
Actually, the Isabelle symbols where never meant to be used in informal
text, only in formal one. Normally you do document markup in LaTeX, where
you would use \textbf{...} as usual. This does not mean there could not
be any reforms, but how long it will take is unspecified.
Just last week I was preparing some slides in Isabelle, and found the
traditional latex batch-run quite cumbersome, so the obvious thing is to
renovate the HTML presentation instead and make it render on the spot in
real-time in Isabelle/jEdit (lets say in some Preview panel).
My main concern at the moment is to find good in-text representation of
list environments; bold, emphasize, or even text colors would be obvious
extensions. Apart from implementation efforts, an open question is how to
spell this out in the source text. Maybe a reduced version of Markdown?
But the whole thing needs to be conservative over the embedded LaTeX in
Isabelle theories.
Ultimately, jEdit is a simple texteditor, so questions remain how far it
can be stretched without breaking down.
Makarius
Email Gateway (Aug 19 2022 at 08:49):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/12/2012 1:34 PM, Makarius wrote:
What exactly means "don't work" here? In Isabelle/jEdit these control
symbols should be shown uniformly as diagonal arrows, without any
attempt to make any sub- or superscripting.
Markarius,
So it works after all. That's what it's doing.
BTW, there is also C-e DOWN. Next time I will make that operate on
the text selection as well, for convient superscripting of text
ranges, without the conceptual problems of \<^bsub> and \<^esub>.
Thanks for the tip.
Actually, the Isabelle symbols where never meant to be used in
informal text, only in formal one. Normally you do document markup in
LaTeX, where you would use \textbf{...} as usual. This does not mean
there could not be any reforms, but how long it will take is unspecified.
So in that case, I appeal to formal use only, such as \<^ibold> to
signify that a variable is a vector. We all know how we'd be in a world
of hurt without vectors, and how a vector is represented either with an
overhead arrow, or with bold.
I say more about LaTeX markup vs. jEdit markup in the other reply.
Ultimately, jEdit is a simple texteditor, so questions remain how far
it can be stretched without breaking down.
I reduce my requests. The commands \<^iitalic> and \<^ibold>, that's all
I'm asking for now. I address the italic issue in the other reply.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:49):From: Makarius <makarius@sketis.net>
On Wed, 12 Sep 2012, Gottfried Barrow wrote:
So in that case, I appeal to formal use only, such as \<^ibold> to
signify that a variable is a vector. We all know how we'd be in a world
of hurt without vectors, and how a vector is represented either with an
overhead arrow, or with bold.
This can be done just with \<^bold> -- after the next reform of special
identifier notation. (Although Proof General users will complain, because
\<^bold> has never worked there on the display.)
BTW, old-fashioned continental European vectors would be written in
Fraktur 𝔵𝔶𝔷which is already there, but that is a bit difficult to
read even for Germans.
I reduce my requests. The commands \<^iitalic> and \<^ibold>, that's all
I'm asking for now. I address the italic issue in the other reply.
So what is your application for \<^italic> in identifiers?
Makarius
Email Gateway (Aug 19 2022 at 08:49):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/12/2012 2:43 PM, Makarius wrote:
So in that case, I appeal to formal use only, such as \<^ibold> to
signify that a variable is a vector. We all know how we'd be in a
world of hurt without vectors, and how a vector is represented either
with an overhead arrow, or with bold.This can be done just with \<^bold> -- after the next reform of
special identifier notation. (Although Proof General users will
complain, because \<^bold> has never worked there on the display.)
Thanks. Did I not say, "Makarius has probably already thought about all
of this"?
BTW, old-fashioned continental European vectors would be written in
Fraktur 𝔵𝔶𝔷which is already there, but that is a bit difficult to
read even for Germans.
Being mono-lingual, to compensate, it is important that Americans be
well-versed in European trivia.
I reduce my requests. The commands \<^iitalic> and \<^ibold>, that's
all I'm asking for now. I address the italic issue in the other reply.So what is your application for \<^italic> in identifiers?
You may have read my other email by now, but I make my argument again.
It's purely to have another option for me to mark up a THY so that it's
more readable for me. I spin here the "educational use of Isabelle like
that of Mathematica". When THYs can be marked up to be very readable in
their own right, then there's the possibility of passing around THY
files in an educational setting, although that's not the purpose of my
request.
I just want to be able to read the mathematics that I'm writing in
jEdit, without having to resort to LaTeX. At a certain point, the
technical hassles can kill your inspiration.
I don't know how important it would be for me to italicize variables so
that they have a traditional look in jEdit. If all you have to do is add
\<iitalic> in the identifier specification and in one ML file, it's my
opinion that wouldn't be an unacceptable expansion of Isar, but that's
me, and you didn't ask my opinion.
Regards,
GB
Last updated: Apr 25 2024 at 01:08 UTC