Re: [isabelle-dev] NEWS: proof outline with cases

2016-08-09 Thread Makarius 
On 08/08/16 10:52, Andreas Lochbihler wrote:

> sometimes quotes are needed around the case name (e.g., if it is a
> keyword like "try" or "oracle", or if it is a case of an induction rule
> by the function package for an equation which has been split up by the
> sequential option, i.e., 3_1 and 3_2).

See now

changeset:   63640:c273583f0203
parent:  63633:4302f86920fe
user:wenzelm
date:Tue Aug 09 19:44:28 2016 +0200
files:   src/Pure/Isar/proof_context.ML src/Pure/Isar/token.ML
description:
print name in parsable form;


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

2016-08-09 Thread Makarius 
On 08/08/16 14:44, Lars Hupel wrote:
> 
> For HOL-Proofs, the relevant job is "isabelle-repo-makeall". A catalog
> of all builds and all archived logs can be found under the following URL:
> 
> 
> 

I did not know of this JSON API yet. In Isabelle/74604a9fc4c8 there are
Isabelle/Scala operations to access that information. (It is an
interesting experience to work with these untyped JSON things; reminds
me of LISP expressions.)

I will later work out, if this is going to be a batch tool (like former
isatest-stats) or a PIDE GUI panel. It might be actually easier to make
proper a GUI application than a web application from it.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev