[isabelle-dev] html output of theories

[Gottfried Barrow]

On 14-04-14 06:37, Makarius wrote:
> On Mon, 14 Apr 2014, John Wickerson wrote:
>
>> ...so I have no interest in a boring monochrome paginated PDF -- I 
>> just want my theory to look like it does in Isabelle/jEdit, but with 
>> the antiquotations properly rendered.
>
> That alone is just an omission of current Isabelle/jEdit.  I've come 
> across this a few times recently, so expanded antiquotations are 
> likely to become part of the PIDE document model eventually.  (A 
> technical snag is that the current programming interface for document 
> antiquotations is for generating raw Latex source.)

Makarius,

This discussion between you and John is related to a user list email 
that I will probably will reply to. The particular sentence above is 
100% related to what I was going to explain about what I need with 
antiquotations.

There gets too much to explain by text, and I'll explain a little back 
on the user list, but here's what's in my mind, in case it's not already 
in your mind, where I assume that many times, what ideas I have, you 
already have, but even better, and even had them a long time ago. Here's 
what I think I need:

(1) Expand an antiquotation in the PIDE, as you've mentioned, where the 
antiquotation command gets hidden, and replaced by its graphical 
counterpart.

(2) Provide the option to save both the antiquotation command and the 
expanded content to file.

If you don't provide (2), then expanded antiquotations in the PIDE don't 
do me any good.

If you do provide (2), then I will never have a need to use 'isabelle' 
for for its LaTeX processing ability. I will only need 'isabelle' for 
other things, like to formally check my logic, build graphs, etc.

I state some facts:

(F1) For my needs, I can either heavily edit your 'isabelle' LaTeX 
preamble, followed by some heavy scripting, or I can completely create 
my own preamble as part of some heavy scripting. Using 'isabelle', for 
my needs, would still require a lot of extra work from me to process the 
input and output.

(F2) Fact F1 is wrong. After using the 'isabelle' PDF build to get its 
benefits, I would still have to do a second LaTeX build after processing 
your the TeX files 'isabelle' created.

(F3) Fact F1 is wrong because I have to be able to put anything in a THY 
inside a fncyvrb Verbatim. I'll mention that again if I respond on the 
other list. I tried it in 2011-1, and I couldn't do it. I have an idea 
of how to do it now, which is to pull everything out of Verbatim, run 
'isabelle', put it back in 'verbatim', then run it through MiKTeX.

Now for a rule:

(RULE1) Do not do something that may be beneficial in the short term but 
ties you into something for the long term you don't want to be tied into.

That "something" is Cygwin texlive. Cygwin like you're using, as a fast 
form of Unix for Windows, is an amazing thing, but I don't see texlive 
ever being supported like the native Windows LaTeX distributions, such 
as MiKTeX. I did run Cygwin-Latex-Setup.bat, and it did an effortless 
setup. However, there's the magic retrieval  of packages I get with 
MiKTeX. Also, I use portable MiKTeX because I got tired of continually 
doing setup for a LaTeX distribution.

(SIDENOTE: In looking at Cygwin-Latex-Setup.bat, possibly I could add 
what packages I need to the batch file.)

(RULE2) Concede where possible. Concrete application: PDF vs. HTML.

For lengthy comments, I would explain to John Wickerson why I'm very 
happy to tolerate "boring monochrome paginated PDF". It's all what a 
person needs. When Mac guys have all their needs met by Macs, and 
Windows guys by Windows, that's the best possible scenario. I'm 100% 
electronic with documents, and it's 100% related to PDF bookmarks, and 
the PDF bookmark tree. They're already there many times, I can edit 
what's there, and I can create my own bookmarks. Without a tree view to 
get a global view of what's in a book, reading books electronically 
wouldn't be a 100% solution. I gave up trying to edit other people's 
HTML. There are also two other important features. A PDF is a single 
document, and it's predictable.

I also quit saving web pages using HTML. It's that single document 
thing. There's no standard for HTML as a single document. Windows 
Internet Explorer can do it, but then I would get tied into Internet 
Explorer.

But, HTML is also 100% important. I frequently rip complete sections of 
web sites to get the HTML documentation (with GetleftToGo). PDF for one 
thing, HTML for another. I'm definitely for other people doing the hard 
work to make the unpredictability of HTML predictable.

On 14-04-14 05:01, Makarius wrote:
> I've recently started to think about adding a bit of Markdown 
> (https://daringfireball.net/projects/markdown) to the 'text' syntax in 
> a conservative way, such that there is no LaTeX required for basic 
> things like itemize/enumerate/description, and it also looks better in 
> the editor.

The word count in this email is already too high, and the only reason I 
showed up was to state what's at the top about (1) and (2).

I speculate that you're very conservative about changing Isar because of 
the the principle of RULE1.

You mentioned markdown a while back, and now I understand it. Like any 
word, the meaning of "markdown" is going to fragment over time. Now that 
certain markdowns are standardized, used officially by sites like 
Stackoverflow, is markdown the workaround that it used to be? I say no, 
but that's only a side comment.

For myself, I consider what I'm doing as markdown because it's an 
unsupported, unorthodox use of how syntax is used in a THY.

If you added one, single, subscript command, that is reserved for users 
to do anything they want to do with it, then what I'm doing would cease 
to be markdown, and it would become markup. That's my opinion again, 
which is not important here.

I speculate further that you won't do that because any markup needs to 
fit into a long term grand plan, and certain quick hacks would be bad 
for the grand plan.

What I say is that markup which is visible, but subtle, might be 
something that should be an option for the long term, even if a very 
complete and sophisticated markup is implemented in the PIDE.

The graphical notation of Mathematica is great if you've gone through 
the lengthy learning curve to be able to use the 100 or so escape 
sequences. I set out several times to go through the learning curve. It 
was my last attempt which led me to functional programming in 
Mathematica, which led me to proof assistants. The rest is history. My 
perspective here comes from wanting to easily enter math notation in 
Mathematic, but it never being easy. The options are graphical pallets, 
which is typing with a mouse, or memorizing key sequences.

Visible, but subtle, subscripted, graphical characters to mark the 
beginning and end of a markup command are self-documenting. You have to 
know how to subscript a character, and you have to know the command for 
the sub-scripted symbol that you see. It cuts down on the learning curve.

I'm not dependent on any of this, except what I said about (1) and (2). 
Even for those, I already have a workaround in mind to be able to expand 
antiquotations in the PIDE. If I have to do the work, that's okay. If it 
gets done before I get around to it, that's good, too.

I do my best to stay off of this list, but you don't like cross-posting. 
I'm checking out of this, unless there's a good reason why I shouldn't.

Regards,
GB