Re: [isabelle] Basic IsarToLatex markup completed

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 implemented officially.

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 help file.

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 commented lines.

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 example.

I use the VoxSpell plugin:

It comes with a dictionary. I tried the SpellCheck plugin, which can use Aspell and several other dictionaries, including VoxSpell, if I remember right.

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 most fonts.

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> and \<^sup>.

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 what's best.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.