Re: [isabelle] Document preparation hints



* Makarius <makarius at sketis.net> [2014-01-07 22:43 +0100]:
> On Tue, 7 Jan 2014, Timothy Bourke wrote:
> 
> >What is the best way to skip proofs when generating .tex files in this
> >way? I was using "ML {* Toplevel.skip_proofs := true *}" but it seems to
> >have stopped working with Isabelle 2013-x (or I have started making a
> >mistake).

...

> The "more official Isabelle means" to access such options are manifold,
> e.g. in a session ROOT file:
> 
>   options [skip_proofs]
>   theories
>     Foo
>     Bar
>     Baz
> 
> or for some particular theories within it:
> 
>   theories [skip_proofs]
>     Foo
>     Bar
>   theories
>     Baz
> 
> or globally on the isabelle build command line:
> 
>   isabelle build -o skip_proofs -D.
> 
> Since this thread is about eliminating the command shell, the latter form
> works in isabelle scala like this:
> 
>   val options = Options.init().bool("skip_proofs") = true
> 
>   Build.build(options, progress = new Build.Console_Progress(verbose =
>   false), more_dirs = List((true, Path.current)))

Very nice. Thank you.

Tim.

(I must have only grepped in 2013-1...)

Attachment: signature.asc
Description: Digital signature



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