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