Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-19 10:58:23 -0700 (Mon, 19 Apr 2004)
Revision: 5672
Log message:

      Use CSS stylesheets instead of hardcoding fonts and colors.
      

Changes  Path
+4 -3 metaprl/support/display/base_dform.ml
+10 -10 metaprl/support/display/nuprl_font.ml
+2 -1 metaprl/support/shell/Files
+1 -0 metaprl/support/shell/browser_copy.mli
+4 -14 metaprl/support/shell/browser_copy.mll
+11 -9 metaprl/support/shell/browser_display_term.ml
+1 -2 metaprl/support/shell/inputs/layout.js
+3 -1 metaprl/support/shell/inputs/login.html
+7 -5 metaprl/support/shell/inputs/pagelong.html
+7 -5 metaprl/support/shell/inputs/pageshort.html
Added metaprl/support/shell/inputs/style.css
Properties metaprl/support/shell/inputs/style.css
+1 -1 metaprl/support/shell/shell_browser.ml