Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-21 15:11:58 -0800 (Mon, 21 Feb 2000)
Revision: 2900
Log message:

      When a list of subgoals is too big, displaying used to take a while. I implemented a
      workaround - to only display subgoals when there are <20 of them. We'll need to
      find a better solution - in particular we should take into account subgoal sizes, not only
      the number of subgoals.
      
      It may be a good idea to implement a generic display-form mechanism to allow limiting
      the number of lines a sertain term would occupy. On the other hand, such an approach
      would only save the time to output the display form, but not the time to produce it.
      

Changes	Path
+8 -0	metaprl/BUGS
+6 -1	metaprl/editor/ml/proof_edit.ml