Michael Norrish
Michael Norrish
Is there an easy fix for the regression here? Would be nice to resolve the PR if possible.
Actually, if users are just forbidden from using `verbatim`, this wouldn't be so bad. Inside an `alltt` they can use `\%` to get a `%` that isn't stripped as a...
I agree with Magnus about both the need to make the common case easy and to include support for `set_grammar_ancestry`. I’d also prefer to have the `Theory bla` as the...
Agreed that it can be deferred. It might at least be easy to implement (outside of Holmake) : `s/(ident)Theory/\1/g`
I think you are conflating two namespace levels. This proposal is more about the SML level (the names visible in tactics for example). The renaming you did in your example...
The grammar and parsing for this change would be easy. The more significant change would be giving this syntax a target in the AST type and then ensuring that those...
Functions, the `fn` form and `val` all allow patterns already. See for example the tests in `compiler/parsing/tests/cmlTestsScript.sml` around line 192. Not to mention the grammar itself.
Ah. That's true. The syntax only allows for patterns; it doesn't allow for multiple cases separated by bars (except in the `case` syntax of course). I think something like fun...
I'm happy to do the parser part of all three strategies (the changes will all be pretty similar).
None by me so far. I can look into it this week though.