On 14-04-16 07:47, Makarius wrote:
I started recently to wonder about the question of latex installations
on Windows. Is MikTeX *the* thing to look at? There also seems to be
a Windows version of TeXlive, but maybe that is just an odd minority
thing?
I did a search on "windows latex distrib
On Tue, 15 Apr 2014, Lawrence Paulson wrote:
PIDE does an awful lot already, and I’d worry about burdening it with
yet more functions.
I know what you mean. When David Aspinall started some PGEclipse
experiments 10 years ago I made jokes about it, like Eclipse being not the
darkening of the
On Tue, 15 Apr 2014, Christian Sternagel wrote:
(3) This is what we all use every day, right? So this should be most
sophisticated (and already is, I think). Presentation wise the only
negative point I can think of, is that ugly LaTeX code is mostly
unreadable in the theory-file, while I need
On Mon, 14 Apr 2014, Gottfried Barrow wrote:
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
On Mon, 14 Apr 2014, Gottfried Barrow wrote:
(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
PIDE does an awful lot already, and I’d worry about burdening it with yet more
functions.
It’s easy to get PDF from HTML, provided the quality is high enough. The other
direction does not work.
Larry
On 15 Apr 2014, at 09:51, Christian Sternagel wrote:
> On 04/14/2014 12:01 PM, Makarius wro
On 04/14/2014 12:01 PM, Makarius wrote:
So what are the characteristic points for theory presentation, either
(1) as paginated PDF,
(2) as static HTML,
(3) as dynamic document within the Prover IDE?
I hope I got it right that you are interested in opinions here?
Otherwise, sorry ;)
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 curren
On Mon, 14 Apr 2014, John Wickerson wrote:
After typing out lots of antiquotations and so on inside my
"text{*...*}" and "header{*...*}" blocks, I would like to see what these
will look like in the finished product. I don't want to print it out, so
I have no interest in a boring monochrome pag
Hi Makarius,
> A general observation is that Isabelle/jEdit has become more and more a live
> document browser, now even with Navigator (e.g. in current
> Isabelle/282f3b06fa86). So one could also ask the question what is still
> missing to eliminate the need for separate HTML browsing.
I thi
On Sun, 13 Apr 2014, John Wickerson wrote:
Hm, it seems that different browsers interpret the CSS "white-space"
property in different ways. (Who'd have thought?)
That is the normal situation. "HTML" has so many standards and different
implementations that one can never be sure what works as
On Sat, 12 Apr 2014, John Wickerson wrote:
One problem with all this is that the contents of "text {* ... *}" is
generally written in LaTeX. It would be desirable if this could also be
exported to HTML. Maybe one has to resort to using something like HeVeA?
I am asking myself these questions
Hm, it seems that different browsers interpret the CSS "white-space" property
in different ways. (Who'd have thought?) It's better now, thanks for pointing
it out.
John
On 12 Apr 2014, at 17:55, Lawrence Paulson wrote:
> I see no indentation at all, e.g.
>
>
> enriched_type map: Option.map
I see no indentation at all, e.g.
enriched_type map: Option.map proof -
fix f g
show Option.map f o Option.map g = Option.map (f o g)
proof
fix x
show (Option.map f o Option.map g) x= Option.map (f o g) x
by (cases x) simp_all
qed
next
show Option.map id = id
proof
fix x
show Option.map id x = id
Thanks Larry. Sorry, but I don't see any difference in the indentation, at
least not in safari or chrome. Can you point out a line that's wrong?
Sent from my iPhone
> On 12 Apr 2014, at 17:01, Lawrence Paulson wrote:
>
> Looks nice. Just the indenting needs fixing.
> Larry
>
>> On 12 Apr 2014
Looks nice. Just the indenting needs fixing.
Larry
On 12 Apr 2014, at 11:58, John Wickerson wrote:
> Hi all,
>
> I've been thinking about and playing with the "theory to HTML" feature of
> Isabelle. The PDF output is handy for producing papers, but I do find HTML so
> much easier to read onsc
Hi all,
I've been thinking about and playing with the "theory to HTML" feature of
Isabelle. The PDF output is handy for producing papers, but I do find HTML so
much easier to read onscreen than PDFs. I mostly use Isabelle/jEdit for
browsing theories, but I think HTML output is still very import
17 matches
Mail list logo
