[isabelle-dev] html output of theories
igbi at gmx.com
Mon Apr 14 16:17:49 CEST 2014
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.)
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
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
(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
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.
More information about the isabelle-dev