Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-14 12:02:36 -0700 (Wed, 14 Apr 2004)
Revision: 5647
Log message:

      Added rudimentary support for display in a Web Browser.
      To use, use the command "mpopt -browser [-port <int>]",
      and follow the directions.  The interface is basically
      the same as the normal toploop.  You type commands in
      the input area, and MetaPRL displays the output.
      
      Some notes about authentication.  The interface uses
      challenge/response validation based on MD5 sums.
      The connection requires a password, which is stored
      in the clear in a protected file on the MetaPRL host,
      and optionally as a cookie in your browser.  The
      password is never sent in the clear over the network.
      
      This isn't finished yet, but is pretty usable.  I would
      appreciate comments.
      
      TODO:
         1. Some exceptions are not being caught.  In general
            exception printing should be directed to the browser.
         2. Normal output should also be directed to the browser.
         3. Somehow Mozilla is not remembering cookies, which
            means that you have to enter your password more
            often than necessary.  Undoubtably this is due
            to my lack of Javascript knowledge.  If this can be
            fixed, the challenge can be updated frequently.
         4. There are some leftover files from a frame-based
            interface.  Frames are awkward, so I'll delete these
            files after the commit.
         5. I haven't tried it on Win32.
      

Changes  Path
Added metaprl/clib/Files
Properties metaprl/clib/Files
+1 -11 metaprl/clib/Makefile
+2 -12 metaprl/clib/OMakefile
Added metaprl/clib/c_time.c
Properties metaprl/clib/c_time.c
+8 -2 metaprl/editor/ml/mp_top.ml
+3 -0 metaprl/editor/ml/mpconfig
+13 -4 metaprl/editor/ml/shell_mp.ml
+18 -10 metaprl/editor/ml/shell_p4.ml
+4 -2 metaprl/filter/base/filter_cache_fun.ml
+1 -1 metaprl/filter/base/filter_exn.ml
+1 -1 metaprl/filter/phobos/phobos_exn.ml
+4 -1 metaprl/mllib/Files
Added metaprl/mllib/ctime.ml
Properties metaprl/mllib/ctime.ml
Added metaprl/mllib/ctime.mli
Properties metaprl/mllib/ctime.mli
+6 -1 metaprl/mllib/http_server.ml
+6 -0 metaprl/mllib/http_server.mli
Added metaprl/mllib/http_server_type.ml
Properties metaprl/mllib/http_server_type.ml
Added metaprl/mllib/http_simple.ml
Properties metaprl/mllib/http_simple.ml
Added metaprl/mllib/http_simple.mli
Properties metaprl/mllib/http_simple.mli
+34 -28 metaprl/refiner/reflib/dform.ml
+2 -2 metaprl/refiner/reflib/refine_exn.ml
+142 -117 metaprl/refiner/reflib/rformat.ml
+15 -4 metaprl/refiner/reflib/rformat.mli
+10 -10 metaprl/refiner/reflib/simple_print.ml
+6 -4 metaprl/support/display/nuprl_font.ml
+16 -4 metaprl/support/display/summary.ml
+2 -1 metaprl/support/display/summary.mli
Properties metaprl/support/shell
Added metaprl/support/shell/Files
Properties metaprl/support/shell/Files
+1 -23 metaprl/support/shell/Makefile
+8 -23 metaprl/support/shell/OMakefile
Added metaprl/support/shell/browser_copy.mli
Properties metaprl/support/shell/browser_copy.mli
Added metaprl/support/shell/browser_copy.mll
Properties metaprl/support/shell/browser_copy.mll
Added metaprl/support/shell/browser_display_term.ml
Properties metaprl/support/shell/browser_display_term.ml
Added metaprl/support/shell/browser_display_term.mli
Properties metaprl/support/shell/browser_display_term.mli
Added metaprl/support/shell/browser_sig.mlz
Properties metaprl/support/shell/browser_sig.mlz
Deleted metaprl/support/shell/display_term.ml
Deleted metaprl/support/shell/display_term.mli
Properties metaprl/support/shell/inputs
Added metaprl/support/shell/inputs/content.html
Properties metaprl/support/shell/inputs/content.html
Added metaprl/support/shell/inputs/frameset.html
Properties metaprl/support/shell/inputs/frameset.html
Added metaprl/support/shell/inputs/login.html
Properties metaprl/support/shell/inputs/login.html
Added metaprl/support/shell/inputs/longcommand.html
Properties metaprl/support/shell/inputs/longcommand.html
Added metaprl/support/shell/inputs/pagelong.html
Properties metaprl/support/shell/inputs/pagelong.html
Added metaprl/support/shell/inputs/pageshort.html
Properties metaprl/support/shell/inputs/pageshort.html
Added metaprl/support/shell/inputs/shortcommand.html
Properties metaprl/support/shell/inputs/shortcommand.html
Added metaprl/support/shell/inputs/start.html
Properties metaprl/support/shell/inputs/start.html
Added metaprl/support/shell/java_display_term.ml
Properties metaprl/support/shell/java_display_term.ml
Added metaprl/support/shell/java_display_term.mli
Properties metaprl/support/shell/java_display_term.mli
Added metaprl/support/shell/java_mux_channel.ml
Properties metaprl/support/shell/java_mux_channel.ml
Added metaprl/support/shell/java_mux_channel.mli
Properties metaprl/support/shell/java_mux_channel.mli
Deleted metaprl/support/shell/mux_channel.ml
Deleted metaprl/support/shell/mux_channel.mli
+53 -34 metaprl/support/shell/proof_edit.ml
+2 -1 metaprl/support/shell/proof_edit.mli
+119 -79 metaprl/support/shell/shell.ml
Added metaprl/support/shell/shell_browser.ml
Properties metaprl/support/shell/shell_browser.ml
Added metaprl/support/shell/shell_browser.mli
Properties metaprl/support/shell/shell_browser.mli
Deleted metaprl/support/shell/shell_http.ml
Deleted metaprl/support/shell/shell_http.mli
Added metaprl/support/shell/shell_java.ml
Properties metaprl/support/shell/shell_java.ml
Added metaprl/support/shell/shell_java.mli
Properties metaprl/support/shell/shell_java.mli
+1 -0 metaprl/support/shell/shell_p4_sig.mlz
+25 -37 metaprl/support/shell/shell_package.ml
+25 -37 metaprl/support/shell/shell_root.ml
+4 -2 metaprl/support/shell/shell_rule.ml
+12 -4 metaprl/support/shell/shell_sig.mlz
+20 -2 metaprl/support/shell/shell_state.ml
+1 -0 metaprl/support/shell/shell_state.mli
+3 -3 metaprl/tactics/proof/proof_boot.ml