Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-19 21:49:30 -0700 (Mon, 19 Apr 2004)
Revision: 5678
Log message:

      Some minor changes to the browser display mode.  This *should*
      add:
         1. Catch chdir exceptions, so the browser doesn't abort
            if you give it a bad directory.
         2. The Short/Long mode is now handled in your browser,
            in Javascript.  If you refresh, you get short mode.
         3. Sessions.  This really only makes sense with threads,
            so you will normally use session/2.
         4. Use <span> instead of <font>.
      

Changes  Path
+2 -2 metaprl/support/display/base_dform.ml
+4 -4 metaprl/support/display/nuprl_font.ml
+1 -2 metaprl/support/shell/Files
+2 -2 metaprl/support/shell/browser_display_term.ml
+29 -0 metaprl/support/shell/inputs/layout.js
Added metaprl/support/shell/inputs/page.html
Properties metaprl/support/shell/inputs/page.html
Deleted metaprl/support/shell/inputs/pagelong.html
Deleted metaprl/support/shell/inputs/pageshort.html
+36 -15 metaprl/support/shell/inputs/style.css
+195 -179 metaprl/support/shell/shell.ml
+113 -80 metaprl/support/shell/shell_browser.ml
+5 -1 metaprl/support/shell/shell_java.ml
+8 -5 metaprl/support/shell/shell_sig.mlz