Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 21:48:25 -0700 (Wed, 25 Aug 2004)
Revision: 6139
Log message:
- Adjusted the precedences so that the "smart" syntax for sequents is parsed
correctly. E.g. "a b{| ... |}" is now correctly parsed as "a ('b{| ... |})"
instead of "(a b){| ... |}" and similarly for "a in b{| ... |}" and other
operators.
- Simplified the grammar a bit, removing some unnecessary restrictions (for
example, the notion of "applyterm" was removed - now any term not containing
a non-parenticized coma can be a subterm of an application).
Changes | Path |
+0 -1 | metaprl/filter/base/filter_type.ml |
+4 -5 | metaprl/filter/filter/filter_parse.ml |
+50 -65 | metaprl/filter/filter/term_grammar.ml |
+0 -1 | metaprl/support/shell/shell_state.ml |