Re: [isabelle] Custom inner syntax parsing in ML.




On 1/10/19 11:16 pm, Makarius wrote:
>> The otherwise very great tutorial at https://
>> nms.kcl.ac.uk/christian.urban/Cookbook/ is unfortunately still lacking
>> information on parse translations and generally on intervening on the inner
>> syntax parsing process - in fact I'm considering to contribute to it once my
>> own project is done.

> That document is "fan-fiction". In its early years, I tried to
> contribute to it and rectify its somewhat misleading approach at
> "Isabelle system hacking", but I've given up on it long ago.
> 
> 
> 	Makarius
> 
At an earlier stage of this document there was a chapter on parsing.  I 
have two copies of pdf versions of the document, of which one says

Jeremy Dawson wrote the first version of chapter 5 about parsing.

and the other (I think more recent) says

Jeremy Dawson wrote the first version of chapter ?? about parsing.

I understood this to indicate that parsing in Isabelle had changed so 
significantly that the chapter was no longer useful, and that the 
authors of these changes failed to update the documentation.

Unfortunately I can't recall enough about the chapter to tell whether it 
would have given exactly what you want.

(I have no idea what "fan-fiction" or the somewhat misleading approach 
at "Isabelle system hacking" mean)

Cheers,

Jeremy


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