Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-04 19:41:51 -0800 (Fri, 04 Feb 2005)
Revision: 6598
Log message:

      This tries to be more careful about parsing terms.
      
      In general if you see an unparsed term in MetaPRL, it has to be
      due to the use of one of two functions being used in Filter_parse:
      raw_term_of_parsed_term, or quote_term_of_parsed_term.  These are the
      only two functions that bypass term parsing.
      

Changes  Path
+14 -7 metaprl-branches/opname_classes4/filter/base/filter_type.ml
+30 -25 metaprl-branches/opname_classes4/filter/filter/filter_parse.ml
+43 -33 metaprl-branches/opname_classes4/filter/filter/term_grammar.ml
+0 -3 metaprl-branches/opname_classes4/support/display/perv.ml
+6 -63 metaprl-branches/opname_classes4/theories/experimental/syntax/syntax_test.ml