Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-21 19:48:11 -0800 (Sat, 21 Jan 2006)
Revision: 8564
Log message:

      In the theory search (OMakefile_theories.find-theory), do not
      find the theory unless the MetaprlInfo file exists.
      
      The issue is as follows.  The THEORY_DEPS variable specifies
      theories relative to the theories/ directory.  So this requires
      that we place theories in some place where the path works.
      
      For example, I want my private theory to include these theories:
         itt/reflection
         poplmark/naive
      
      This means I *must* name these directories as such (with
      the current scheme), I can't just put them somewhere
         myproject/reflection
         myproject/naive
      
      Instead, they must be something like
         myproject/itt/reflection
         myproject/poplmark/naive
      
      Oh well.  But if I define myproject/itt, this *does not* define the
      itt theory.  So the theory-path-search matches only if the MetaprlInfo
      file exists.
      
      With this, the search really is MetaPRL-specific.  While I think that
      this might still be a general problem, perhaps Aleksey's solution is
      the right way to go.  That is, we would keep a Map that would cache the
      search-path results.
      

Changes  Path
+8 -2 metaprl/OMakefile_theories
+0 -8 metaprl/theories/itt/MetaprlInfo
+8 -0 metaprl/theories/itt/reflection/MetaprlInfo