Re: [isabelle] Custom inner syntax parsing in ML.
- To: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
- Subject: Re: [isabelle] Custom inner syntax parsing in ML.
- From: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>
- Date: Wed, 2 Oct 2019 03:45:30 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=Ir+wDmIGT1Py7VQVoZGVnXh3j3L6lmpYsjKAzgWH9Ok=; b=DSyNhcCRWxmK9umX52CINThmCtAi2TLX96B3NbHMoS+SWPhURC9QIvw65LjFB/JI73rsZFuU0x9gZm9xItaaAPLOzJ+maKOyMWIg9QGwgyTQwKKM/ZHLuHmTPloCCrvPJMs69wIElTSyTBIsVUnrSf08m558ZniRG70kosq3ehCormtpUlhM97CAmoMCt1MwfRcAYf+Ru5b5XfqtZBLwaDh3zhOOjX5/k00gl23tZPrcZzKFsp6lSdA2NDkAohjts7WsvRPU8asjeMOz7hddUt/YyCm2dvOkB1EeK5GxAKpVlle2LMu3eecHvIHMvS/fKTAEAuNpZf+k6CY4yhYzgQ==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=MPsuRn45bvRXvdq03nLIS39bxSbkPZ4j5PE+pA/64z3Uvy2SBadbxRXKWjE2occV0UGnZz6V4xYv4/VFp5G1R0Fczcg0Hk4YDPRGrwTwtpCPiEhvrI4FQkKe0y/BsdLvWzBjvG+2+266Ri5I3sxq+RN/ua0UzfG3rgLRpFtIDQ/cW2MEdAjxHFNgGOx/Pkx4wed6I2aJ8y8vAc38XJgEn7dVW1FY33wZwdaTM9lesfzkVDPXPdjcVe1htC2EQSZgUl17Tr5JV9m9wI+fWvWPbCY29rospPdQx5DgaIWejWeG/4frAzApXq0bJeg7M/dS4cKBg036DpYPOgBkxfG9GQ==
- Authentication-results: spf=none (sender IP is ) smtp.mailfrom=Jeremy.Dawson at anu.edu.au;
- In-reply-to: <firstname.lastname@example.org>
- References: <2074102.1x7EFbrfS5@ekpyrosis> <email@example.com>
- Thread-index: AQHVdR8n9pjilSMw/UuTVJySQVT6b6dFyrGAgADyugA=
- Thread-topic: [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.
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 ﬁrst version of chapter 5 about parsing.
and the other (I think more recent) says
Jeremy Dawson wrote the ﬁrst 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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and