Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-11 00:18:24 -0700 (Fri, 11 Apr 2003)
Revision: 4410
Log message:

      - The "doc" directive now does not require the <:doc< >> quotation. One
      can now use normal terms (applytermlist, to be exact; no quotations required)
      under it.
      
      - <:doc<, <:ext<, << (<:term<) quotations can now be freely mixed (except
      inside <:ext:<, probably - Adam, will non-Phobos quotations be recognized
      correctly inside the Phbos syntax?). Note, that <:doc< >> will produce an
      xlist term with all white space being Comment!comment_write, so is would not
      be a good idea to use those in formal environment. But doing things like
      doc ... <:doc< ... << ... >> .. >> ...
      Should work fine.
      
      - When <:doc< is immediatelly (e.g. on top level) inside the "doc"
      str/sig_item, it will be parsed _delayed_ (e.g. only after the rest of the file
      is processed, including all the declare directives that might go _after_ it.
      Normal terms and <:doc< syntax in other places will be parsed right away.
      
      - The <;doc< and <:ext< quotations are now available in top loop and not just
      in .ml file compilation (Adam, please take a look and see if I did it correcty.
      In particular, is there anything in Phobos that does not need to be compiled in?).
      
      - The qoutations are now handled in term_grammar, not in filter_parse (since
      filter_parse is _not_ a part of top loops, while term_grammar is). This meant
      having to move term_grammar to be _after_ the phobos in the compilation
      order, which meant having to move it to filter/filter.
      
      - Changed ocamldep to ignore module names inside quotations. This helps
      get rid of bogus dependencies for filter_prog (which is full of <:expr< >>
      quotations that have module names in them).
      

Changes  Path
+5 -1 metaprl/editor/ml/Makefile
+1 -0 metaprl/editor/ml/shell_state.ml
+17 -14 metaprl/filter/Makefile
+1 -2 metaprl/filter/base/Files
Deleted metaprl/filter/base/term_grammar.ml
Deleted metaprl/filter/base/term_grammar.mli
+1 -0 metaprl/filter/filter/Files
+1 -2 metaprl/filter/filter/filter_main.ml
+33 -210 metaprl/filter/filter/filter_parse.ml
+2 -5 metaprl/filter/filter/filter_parse.mli
Added metaprl/filter/filter/term_grammar.ml
Properties metaprl/filter/filter/term_grammar.ml
Added metaprl/filter/filter/term_grammar.mli
Properties metaprl/filter/filter/term_grammar.mli
+5 -5 metaprl/theories/itt/itt_subset.ml
+3 -3 metaprl/util/check-status.sh
+4 -3 metaprl/util/ocamldep.mll