On Mon, 26 May 2014, Jasmin Blanchette wrote:
Am 26.05.2014 um 15:24 schrieb Makarius <makar...@sketis.net>:
I think you could afford an actual keyword for the "dead" modifier and
use it without colon, like "lazy" in HOLCF/domain. That would
substract "dead" from the normal identifier space, but merely means its
very few occurrences on AFP/Jinja and AFP/JinjaThreads need to be
quoted.
Indeed, that would make sense. And perhaps we don't even need to make it
a keyword? It shouldn't be hard to parse "(dead 'a)" with
"Parse.reserved" for "dead".
In principle yes. The final answer is left to the one who goes to the
bottom of the system to implement it -- and sees if there are other
side-conditions.
Note that in PIDE there is extra markup even for certain quasi-keywords,
e.g. the "add" in "(simp add: ...)".
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
