Email Gateway (Aug 19 2022 at 08:38): Email Gateway (Aug 19 2022 at 08:38):From: Makarius <makarius@sketis.net>
On Thu, 13 Sep 2012, Gottfried Barrow wrote:
I was using LaTeX to produce a readable document. Recently, I broke my
LaTeX build script, and before I got it fixed, I said, "Forget LaTeX
right now. I have 500 pages of theorems I have to implement, and if I
can't make it all work, then it's worthless to make something look good
that's worthless."
I've recently seen myself doing "drafting" directly in the editor buffer,
with its slightly improved rendering quality in the last 12 months or so.
The jEdit print operation also produces suprisingly good results with the
IsabelleText font.
I attach a screen shot. How would it print out with LaTeX? It would look
terrible, I'm sure, but that's not the purpose. If I want to print it, I
can print it out with a regular printer driver. But I read everything in
electronic form, so I always need a tree view, and Sidekick gives me
that in jEdit.
The LaTeX appearance is defined by the .sty files you provide to render
it. The default isabelle.sty would make inlined comments with "--" look
unsatisfactory, for example. Normally you use the 'text' command for
larger paragraphs of semi-formal text.
What is the purpose of the paragraph signs in your source (in the
'section' command)?
Makarius
Email Gateway (Aug 19 2022 at 08:39):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/17/2012 8:31 AM, Makarius wrote:
The LaTeX appearance is defined by the .sty files you provide to
render it. The default isabelle.sty would make inlined comments with
"--" look unsatisfactory, for example. Normally you use the 'text'
command for larger paragraphs of semi-formal text.
As to why I use --"......" instead of "text{....}", (....), and
--{...}, that gets into the analysis of what I'm trying to accomplish
in my first phase of editing a THY file. I'm always happy to analyze things.
My source code editing method could partially described with these
phrases: "readability", "absorb information fast", "get around fast",
"don't let the code get so unwieldy you don't know what's there", and
"always have an idea of where you're at in the code on an outline level".
What is the purpose of the paragraph signs in your source (in the
'section' command)?
The purpose is just visibility, so that as I'm scrolling down through a
document fast, I can see when there's a sectioning command, and I can
see at what level it's at, that is, whether it's section, subsection, or
subsubsection. One paragraph symbol means "section". Three paragraph
symbols means "subsubsection".
Graphics can, many times, help us absorb a lot more information, and
absorb it faster than reading text.
Here's where someone might think I would make a request of you. I could
request that you hide the syntax "section{*", and based on command
context, make the words inside "section{.....}" bold.
But if you lock me into them, I might not like your decisions on font
style and font size. Mathematica is highly customizable, but at some
point it becomes, "I just want something that's basic, functional, looks
decent, and doesn't require me to give people a style document."
As it is, I'd rather be working in jEdit as I am now than in Mathematica.
I'm still experimenting, but there are three types of information that I
want to find and recognize fast:
1) Sectioning: what level a section command is at, and what the heading
says, both when scrolling and when looking at the Sidekick panel.
(a) I do that as shown by the attached images; that is, using a
--"...." command with bold text for scrolling through the text, and
immediately followed by a sectioning command underneath it for the
Sidekick panel. I have to have two. I can't read the title in Sidekick
if it's full of \<bold> symbols.
2) The start of textual exposition, or text notes under theorems and
other keywords.
(a) I do that with \<bullet> and some scientific amount of
indentation, which I haven't locked in yet.
3) Toplevel keywords such as theorem, definition, syntax, notation, and
definition.
(a) I'm still experimenting. For example, the blue and boldfaced
keyword "theorem" is not enough to make it stand out from lots of other
keywords in its vicinity. I'm currently experimenting with this for
unnamed theorems, like this:
theorem --"\<^bold>(*\<^bold>) What the theorem does starts
here..."
With that, I can also replace "*" with a number, if needed, so that I
can reference it within a section.
I'm still looking for a more perfect symbol than "*". \<bullet> is not
vertically centered in the "( )", and "*" doesn't stand out enough. I
try things like \<^bold>(\<^bold>\<^bold>). I need to identify theorems
quick when they're interspersed with a bunch of bulleted text. But now,
I'm in realm of "personal tweaking".
To find something that works, looks good, and helps me see it and
recognize it fast, that takes a lot of experimenting. For my other
editor for LaTeX, I put a massive amount of work into syntax
highlighting and making trees in a sidepanel.
The "looking good" is not an unimportant part of it. It's for myself,
but I don't like looking at obnoxious, gaudy looking code.
I need dark, black symbols to stand out, like \<bullet> and
\<paragraph>, but there's not a lot of them available. I used
\<spadesuit> for a while in place of \<paragraph>, but it got on my nerves.
Simplicity and full featured is a hard balance to find. The \<bold> for
use in identifiers will be a huge addition. I'll just grow with whatever
you add, and hope you don't force something on me that doesn't look good
to me, but if you do, I'll live with it.
Oh yea, as to why I don't use "text{......}". I don't like seeing
"text", and --"....." only uses 4 characters instead of 8 characters.
Of the options available for writing notes, it looks the best, but I do
resort to --{*.....*} if I need to do lots of quoting using double
quotes.
Both "text{....}" and --"....." make the background grey, and I would
turn that off if I could. An example of "I live with it", because it's
not a problem. The grey is a little too dark on my laptop monitor, but I
mainly have jEdit on my external monitor.
If I ever do need to covert everything to use "text{.....}", I'll just
go through lots pain and agony.
The image attachments show how I'm trying to balance the need for
reading information in Sidekick with "reading when scrolling", all
without ending up with something ugly or obnoxiously cluttered up, and
where different symbols and formatting makes the 3 different categories
stand out in 3 different ways.
Regards,
GB
sectioning_paragraph_marks.png
trying_to_emphasize_theorem.png
Email Gateway (Aug 19 2022 at 08:40):From: Makarius <makarius@sketis.net>
On Mon, 17 Sep 2012, Gottfried Barrow wrote:
As to why I use --"......" instead of "text{....}", (....), and
--{...}, that gets into the analysis of what I'm trying to accomplish in my
first phase of editing a THY file. I'm always happy to analyze things.My source code editing method could partially described with these
phrases: "readability", "absorb information fast", "get around fast",
"don't let the code get so unwieldy you don't know what's there", and
"always have an idea of where you're at in the code on an outline
level".
Some of these aspects are shared by projects like Markdown, which I have
encountered just recently myself, although the ideas (and tools) are
already there for several years. The idea is to write plain text with
some level of "formality", such that the immediately readable text can be
typeset in reasonable quality offline (or as preview online, like in the
"enki" editor).
I've started thinking about making Isabelle section / text / "--" follow
some Markdown principles. You have already \<bullet> symbols that
approximate a formal itemization. A bit more such things could become
standard one day.
Here's where someone might think I would make a request of you. I could
request that you hide the syntax "section{*", and based on command
context, make the words inside "section{.....}" bold.
Maybe in the next round of jEdit trickery. There is still the TokenMarker
limitation imposed by the original code base, but I might eventually
manage to get a tiny little modification accepted by the jEdit maintainers
to make font styles dependent on a semantic context, not just the plain
text you see in the buffer.
I'm still experimenting. For example, the blue and boldfaced keyword
"theorem" is not enough to make it stand out from lots of other keywords in
its vicinity. I'm currently experimenting with this for unnamed theorems,
like this:theorem --"\<^bold>(*\<^bold>) What the theorem does starts here..."
With that, I can also replace "*" with a number, if needed, so that I can
reference it within a section.
BTW, there is a semiformal "tag" concept that could be used here:
theorem %important ...
Right now these tags are mainly relevant for LaTeX output, but one could
make more of them. You can also try to be creative with non-alphabetic
tag names, although LaTeX will choke on that.
I'm still looking for a more perfect symbol than "*". \<bullet> is not
vertically centered in the "( )", and "*" doesn't stand out enough.
It seems that when merging Bitstream Vera and TeX fonts in IsabelleText,
I've got the spacing not exactly right. This is the normal situation for
a non-fontdesigner like myself tinkering with existing fonts.
Nonetheless the outcome is so much better than anything we've had in the
last 15 years, and also slightly better than STIX in many respects.
I try things like \<^bold>(\<^bold>\<^bold>). I need to identify
theorems quick when they're interspersed with a bunch of bulleted text.
But now, I'm in realm of "personal tweaking".
Personal tweaking may be perfected by assigning your own (unused) Unicode
points to (unused) Isabelle symbols in $ISABELLE_HOME_USER/etc/symbols
like this:
\<blob> code: 0x2593 font: STIXGeneral
This gives you a 75% grey shade quad, assuming you and your recipients
have that font and your etc/symbols file. Otherwhise they will see a
literal \<blob> which is also OK.
Both "text{....}" and --"....." make the background grey, and I would
turn that off if I could. An example of "I live with it", because it's
not a problem. The grey is a little too dark on my laptop monitor, but I
mainly have jEdit on my external monitor.
In the next Isabelle release, all these colors will be configurable via
user options. Then people can come up with their own "themes".
Makarius
Email Gateway (Aug 19 2022 at 08:40):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Makarius,
If you get some ideas from this that's good, but I'll do 6 things and
then back out of 5 of them.
I don't want to work with LaTeX right now, but I'm switching things
around so that I can either build a PDF through Isabelle, or through my
own scripts.
I switch to "text{...}" to use it like it's typically used, and I use
--"...." for adding comments to proofs and other syntax.
I get rid of the bullets and make more intelligent use of subsubsection.
When everything ends ups having a bullet, they lose their effect.
I use the section commands like normal; I get rid of the bold text in
the section title, and I get rid of the duplicate title.
It's worth spending some time to try and format the code so that it's
more readable in jEdit, but complexity can only be reduced so much.
Cheap imitations aren't the way to go if they complicate things too
much. LaTeX is supposed to extend things, not be duplicated.
Other than \<^bold> in identifiers, you could lock in jEdit today for 2
or 3 years, and it would be good enough.
I see on [isabelle-dev] that it's not locked in, and the speed
improvements sound good. If users can create huge theories beyond
Complex_Main, and other users can use those theories without having to
build the heap, that simplifies things. Speed can solve a lot of problems.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:46):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I might as well attach related requests, which would be a request for a
set of italic commands, like:
\<^iitalic>, \<^bitalic>, and \<^eitalic>,
where \<^iitalic> would be a command that could be used in an
identitifer, like \<^isub> and \<^isup>.
And I might as well request
\<^ibold>,
for things like vectors and special sets.
I'm sure Makarius has already thought of all this, and either doesn't
have time to do it, or has already decided he doesn't want to do it,
maybe because it can't be practically done.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:49):From: Makarius <makarius@sketis.net>
Implementing, maintaining, discontinuing features is all very time
consuming -- with increasing efforts on this scale. The \<^sub> \<^isub>
\<^bsub> \<^esub> varieties emerged in historic sitations. Even now it
should be possible to get there with \<^sub> alone in most applications,
but it needs work to untangle all that.
In formal text italic style does not make much sense, because the formal
text is implicitly "italic" already. You see this when printing in LaTeX
in the "best style" \isabellestyle{it} that imiates Don Knuth as best as
possible. If you need "non-italic" special styles, you can define your
own symbols like \<sin> \<cos> \<tan> and render them in LaTeX as usual.
In informal text, one could think of bold and italic in the sense of
Markdown. What is a good notation for that? It needs to co-exist with
regular latex macros.
Makarius
Email Gateway (Aug 19 2022 at 08:49):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/12/2012 1:43 PM, Makarius wrote:
From the other email of yours:
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).
From this email:
In formal text italic style does not make much sense, because the
formal text is implicitly "italic" already. You see this when
printing in LaTeX in the "best style" \isabellestyle{it} that imiates
Don Knuth as best as possible. If you need "non-italic" special
styles, you can define your own symbols like \<sin> \<cos> \<tan> and
render them in LaTeX as usual.
In informal text, one could think of bold and italic in the sense of
Markdown. What is a good notation for that? It needs to co-exist
with regular latex macros.
Markarius, I'm not using your tool the same way you use it.
To summarize, what I'm trying to get even more is a "logical Mathematica
thing". Ultimately, I don't have to have \<iitalic> and \<ibold>, my use
of jEdit as a "Mathematica thing" is already happening.
I quoted from the last email because that applies, although not the
"preview", though that sounds like a good thing. I want to write like
I'm writing in a word processor, and that's what I'm already doing.
My marked up THY file is what I'll call a pre-LaTeX version. LaTeX is
compile, compile, compile, and compile after every few changes to
prevent having to track down errors. Plus, I'll spend an hour trying to
make an equation look perfect, when all I'm doing is making notes about
a textbook. That's a waste when I may delete much of what I do.
There will be what I publish for public consumption, which will be a
LaTeX product, but my preliminary markup of a THY file is for me. I need
to not get lost in the details, which is a combination of markup using
bullets and other symbols, using section headings with bold titles, and
Sidekick trees.
So \<^iitalic> is not a duplication of effort when a person is primarily
reading a theory with jEdit, rather than a PDF. Would I want to
italicize every variable in a formula? I might. I can already subscript
and superscript every variable, and put things like "\<^isub>_" in them.
I can get LaTeX without your LaTeX tools, but I can only get in jEdit
what you provide in jEdit. But what you've given is very generous.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:50):From: Makarius <makarius@sketis.net>
I think it is better to move in a presentational direction: you write the
formal text without special markup for italics, but the implicit markup as
logical identifiers that the prover provides is turned into italics
on-screen. So it would be just a continuation of the blue, green, brown
variable game with font-styles.
I did not do this so far, because jEdit cannot change the font-style once
it has been assigned statically by its token marker. It will require
another round of convincing it to do it nonetheless -- like I already did
with the text rendering as you see it in Isabelle2012.
Makarius
Email Gateway (Aug 19 2022 at 08:51):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/12/2012 3:30 PM, Makarius wrote:
I think it is better to move in a presentational direction: you write
the formal text without special markup for italics, but the implicit
markup as logical identifiers that the prover provides is turned into
italics on-screen. So it would be just a continuation of the blue,
green, brown variable game with font-styles.
It did occur to me that when "every character" is italicized, I really
don't want to be putting an \<italic> in front of "every character".
Trying to back out of that could end up being a nightmare, or really
aggravate someone else wanting to use my stuff.
It sounds like plans for even more of a Mathematica thing.
I did not do this so far, because jEdit cannot change the font-style
once it has been assigned statically by its token marker. It will
require another round of convincing it to do it nonetheless -- like I
already did with the text rendering as you see it in Isabelle2012.
Actually, with Mathematica, their document model is way more complex
than what I need, or have time to learn.
A combination of basic text editing, with an 80 character column, a few
extra symbols, some consistent formatting using your comment command
--"........", and section headings, are good enough to make things
readable. The math formulas are pretty much readable by default.
With Isabelle2011, I was using LaTeX to produce a readable document.
Recently, I broke my LaTeX build script, and before I got it fixed, I
said, "Forget LaTeX right now. I have 500 pages of theorems I have to
implement, and if I can't make it all work, then it's worthless to make
something look good that's worthless."
I attach a screen shot. How would it print out with LaTeX? It would look
terrible, I'm sure, but that's not the purpose. If I want to print it, I
can print it out with a regular printer driver. But I read everything in
electronic form, so I always need a tree view, and Sidekick gives me
that in jEdit.
Regards,
GB
jEdit_mathematica_thing.png
Last updated: Apr 25 2024 at 08:20 UTC