Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-04-01 18:31:19 -0800 (Thu, 01 Apr 2004)
Revision: 5587
Log message:

      Display forms are started.
      I reuse math_fun from Itt_comment and later more forms might be reused.
      May be some part of Itt_comment should be moved to theory-independent
      location or to base theory?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-02 15:33:01 -0800 (Fri, 02 Apr 2004)
Revision: 5591
Log message:

      Adding theories/mojave/extensions/string
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-04 18:39:50 -0700 (Sun, 04 Apr 2004)
Revision: 5594
Log message:

      1. some display forms are defined
      2. cic_list - first example (not finished yet)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-05 17:20:23 -0700 (Mon, 05 Apr 2004)
Revision: 5605
Log message:

      The theories/mojave now lives in a separate CVS repository "mmc" on cvs.metaprl.org.
      
      I am not quite sure, but I believe that "mmc" is supposed to stand for something like
      "Mojave Meta-Compiler", "Meta Mojave Compiler", "Modern Mojave Compiler", or
      "Mean Meta-Compiler" ;-)
      
      The commit logs for the "mmc" repository are going to go to mcc-cvs@metaprl.org,
      go to https://lists.metaprl.org/mailman/listinfo/mcc-cvs to subscribe.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-05 18:47:09 -0700 (Mon, 05 Apr 2004)
Revision: 5608
Log message:

      Add Mmc_ prefix in the syntax.pho and .prla files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-06 08:36:36 -0700 (Tue, 06 Apr 2004)
Revision: 5612
Log message:

      Added closure conversion on assembly code.
      
      Functions in the assembly now use the Lambda["rec"] version
      of recursive functions (the recursive binding is final in the
      parameter list).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-06 20:27:58 -0700 (Tue, 06 Apr 2004)
Revision: 5614
Log message:

      1. Updated standardization to start from index 1.
      2. Simple spilling works.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-06 20:53:11 -0700 (Tue, 06 Apr 2004)
Revision: 5615
Log message:

      product + substitution + application over whole contexts transformed
      from universal to more rule-specific and more correct form.
      

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

      Updated var_subst to avoid capture.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-07 20:26:43 -0700 (Wed, 07 Apr 2004)
Revision: 5619
Log message:

      display forms for applH and  Inductive Definitions are defined
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-08 10:14:09 -0700 (Thu, 08 Apr 2004)
Revision: 5620
Log message:

      A few changes:
      
         1. Trying to get rid of the naming stage.  This stage should be used
            only when needed, not arbitrarily.  It might happen that naming
            is required for type inference, because of let-polymorphism,
            then we might want to add it back.
      
         2. Removed the || and && transformations from naming, and added
            a Mmc_core_front stage that is applied before CPS.  This is
            also where loops get transformed into recursive functions.
      
      One issue: currently it is the CPS transformation that ensures that
      conditionals don't return a value.  However, we want to apply this
      transformation even if we don't use CPS.
      
         3. Added an extension for unit values.
      
         4. Added an extension for loops.  Currently, we just have a while-loop.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-08 12:02:47 -0700 (Thu, 08 Apr 2004)
Revision: 5621
Log message:

      1. Removed the naming stage.
      2. Added the Mmc_core_front, for front-end transformations that
         are performed after type checking.  For example, this is the
         stage for eliminating:
            a. Short-circuit Boolean operations && and ||
            b. Loops
            c. Conditionals nested in an expression
      3. Added "direct" functions for functions that do not escape.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-10 17:31:44 -0700 (Sat, 10 Apr 2004)
Revision: 5630
Log message:

      Moved beta reduction into the Mmc_core_inline module.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-10 18:52:04 -0700 (Sat, 10 Apr 2004)
Revision: 5631
Log message:

      Added a dead code elimination phase to get rid of at least some of the junk.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-10 21:06:09 -0700 (Sat, 10 Apr 2004)
Revision: 5633
Log message:

      The first approximation of display forms is ready.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-11 09:09:05 -0700 (Sun, 11 Apr 2004)
Revision: 5634
Log message:

      Added a slot[str:s, width:n] term that acts as a hint to the formatter
      that typesetting the str:s takes width:n units of horizontal space.
      This partially addresses bug #176.
      
      We should probably define a unicode[str:s, width:n] special term that
      understands that the string is a unicode string.
      
      The typesetter is always free to ignore the width:n hint.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-11 14:40:14 -0700 (Sun, 11 Apr 2004)
Revision: 5636
Log message:

      A minor change to display: display forms are parenthesized only if
      they actually mention the parens option.  This just decouples the
      precedence directive from the parens.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-11 15:58:51 -0700 (Sun, 11 Apr 2004)
Revision: 5638
Log message:

      By default, display keywords in bold.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-11 20:37:01 -0700 (Sun, 11 Apr 2004)
Revision: 5641
Log message:

      first proof (in parameterized list example)
      

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 by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-14 12:04:40 -0700 (Wed, 14 Apr 2004)
Revision: 5648
Log message:

      Removed .js files from support/shell/Files
      

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

      Removed support for frames.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-14 21:08:56 -0700 (Wed, 14 Apr 2004)
Revision: 5651
Log message:

      Added layout control based on browser window size (as Aleksey
      suggested).  This info is not propagated to MetaPRL yet.
      
      Added http service for raw files, with proper handling of
      Last-Modified.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-14 22:49:33 -0700 (Wed, 14 Apr 2004)
Revision: 5652
Log message:

      Added support to start the browser at startup.  The typical use is
      
         setenv MP_BROWSER_COMMAND mozilla
      
      This works with mozilla+Linux, but I'm not at all sure about
      other combinations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-15 19:58:59 -0700 (Thu, 15 Apr 2004)
Revision: 5658
Log message:

      Remove the reference for Shell_http.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-16 11:47:07 -0700 (Fri, 16 Apr 2004)
Revision: 5659
Log message:

      Added a <:dform< ... >> quotation, so we can use doc-style notation
      in display forms.  Unlike <:doc< ... >> quotations, whitespace is
      ignored in dforms, unless enclosed in quotes or the space{'e} term.
      
      Here are some examples:
      
         dform if_df : If{'e1; 'e2; 'e3} =
            <:dform<
               @begin[it]
               @space{// This is a conditional}
               @end[it]
               @hspace
               @bf[if] " " @slot{'e1} " " @bf[then] " " @slot{'e2} @bf[" else"] @slot{'e2}
            >>
      
      So far, this is not obviously better than what we have already.
      However, it makes it easy to use the doc-style display forms.
      
         dform_my_table : Table[title:s]{'e1; 'e2; 'e3} =
            <:dform<
               (* This text comment is displayed with spacing *)
               @begin[space]
               Richard had a dog called Muffin.  He often
               spoke of Muffin in his fireside chats.
               @end[space]
      
               (* This is a nested term *)
               << Muffin{v. 'e1} >>
      
               (* Now display the table *)
               @begin[tabular, l]
               @line{@slot[title:s]}
               @hline
               @line{'e1}
               @line{'e2}
               @line{'e3}
               @end[tabular]
            >>
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-16 11:54:10 -0700 (Fri, 16 Apr 2004)
Revision: 5660
Log message:

      Actually, the space{'t} term should probably be called text{'t}.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-16 12:48:33 -0700 (Fri, 16 Apr 2004)
Revision: 5661
Log message:

      Trying to get output to display correctly in the browser.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-16 16:01:41 -0700 (Fri, 16 Apr 2004)
Revision: 5662
Log message:

      This implements bug 188:
      
      Now in prim rules syntax the "= term" extract specification is optional.
      By default (e.g. if the extract specification is omited), the extract
      is taken to be "default_extract{}". The system will still complain if the
      default_extract opname is not declared, making the extracts truly optional
      only in theories that declare such an opname.
      
      For now, the only theory that uses this is the fir one (which I used to test
      the implemention).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-16 18:41:17 -0700 (Fri, 16 Apr 2004)
Revision: 5664
Log message:

      The links to the inputs directory should be "/inputs/...", not "inputs/...".
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-16 21:00:48 -0700 (Fri, 16 Apr 2004)
Revision: 5665
Log message:

      Added message pane, but only toploop output is captured to the message window.
      The next step is to divert exception output to the browser.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-17 02:43:51 -0700 (Sat, 17 Apr 2004)
Revision: 5666
Log message:

      Removin unused/unneeded "open" statements.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-17 08:06:10 -0700 (Sat, 17 Apr 2004)
Revision: 5667
Log message:

      Minor changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-18 18:46:53 -0700 (Sun, 18 Apr 2004)
Revision: 5668
Log message:

      This is an annoying commit.  It looks massive, but many of the changes
      are just to "open" statements.  Here is the issue that is addressed.
         1. Format is a superset of Printf, and it is much better.
         2. MetaPRL's Rformat is a superset of Format, and it is much better.
      
      This commit moves Rformat into libmojave, as Lm_rformat.  With this
      commit, all output normally goes through Lm_rformat.  Feel free to
      continue to use Format/Printf in special cases, but normal user output
      should go through Lm_format/Lm_printf.  You will probably need to use
      Lm_pervasives as well.
      
      Lm_pervasives defines an (output_rbuffer : out_channel -> Lm_buffer.t -> unit)
      that should be used instead of the print_text_channel function.
      
      There is a new FORMAT option in mk/config.  Define FORMAT=Format to
      enable old behavior if you have trouble.
      
      There are two reasons behind this:
         1. We had a mix of files that use Printf and those that use Format
            for output.  This was a mess.  For instance format-style print
            directives (like "@[<hv 3>Content of text box@]@.") can't be
            used in raw Printf.  This meant that output functions had
            to be duplicated, one version for Printf, and one for Format.
            This commit solves the problem.
         2. Another reason, and the real reason behind this, is to allow
            output to be diverted based on the display device.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-18 18:48:10 -0700 (Sun, 18 Apr 2004)
Revision: 5669
Log message:

      Forgot the add the FORMAT option to the Makefiles.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-19 02:58:14 -0700 (Mon, 19 Apr 2004)
Revision: 5670
Log message:

      A few minor HTML fixes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-19 08:36:51 -0700 (Mon, 19 Apr 2004)
Revision: 5671
Log message:

      Display output correctly in browser mode.
      

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 by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-19 12:11:47 -0700 (Mon, 19 Apr 2004)
Revision: 5673
Log message:

      Browser layout should be updated using BODY.onLoad, not in the HEAD
      section.  This now works with IT.  It also does active resizing when
      then browser window is resized.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-19 15:16:39 -0700 (Mon, 19 Apr 2004)
Revision: 5674
Log message:

      - Removed Lm_string_util.concal which was just duplicating String.concat.
      - A bit more debugging in Shell_browser.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-19 20:45:42 -0700 (Mon, 19 Apr 2004)
Revision: 5676
Log message:

      When dealing with Ocaml toploop, we must use the Ocaml Formal module.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-19 21:09:03 -0700 (Mon, 19 Apr 2004)
Revision: 5677
Log message:

      When a non-existing theory is specified in a URL, print a Not_found error page,
      instead of dying with an uncaught exception.
      

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 by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-20 02:07:38 -0700 (Tue, 20 Apr 2004)
Revision: 5679
Log message:

      - For Last-modified, do not forget to add 1900 to the year.
      
      - Fixed the problem with accessing directories in /inputs. I got the backtrace
      of this problem and it appears to be that open_in succeeds on directories and
      only the input function (in Http_simple.copy) raises the Sys_error exception.
      I ended up adding an explicit Unix.stat.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-20 04:16:07 -0700 (Tue, 20 Apr 2004)
Revision: 5680
Log message:

      1. Make sure all session (i.e. non-special) URLs end with a /.
         Rationale:
            (a) It used to be the case that both ".../itt_fset" and ".../itt_fset/"
                would display the itt_fset theory. Obviously, the relative links
                would only work correctly in at most one of the two.
            (b) Between always stripping the last / and always insisting on the
                / ending I chose the latter since it makes figuring out the links
                much easier (e.g. this way the link to a rule in a theory listing
                does not have to include the theory name, just the rule name). Also,
                all the entries in MetaPRL are directory-like (since they are allowed
                to have subentries), so this appears to be consistent.
      
         As in a standard web server, attempt to go to a URL that does not end with
         a /, but is otherwise valid results in a redirect to a proper URL (i.e. with
         the missing / appended).
      
      2. Linkified the rule and rewrite names. For now all of them are linkified, even
         the primitive ones - this should be fixed eventually. The CSS class is "rule_name".
      
      3. Added the charset information (charset=utf-8) to all the html pages, as required
         in the standard.
      
      4. Changed the style.css, page.html and style-related stuff in layout.js to be
         fully standards-complient (and pass the validator). Note that this also included
         deleting the non-standard "onResize" attribute. Unfortunalely, the divs still
         do not scroll.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-20 17:21:30 -0700 (Tue, 20 Apr 2004)
Revision: 5681
Log message:

      Removing some code left over from the old-style comments support.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-20 20:22:12 -0700 (Tue, 20 Apr 2004)
Revision: 5682
Log message:

      (* WARNING : this breaks .prla/.cmoz binary compatibility, export ypur proofs *)
      
      Include the resource types in the resource definition, not only in declaration.
      
      The syntax of a resource implementation (in .ml) is being changed to
      let resource (ctyp1, ctyp2) name = expr
      where the types have the same meaning as in a resource declaration (in .mli)
      
      It is now possible to implement a "private" resource w/o declaring it.
      
      This fixes bug 168 (and its dup bug 178).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-20 23:47:42 -0700 (Tue, 20 Apr 2004)
Revision: 5684
Log message:

      nat_is_int should be added to nth_hyp, not intro.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 01:31:14 -0700 (Wed, 21 Apr 2004)
Revision: 5685
Log message:

      Small step towards making the resource annotations on itt_group rules
      a bit saner.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 02:47:02 -0700 (Wed, 21 Apr 2004)
Revision: 5686
Log message:

      Be more clean on "omake clean"
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-04-21 08:52:16 -0700 (Wed, 21 Apr 2004)
Revision: 5687
Log message:

      FORMAT was missing
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-21 08:54:55 -0700 (Wed, 21 Apr 2004)
Revision: 5688
Log message:

      Added some widgets to the browser.  Widgets are context-sensitive,
      you can add them to the browser resource define in Browser_resource.
      
      This version also demonstrates the use of iframes to display the
      document.  I'm including for demo purposes, but I don't like it.
      
      TODO:
         1. The upper menubar should always be present, even if
            the resource is not.
         2. The history should select the last entry.  It would be
            nice to catch arrow events in the input area, and scroll
            the history.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 11:41:48 -0700 (Wed, 21 Apr 2004)
Revision: 5689
Log message:

      - Another minor change in resource annotations (subset intro is now
        AutoMustComplete)
      
      - Fixed the itt_cyclic_group.prla file that somehow got corrupted.
      
      - Proved a bit more in itt_subset2.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 21:52:45 -0700 (Wed, 21 Apr 2004)
Revision: 5691
Log message:

      This commit changes the way the AutoMustComplete flag for intro annotations is
      implemented.
      
      Instead of using it to check the item found by the term table _after_ it is
      found, the AutoMustComplete flag is now checked _during_ the term table lookup.
      This means that the AutoMustComplete entries will now be completely ignored
      during the "normal" phase of autoT, allowing it to fall back to less specific
      entries. The manual entires to intro now have to include an extra boolean field
      --- setting it to true has the same effect as AutoMustComplete.
      
      P.S. The meaning and implementation of CondMustComplete did not change.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 22:28:18 -0700 (Wed, 21 Apr 2004)
Revision: 5692
Log message:

      [Bug 129] Got rid of the eqcd resource and the eqcdT tactic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 23:19:31 -0700 (Wed, 21 Apr 2004)
Revision: 5694
Log message:

      Adding m-paper-hosc, that uses kluwer style. Surprizingly, the formatting
      looks pretty good, so we need to "only" worry about contents.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 23:24:16 -0700 (Wed, 21 Apr 2004)
Revision: 5695
Log message:

      Citations style.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-22 15:50:05 -0700 (Thu, 22 Apr 2004)
Revision: 5696
Log message:

      Removing some dead code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-23 05:42:38 -0700 (Fri, 23 Apr 2004)
Revision: 5699
Log message:

      - Updated the title
      - Formatting updates
      - Fixed the appendix style
      - Merged the related work with the new stuff from the ICFP paper
      - Cut the parsing section down to one paragraph and source language table
      - Killed the "on next page" and othe similarly fragile references to figure
      locatins. Hopefully I got them all.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-23 12:10:20 -0700 (Fri, 23 Apr 2004)
Revision: 5700
Log message:

      I had been working on the browser sporadically; here is a demo
      update.
      
      Changes:
         1. Use frames instead of div.  I'm still not sure what the
            advantage is beyond getting the scrollbars to work
            properly.  The control code is a lot more complicated
            of course.
         2. This history works with the arrow keys.
         3. Session support is better.
      
      Tested just on Mozilla 1.4, I haven't tested on other browsers.
      
      TODO:
         1. It is not possible to create a new session currently.
         2. Menubar should have some default non-context-sensitive
            entries.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2004-04-23 12:44:44 -0700 (Fri, 23 Apr 2004)
Revision: 5701
Log message:

      Attempting to tweak/clean-up the Mac OS X README.  Also attempted to
      document check() and check_all() as they seem to be implemented now(?).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-23 12:50:42 -0700 (Fri, 23 Apr 2004)
Revision: 5702
Log message:

      Somehow, I forgot to add these files in the last browser commit.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-04-23 14:28:23 -0700 (Fri, 23 Apr 2004)
Revision: 5703
Log message:

      Some mpopt args might be more than one word.  Also added ppc directory to
      mpconfig.
      

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-04-23 14:30:22 -0700 (Fri, 23 Apr 2004)
Revision: 5704
Log message:

      Browser command might be more than one word.  E.g. "open -a safari".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-23 17:18:47 -0700 (Fri, 23 Apr 2004)
Revision: 5706
Log message:

      Made some of the changes discussed earlier.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-23 19:18:02 -0700 (Fri, 23 Apr 2004)
Revision: 5708
Log message:

      Remove aggressive use of Lm_rformat.  To use the normal format library,
      use Lm_printf.  For output that should be diverted to the output device,
      use Lm_rprintf.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-23 20:26:21 -0700 (Fri, 23 Apr 2004)
Revision: 5710
Log message:

      Remove some references to Lm_format.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-23 21:03:39 -0700 (Fri, 23 Apr 2004)
Revision: 5711
Log message:

      Removing more dependencies on Lm_format.
      
      Adjusting name comvention: functions named output_XXX take an output
      channel, and functions names print_XXX send to stdout.  We violated
      this all over the place, using print_XXX not output_XXX.  No big deal.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2004-04-24 00:08:07 -0700 (Sat, 24 Apr 2004)
Revision: 5712
Log message:

      print_symbol didn't seem to be defined anymore (meaning the module
      didn't compile for me), so I changed the occurances to output_symbol,
      which seems to work/be consistent with recent changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-24 09:43:52 -0700 (Sat, 24 Apr 2004)
Revision: 5713
Log message:

      This should remove the final vestige of Lm_format in the omake
      part of libmojave.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-24 17:33:52 -0700 (Sat, 24 Apr 2004)
Revision: 5714
Log message:

      Sorry for the spam commits.  I'm hoping this is the final change to IO
      that will enable porting omake to the new IO model.
      

Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-24 17:52:13 -0700 (Sat, 24 Apr 2004)
Revision: 5716
Log message:

      cic_ind_type: reversed rewrites and some primitive tactics added
      cic_list: incorrect (unprovable) statements changed to the correct ones
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-04-24 19:57:22 -0700 (Sat, 24 Apr 2004)
Revision: 5717
Log message:

      Enabled rwh to go through sequent-term.
      Basically I've copied sequent case from apply_fun_higher_term to
      apply_var_fun_higher_term,
      copied apply_fun_higher_hyps to apply_var_fun_higher_hyps
      and there I add hyp and context names to the list of bound variables
      for the rest the sequent (not including current hyp/context).
      I didn't really test it but tried in CIC theory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-24 21:15:09 -0700 (Sat, 24 Apr 2004)
Revision: 5718
Log message:

      For the formatter, added an "azone" that assumes that its body is
      "atomic."  That is, the body is to be typeset all or none.  The width
      of an atomic block is 1 unit.
      
      This addresses the formatting problem where multi-character
      sequences were getting split.  By default, if we use UTF-8, the
      formatter would interpret a multi-character unicode sequence
      as multiple characters.  By wrapping it:
          azone <utf-8-sequence> ezone
      the utf-8-sequence gets interpreted as an atomic unit.
      
      This should work properly in prl and html mode.  The TeX version
      is not implemented, but is no big deal for the moment.
      
      For PRL mode, we may or may not want to split multiple character
      Unicode sequences, like atomic["?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189?\239?\191?\189"] (Leftrightarrow)
      since it is actually a sequence of several unicode characters.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-04-24 21:30:44 -0700 (Sat, 24 Apr 2004)
Revision: 5719
Log message:

      cic_ind_type: indWrapC fixed
      cic_list: nil_wf proof updated to reflect my recent update in refiner
      and current update in cic_ind_type
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-25 17:26:45 -0700 (Sun, 25 Apr 2004)
Revision: 5720
Log message:

      Modified some text in the M-paper.  The main issue we must deal with
      is the large comment delimited by !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!.
      
      I added some text there.  Would you look at it Aleksey?  Also,
      I changed the intro to CPS in the appendix in the same way.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-25 18:26:31 -0700 (Sun, 25 Apr 2004)
Revision: 5721
Log message:

      A few fixed to the first 10 pages.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-04-25 18:30:28 -0700 (Sun, 25 Apr 2004)
Revision: 5722
Log message:

      cic_lambda - declarations of bind removed
      cic_ind_type - better convertionals to unfold inductive definitions
      cic_list - tried new convertionals
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-25 19:40:08 -0700 (Sun, 25 Apr 2004)
Revision: 5723
Log message:

      In TeX mode, put quotes in    displayed as ``...''.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-25 20:33:05 -0700 (Sun, 25 Apr 2004)
Revision: 5724
Log message:

      - Added some text in the summary, comparing different CPS approaches (both the
      semantical and syntactical aspects). Jason, please take a look.
      
      - Changed the text width for TeX printouts from 70 to 60 (otehrwise we get
      oevrfull hboxes in this paper). This should be configurable, I will file a
      Bugzilla report.
      
      - Other small fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-25 20:48:00 -0700 (Sun, 25 Apr 2004)
Revision: 5725
Log message:

      A few more changes to the CPS text. Jason, are we done?
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-25 21:11:19 -0700 (Sun, 25 Apr 2004)
Revision: 5726
Log message:

      A very minor change to the wording.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-25 21:20:41 -0700 (Sun, 25 Apr 2004)
Revision: 5727
Log message:

      A number of minor MP_DEBUG=spell fixes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-26 11:07:02 -0700 (Mon, 26 Apr 2004)
Revision: 5728
Log message:

      A slight change to the browser interface.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-26 14:26:49 -0700 (Mon, 26 Apr 2004)
Revision: 5729
Log message:

      MP_DEBUG=spell fixes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-26 22:02:35 -0700 (Mon, 26 Apr 2004)
Revision: 5730
Log message:

      - Updated the Merlin entry (as the ACM volume is finally published)
      - Added the new paper accepted to TPHOLs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-26 22:06:22 -0700 (Mon, 26 Apr 2004)
Revision: 5731
Log message:

      HTML fixes.
      

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

      Added some more buttons to the browser interface.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-27 15:43:46 -0700 (Tue, 27 Apr 2004)
Revision: 5733
Log message:

      Oops, accidentally commited the doublespace version.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-27 16:53:39 -0700 (Tue, 27 Apr 2004)
Revision: 5734
Log message:

      Spelling should not be checked inside the tt and rulebox operators (since
      those never contain English text).