Re: [isabelle] Basic IsarToLatex markup completed
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Basic IsarToLatex markup completed
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Fri, 30 Nov 2012 23:04:22 -0600
- In-reply-to: <alpine.LNX.firstname.lastname@example.org>
- References: <50B6CB7C.email@example.com> <alpine.LNX.firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
On 11/30/2012 5:03 PM, Makarius wrote:
Interesting what can be done with a few control symbols. It appears
to be generally in line with the "markdown" family of tools. Do you
have your own implementation somewhere on the web?
No. It's just me hacking around with the scripting language of WinEdit,
which is a LaTeX editor with it's own flavor of regular expressions:
Consequently, the scripts aren't suitable for public distribution for a
product that's tied into jEdit. I'd like to switch over to jython, so I
can give Isabelle users any scripts I write, but that's not going to
happen for a long time.
I'm also not motivated at this time to get anyone to do anything that
creates forks off of what's being done using only the official
distribution. And there's plenty of time to wait, because I'll be making
lots of additions and changes as I use what I'm doing more and more. For
example, I only had a long form for \eqref, like Equation <ymdhMMa>, and
I've added a short form, like <Eq`ymdhMMa>, so that only the equation
number gets printed.
This ties into what Christian Sternagel said in the message thread that
preceded this one, that if possible, it's best to get features
You can have anything you want of what I've done. To give you the
scripts, I would probably have to zip up the WinEdit executable so you
could figure out how the scripting language works, along with using the
What I don't want to publicly distribute right now is my "Greek theme
layout". I'd like to use it a while before I give people the LaTeX
sources, not that people couldn't easily figure out what I'm doing.
What I'm doing is a 3900 line LaTeX preamble, with a ton of clutter and
commented lines, and a 825 line WinEdit script, which is at least half
I would have never got the idea to make a subscripted ASCII prime.
Such things depend a lot on the actual font being used, though.
It wasn't obvious to me, but you made it available as an identifier
character, and one thing led to another. For markup tags, the
subscripted reverse tick, `, is an excellent character, at least with
the default jEdit font on Windows 7. A subscripted ` and subscripted '
are distinguishable, whereas, a subscripted ' looks the same as lots of
other subscripted characters.
But you bring up a good point that hasn't occurred to me, that all my
choices of subscripted characters, though I can distinguish them with my
font, other people might not be able to.
With Isar identifiers, using subscripted ' is not a problem because
there are only a few non-alphabet or non-numeric characters that can be
used, but there are a bunch of different subscripted characters that
make a small little dot, and people should be able to know what
character they're looking at.
So maybe I'll put some thought into trying to get away from using
subscripted ', `, and *.
Which spellchecker are you using here? Are you satisfied with it? At
some point I would like to wire-up a reasonably good one with
Isabelle/jEdit in a way that it knows about the formal vs. informal
parts of the text. So it won't hilight the formal option "SAT4J", for
I use the VoxSpell plugin: http://plugins.jedit.org/plugins/?VoxSpell
It comes with a dictionary. I tried the SpellCheck plugin, which can use
Aspell and several other dictionaries, including VoxSpell, if I remember
VoxSpell is the only one that checks your spelling as you type. Yea, I
like it. You can't edit its dictionary directly, so I couldn't figure
out how to remove a word from its dictionary, after I had added, but if
you've added an underlined word, such as "word", if you right click on
"word", there's an item in the menu which says "reset 'word'".
...but not to be done if unnecessary. These days, most people don't
expect HTML pages to be converted to TXT files.
At some point I would like to see the Isabelle/Isar sources rendered
nicely in HTML, based on similar pseudo-markup symbols as you have
here, or like a variant of Markdown that is using non-ASCII characters.
Luckily Isabelle has an infinite amount of \<foo> symbols to play
with, and they can be assigned to Unicode glyphs on demand.
As far as interface, I try not to make any requests, since you were way
ahead of everyone anyway. I'm sure the HTML feature will be useful, but
it's not like I need to wait on it to get what I need now. The basics of
what I need now is pretty much there, and I didn't do anything.
I will make a pseudo-request, but first, you mention our ability to add
\<foo> commands to our etc/symbols, and that ties into a fundamental
rule I try to follow which is, "Try to never require anything of another
Isabelle user other than the default distribution".
So, if I put new \<foo>s in my etc/symbols that I use for markup tags,
then other people will need to use my etc/symbols file to see what I
see, and I can be pretty sure that no one will want to do that.
This leads into the \<^isub> command. What I want is not just characters
for markup tags, but subscripted characters. Your point is good about
the possibility of subscripted primes not being distinguishable under
certain fonts, but subscripted \<rhd>, \<lhd>, \<lless>, and
\<ggreater>, which I'm using for equations, would probably work under
Here are three things that would make for safer markup:
1) You leave \<^isub> and \<^isup> in Isar.
2) They and the character that follows them get ignored, other than the
fact that the character gets subscripted or superscripted.
3) They're highlighted different than the characters following \<^sub>
Without item three, it might just end up confusing people, if they're
trying to figure out what the markup tags are. Is it \<^isub>' or
\<^sub>'? You wouldn't be able to tell.
That's not a request. It's merely a pseudo-request. I wouldn't know
This archive was generated by a fusion of
Pipermail (Mailman edition) and