Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-06-09 11:38:02 -0700 (Wed, 09 Jun 2004)
Revision: 5869
Log message:

      This modifies the infrastructure for threads.  Here is the model:
      
          1. Each thread has a current state, and each state has a set
             of global variables.
      
          2. State variables must be locked before being used.
      
          3. State variables come in two types: shared and private.
             Each state has its own copy of the private variables.
      
      For example, each job in the shell has its own state, and its
      own copy of the Shell.info struct.  States are managed implicitly,
      so global variables look just like global variables.  Access is
      managed with the State.read/State.write routines.
      
      Here is an example of usage for a shared variable:
      
          let global_entry = State.shared_val "debug" (ref 0)
      
          let get () =
             State.read global_entry (fun x -> !x)
      
          let incr () =
             State.write global_entry (fun x -> x := !x + 1)
      
      For private variable, you have to supply a "fork" function that
      is used to copy the value.  Each thread/state will have its own copy
      of the variable.  The other functions remain the same.
      
          let global_entry = State.shared_val "debug" (ref 0) (fun x -> ref !x)
      
      All the State.* functions are wrappers that take a function argument.  The
      value is locked on entry into the function, and unlocked when the function exits.
      Exceptions are handled correctly.
      
      Don't use Mutex if you can help it!!!  The Mutex functions do not
      handle exceptions correctly.  Use the State module instead.
      
      NOTES:
      
         1. I removed the Java interface...  It was just getting to be too much
            of a hassle.  We can ressurect it if we ever want it again.
      
         2. This is just the infrastructure pass.  The global values used by the
            browser need to be updated to the new model.
      

Changes  Path
+42 -25 metaprl/editor/ml/mp.ml
+4 -0 metaprl/editor/ml/mp.mli
+3 -5 metaprl/editor/ml/mp_top.ml
+327 -316 metaprl/editor/ml/nuprl_eval.ml
+5 -5 metaprl/editor/ml/nuprl_eval.mli
+2 -0 metaprl/editor/ml/shell_mp.ml
+10 -5 metaprl/editor/ml/shell_p4.ml
+0 -0 metaprl/editor/ml/shell_p4.mli
+1 -1 metaprl/mllib/http_server.ml
+1 -0 metaprl/mllib/http_simple.ml
+1 -1 metaprl/mllib/remote_queue_null.ml
+87 -115 metaprl/refiner/reflib/term_copy2_weak.ml
+3 -7 metaprl/support/shell/Files
+10 -13 metaprl/support/shell/browser_resource.ml
+1 -1 metaprl/support/shell/browser_resource.mli
Deleted metaprl/support/shell/java_display_term.ml
Deleted metaprl/support/shell/java_display_term.mli
Deleted metaprl/support/shell/java_mux_channel.ml
Deleted metaprl/support/shell/java_mux_channel.mli
+106 -118 metaprl/support/shell/package_info.ml
+18 -62 metaprl/support/shell/proof_edit.ml
+0 -1 metaprl/support/shell/proof_edit.mli
+696 -851 metaprl/support/shell/shell.ml
+1 -1 metaprl/support/shell/shell.mli
+220 -239 metaprl/support/shell/shell_browser.ml
+1 -1 metaprl/support/shell/shell_browser.mli
Deleted metaprl/support/shell/shell_java.ml
Deleted metaprl/support/shell/shell_java.mli
+2 -17 metaprl/support/shell/shell_package.ml
+2 -17 metaprl/support/shell/shell_root.ml
+0 -2 metaprl/support/shell/shell_rule.ml
+58 -109 metaprl/support/shell/shell_sig.mlz
+240 -242 metaprl/support/shell/shell_state.ml
+13 -6 metaprl/support/shell/shell_state.mli
+10 -7 metaprl/tactics/proof/proof_boot.ml