Re: [isabelle] Isabelle2016-RC0 - text with cartouches outside theory



Thanks for the explanations. I am looking forward to the renovated document system but in the meantime a short expression would be great, something like:

Build.dummy("~/Documents")

By the ways, MikTeX produces the following warning:

Package hyperref Warning: Option `pagecolor' is not available anymore.

JÃrgen

-----Original Message-----
From: Makarius [mailto:makarius at sketis.net] 
Sent: 19. oktober 2016 23:50
To: JÃrgen Villadsen; cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] Isabelle2016-RC0 - text with cartouches outside theory

On 19/10/16 21:12, JÃrgen Villadsen wrote:
> 
> In HOL/ex/ML.thy, moving the following line before the theory command gives an error message, but why?
>
> text âSee ðâhttp://mathworld.wolfram.com/AckermannFunction.htmlâ.â;

Before the 'theory' command there is no formal context, but antiquotations (like the globe for @{url}) always require that.


> By the way, is there a short expression for the following line used in the Scala console for batch processing?
> 
> Build.build(Options.init, select_dirs = 
> List(Path.explode("~/Documents")))

Mine is even longer, because I usually include (new Console_Progress) in the expression.

I usually use the persistent Console history to get back to older invocations.


The document system is awaiting a great renovation and full integration into the Prover IDE (at least since 2013).


	Makarius




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