Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-27 21:30:09 -0700 (Tue, 27 Apr 2004)
Revision: 5736
Log message:

      This adds the final major feature I wanted to add to the browser:
      copy/paste of terms into the rulebox.  There are two parts:
         1. The display form engine saves the terms in "slot" position
            into a table based on a string ID.
         2. Javascript to paste a term identified by ID into the rulebox.
      To use this, just click on a term, and it will be pasted into the
      rulebox.
      
      The term in the rulebox is pasted in "src" mode.  Currently, terms
      in "src" mode are not parsable by Term_grammar.  Ugh.
      
      At long last, I declare the the browser interface to be in bugfix mode.
      
      Bugfix TODO:
         1. Terms in "src" mode cannot be parsed.  Working on this.
            See Bugzilla bug #212.
         2. Need to add an "options" menu for things like:
            a. default "ls" flags
            b. handles on terms, so any term can be selected
         3. Remove the "Edit" menu, at least for now
         4. The mouse events are hardcoded in Lm_rformat_html.  Try to
            figure out a better way.
      

Changes  Path
+106 -40 metaprl/refiner/reflib/dform.ml
+30 -13 metaprl/refiner/reflib/dform.mli
+2 -0 metaprl/support/shell/Files
+1 -0 metaprl/support/shell/browser_copy.mli
+1 -0 metaprl/support/shell/browser_copy.mll
+2 -2 metaprl/support/shell/browser_resource.ml
+20 -11 metaprl/support/shell/browser_state.ml
+3 -1 metaprl/support/shell/browser_state.mli
+1 -0 metaprl/support/shell/inputs/content.html
Added metaprl/support/shell/inputs/content.js
Properties metaprl/support/shell/inputs/content.js
+2 -32 metaprl/support/shell/inputs/layout.js
+9 -2 metaprl/support/shell/inputs/rule.html
Added metaprl/support/shell/inputs/rule.js
Properties metaprl/support/shell/inputs/rule.js
+13 -0 metaprl/support/shell/inputs/style.css
+5 -3 metaprl/support/shell/proof_edit.ml
+48 -12 metaprl/support/shell/shell_browser.ml
+5 -3 metaprl/support/shell/shell_package.ml
+5 -3 metaprl/support/shell/shell_root.ml
+25 -17 metaprl/tactics/proof/proof_boot.ml