Re: [isabelle] Allowed characters in theory names for document build



El lun, 09-10-2017 a las 21:58 +0200, Lars Hupel escribiÃ:
> [I took the liberty of moving this to isabelle-users]

Thanks!

> Dear Christian,
> 
> > Isabelles pdflatex document build fails when there is a space or
> > any of
> > Ã, Ã, Ã, Ã and % in a theories name. Possibly more characters are
> > affected.
> 
> I would strongly recommend using plain ASCII characters for theory 
> names. Many things might break in unexpected things (apart from
> document 
> preparation) when non-ASCII characters are used.

Things do break, but I do not see how that is a reason not to fix them.

> > To make Isabelle and its document build feature more permissive
> > with
> > filenames, what is the best way to solve these issues?
> 
> I don't think this is expected to work, hence I see very little
> prospect 
> to solve this in the future.

I expect programs to properly handle filenames. I also don't think this
requires a big monolithic change.

Is there any negative effect of making Isabelle more robust in handling
of names?




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