CHGLOG.TXT

//*****************************************************************************/
//* Copyright (C) 2005-2013                                                   */
//* MEL O'CAT  X178G243 (at) yahoo (dot) com                                  */
//* License terms: GNU General Public License Version 2                       */
//*                or any later version                                       */
//*****************************************************************************/
//*456789012345678 (80-character line to adjust editor window) 456789012345678*/


================================================================================
26-Jan-2016:

    CHANGES:

      This long-overdue update includes many many features worked on over a long
      period, so I may be forgetting some features in the list.

    * Line spacing can be adjusted with the ProofAsstLineSpacing RunParm.

    * Batch Commands are now handled uniformly, with automatic documentation
      populating the Help > Batch command documentation list.

    * A new more powerful form of Derive is introduced, called Autocomplete
      steps. This will be used in the future as a general "perform advanced
      simplifications" tactic. Control of the feature is provided by the
      'ProofAsstAutocompleteEnabled,Yes' step (enabled by default). It is
      recommended that 'ProofAsstDeriveAutocomplete,Yes' be enabled to get the
      full advantage of autocomplete steps, as this will automatically enable
      autocomplete on newly created steps (causing a cascade effect of
      derivations of multi-step proofs).

    * A definitional soundness checker has been added for set.mm. It can be run
      via

        SetMMDefinitionsCheckWithExclusions,ax-*,df-bi,df-clab,df-cleq,df-clel
          (deprecated)

      or

        RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel

      It will check the listed axioms against a simple test for conservativity.

    * Local refs can now be empty; a step '1:2,3:# |- formula' will search for
      previous steps deriving '|- formula' and merge the steps if one is found.

    * The autocomplete step framework is extended with Auto-transformations,
      which will detect commutative and associative operations and automatically
      derive equivalence proofs from a proven step to an autocomplete goal step.
      The behavior is enabled by the RunParm:

        ProofAsstUseAutotransformations,yes,no,yes

    * A macro system has been added, for writing extra functionality outside
      mmj2 in Javascript. Macros are stored in the mmj2jar/macros folder, and
      the current set of macros is designed for use with set.mm. Future
      set.mm-specific functionality (such as the definition checker above)
      should be added as macros, keeping the mmj2 source agnostic to any
      particular .mm framework.

      Macros are enabled by default, via 'MacrosEnabled,yes'. The macro folder
      can be set with MacroFolder, and the language can even be changed via
      MacroLanguage (this is not recommended, since all the pre-written macros
      are in Javascript and JRE 8 does not ship with any other script engines
      by default). Macros can be run either via RunParm using RunMacro, or by
      typing a $m statement into the proof text area such as

        $m echo Hello!

      Many macros also operate by hooking into any of several callbacks for
      various points during the read/unify/print loop. See macros/readme.js for
      more info.

    * A new parser, LRParser, has been implemented as an alternative to the
      standard EarleyParser. It can be selected with:
      
        SetParser,mmj.verify.LRParser

      It takes much longer to generate the initial parse table, but subsequent
      parsing is much faster under most conditions. The parse table problem
      is alleviated by saving and loading the parse table to a file (see the
      next point).

    * Saving and loading of settings has been implemented. The file store.json
      is a JSON file that contains many of the settings used by mmj2, and it is
      read just before RunProofAsstGUI and saved just before exit (if the
      program is exited correctly). This allows font settings, window
      positioning, etc. to persist between runs of the program, as well as
      caching expensive-to-compute data such as the LR parse tables. It is also
      designed to be at least somewhat human-readable; see store.json.

    * The entire codebase has been converted to use Java 8. This does not affect
      most users, but it will likely require that users upgrade to Java 8 if
      they have not already.

    * Steps can now refer to later steps, provided that no dependency cycles
      ensue. They will be automatically reordered on unification.

    * A new system for "reverse transformations" extends the auto-transformation
      system (with no change to the RunParm). This enables the loading of
      automatic reduction rules when the hypotheses are simpler than the
      conclusion, with no new variables. This is sufficient to support most
      kinds of closure proofs and equality proofs.

    * The transformations.js macro adds set.mm-specific transformation rules
      to the transformation system, which includes:
      
      - A long list of invalid reduction rules (so that the reverse
        transformation system does not apply undesirable reductions);

      - The arithmetic prover detailed in http://arxiv.org/abs/1503.02349;

      - Automatic structure detection for theorems that use structures from
        abstract algebra. For example, if the theorem hypothesis includes
        "|- .+ = ( +g ` G )", then any group theorem that has a similar
        hypothesis will match ".+" and "G" to the definitions at the top of the
        worksheet, and any other structure slots will be discharged via 'eqid'.
      

================================================================================
4-Feb-2014:

    CHANGES:

    * This update introduces the exiting new feature of syntax highlighting for
      mmp files. The tokenizer and token types are hardcoded, but you can
      customize the coloring and styling of the types using the new
      'ProofAsstHighlightingStyle' RunParm. You can also disable syntax
      highlighting altogether using 'ProofAsstHighlightingEnabled,no' if it is
      too much of a performance hit.

================================================================================
2-Jan-2014:

    CHANGES:

    * The compression format has been updated to match the new compression
      default of the metamath.exe program.

    * Parse tree compression is now more efficient, which means that loading
      completed proof worksheets and unifying a completed proof is faster.

    * Bug fix for 17-Aug change, where steps with no variables or hypotheses
      (such as the example below) would not be collapsed into a single step.

================================================================================
17-Aug-2013:

    CHANGES:

    * New proofs loaded via 'New-Next Proof' and related functions now have a
      step layout that mirrors the compressed format instead of the uncompressed
      RPN. This means that if a given step is referred to twice in a proof, the
      step will only be assigned one step number, rather than making copies of
      the statement for each use. (Depending on the proof, this can mean a
      drastic decrease in the length of proofs as seen in the main text area of
      ProofAsstGUI. The length of compressed and uncompressed proofs themselves
      remains unaffected.) For example:
      Before:                             After:
        1::tru          |- T.               1::tru          |- T.
        2::tru          |- T.               qed:1,1:pm3.2i |- ( T. /\ T. )
        qed:1,2:pm3.2i |- ( T. /\ T. )

    * New menu items "Unify+Don't Convert WorkVars" and "Unify+Erase+Don't
      Convert" have been added to the Unify menu. When activated, they perform
      the regular unification process, but if the process completes successfully
      except that work variables (i.e. &C1, &S2, etc.) are in use in the
      derivation steps, it will abort the unification process and move the
      cursor to the first step containing a work variable, so that you can name
      it properly. (The default option "Unify" will instead replace these
      variables with dummy variables that have been taken from the pool of
      unused variables defined in the .mm file.)

    * The "Reformat" options no longer require you to save the file.

================================================================================
13-Aug-2013:

    CHANGES:

    * New proofs are now output by default in "compressed" format. This behavior
      can be modified by the TL > Set Proof Compression option in ProofAsstGUI
      or by setting the ProofAsstProofFormat RunParm (to Compressed, Packed, or
      Normal).

    * The code base target has been upgraded to 1.5 compatibility, and features
      of Java 1.5 (primarily generics and enhanced for loops) have been utilized
      throughout the program.

    * Mel O'Cat's original search enhancements have been added to the project,
      although since the source was decompiled from the release jar file,
      comments and local variable names are missing. Primary documentation can
      be found at

        mmj2/doc/Release20121225/MMJ2_Release_20121225_Proposals.html

      although that source is a proposal of new features, which includes a few
      that were never implemented.

    * Step names are no longer required to be ints, and are now allowed to be
      arbitrary strings, with a few limitations.

      - Since step names are matched case-insensitively, capital letters are
        allowed, but will be normalized to lowercase upon the next unify.
      - The space character and , and : are not allowed, for obvious reasons.
      - There are two 'keywords' for step names: if the name is
        (case-insensitively) equal to 'qed', it is identified as the final step,
        and if the name begins with 'h', it is a hypothesis step.

    * The default renumber settings have been changed, so that the numbering on
      load and on renumber go up by tens, while the steps generated by Derive go
      up by ones, but have a 'd' prefix, i.e. 'd1', 'd2', etc.

    * The 'Step Search' / 'General Search' and 'Step Selector Search' dialogs
      now use multiline list entries, so that selecting one assertion selects
      all the lines of that assertion.

    * The 'Request Messages' dialog has been deprecated, as the exact same
      content is available in the lower pane of ProofAsstGUI. The compile-time
      constant PaConstants.REQUEST_MESSAGES_GUI_ENABLED controls this new
      behavior.

    * A new RunParm 'ProofAsstLookAndFeel' now controls the Swing L&F for the
      whole application. The default option (and whatwe used before this update)
      is 'Metal', and a list of options (which are OS-dependent) is presented if
      you type an incorrect option. (I recommend 'Nimbus', if available.)

    * A new RunParm 'ProofAsstMaximized' now allows ProofAsstGUI to start in
      fullscreen mode.

    * Added support for compound edits for undo handling. This way, undo and
      redo apply to entire blocks of text, rather than individual characters as
      before. Furthermore (and most importantly), the full-buffer replacements
      performed by Unify now count as a single edit, so you only have to Ctrl-Z
      once to undo/redo unification.

    * Fixed a bug wherein the cursor is positioned at steps with LocalRefs (say
      because the user just typed the LocalRef), but since the step is deleted
      during processing, the cursor loses its anchor and ends up at the top of
      the file. (Very annoying!) Now, the cursor is never positioned at LocalRef
      steps and instead goes to the first non-LocalRef step after the cursor.

    * Malformed steps with only one colon are now interpreted as step:ref
      instead of step:hyp if the second field starts with # (i.e. a LocalRef) or
      it is a theorem or hypothesis in the database (no unification checks are
      done; it is just a heuristic).

    * Steps with no ref and no formula are no longer fatal unification errors.
      Instead, they simply fail to unify, and give errors just like steps with
      formulas, which is to say that step:: alone on a line gives error

          E-PA-0411: Unification failure in derivation proof step.

      and step:?: on a line gives no error at all.

    * All the supplementary dialogs like Step Selector Search, Search Options,
      and the Search Results window now close on ESC (they used to close on
      ALT-F4, but it is easy to make a mistake and close something you don't
      want to close using that key combo). 

================================================================================
1-Nov-2011:

    CHANGES:

    This release includes small but excellent enhancements and a minor
    but important bug fix.

    -----------------------------------------------------------------
    1. Quick Start (see also mmj2\QuickStart.html)
    -----------------------------------------------------------------

       Quick Start!!!:

       Windows:  Double-click mmj2\mmj2jar\mmj2.bat in Windows Explorer

       Mac OS-X: Double-click mmj2\mmj2jar\MacMMJ2.command in Finder


       BUT...WAIT!...before running mmj2, edit, if needed:

       EDIT-->Windows    mmj2\mmj2jar\RunParms.txt
              using      mmj2\mmj2jar\mmj2.bat
              Notepad:   mmj2\mmj2jar\mmj2PATutorial.bat

           -->Mac OS-X   mmj2\mmj2jar\RunParms.txt
              using      mmj2\mmj2jar\MacRunParmsPATutorial.txt
              TextEdit:  mmj2\mmj2jar\MacMMJ2.command
                         mmj2\mmj2jar\MacMMJ2PATutorial.command

       (Double-click works well now because the new "mmj2 Fail Popup
       Window" *not only* provides start-up and "fail" error
       messages, but it also forces the Windows Command Prompt (Mac
       OS-X utilities\terminal.app) window to stay open, which makes
       it possible to see all of the mmj2 output about the error.)

    -----------------------------------------------------------------
    2. RunParms.txt and The mmj2.jar Command Line Arguments Revamped.
    -----------------------------------------------------------------

       The new release contains a serious revamp of both RunParms.txt
       and the command line arguments for mmj2.jar. It has several
       features of interest to the mmj2 user!

       Unless you have been using your own modified version of mmj2.bat
       and/or RunParms.txt you don't need to do anything special to
       take advantage of these new features. Just use the new release
       versions of mmj2.bat and RunParms.txt. (If you have your own
       copies of these files they will -- most likely -- require minor
       adjustments.)

       In brief:

           - New command line arguments specify data Paths for mmj2,
             Metamath and the mmj2 Service feature. These make mmj2
             easier to use in Windows, Mac OS-X and Linux environments
             as well as making it easier to customize your mmj2
             installation.

           - MMJ2 Fail Popup Window which is displayed when startup or
             premature termination errors in mmj2 are encountered.
             Specify 'N' on the command line to disable this feature.

           - The Command Line "Argument Option" report is extremely
             useful during installation, customization and testing of
             mmj2! It is output to Sysout at startup and provides an
             audit trail of the program version and input command line
             arguments. In the event of errors in the command line
             arguments, the program tries to print as much as possible
             of the Argument Option report, up to the point where a
             command line argument error is detected -- and the last
             line of the report printed will correspond to the invalid
             argument!

           - RunParms.txt is now maximally concise. This represents a
             philosophical change. Previously, RunParms.txt contained
             every possible RunParm command with the hard-coded default
             specified (or asterisked-out). This was confusing and
             unhelpful in two ways: 1) there are so many commands that
             it was hard to see the important RunParms; and 2) at
             startup mmj2 "echoes" each RunParm as it is executed and
             this resulted in a bewildering barrage of output to
             Sysout. The old version of RunParms.txt is now maintained
             for reference purposes as RunParmsComplete.txt.

           - All of the batch unit/volume regression tests have been
             modified to take advantage of the Paths Enhancement.
             Hardcoding of "C:\" exists only in the top level .bat
             files -- and in a few cases "C:\" is coded for testing
             purposes. These tests are now much more portable (to non-
             Windows environments such as OS-X and Unix/Linux.)


       Additional documentation at:

           mmj2\doc\mmj2CommandLineArguments.html


    ------------------------------------------------------------
    3. New! GMFF (Graphics Mode Formula Formatting) Enhancement.
    ------------------------------------------------------------

       What is great about this feature is that it helps users see
       right away what the Metamath ASCII formulas look like when
       rendered in html (or Latex, etc.) Simply press Ctrl-1 (One) on
       the Proof Assistant GUI screen to generate export file(s) via
       GMFF -- use Alt-Tab to switch back and forth between the Proof
       Assistant GUI and your browser window.

           - NOTE: default setting for GMFF Export of a Proof Worksheet
                   or theorem is to create both .html and .althtml
                   versions (.gif and Unicode), and to write these
                   to fileS named "general.html":

                       - mmj2jar\gmff\html\general.html

                       and

                       - mmj2jar\gmff\althtml\general.html

                   IF you prefer to use export file names composed of
                   the Theorem Label + ".html" and/or to disable
                   either the html or the althtml versions,
                   THEN copy the "GMFFExportParms" RunParm lines from
                   mmj2jar\RunParmsComplete.txt to your version
                   of RunParms.txt.

                       *GMFFExportParms,althtml,ON,althtmldef,GMFF\althtml,.html,GMFF\models\althtml,A,ISO-8859-1,general
                       *GMFFExportParms,html,ON,htmldef,GMFF\html,.html,GMFF\models\html,A,ISO-8859-1,general

                   Then un-asterisk the commands, change "ON" to "OFF"
                   and/or erase "general" (leaving the option blank
                   allows the default to be used, which is to use Theorem
                   Label in the export file name):

                       GMFFExportParms,althtml,OFF,althtmldef,GMFF\althtml,.html,GMFF\models\althtml,A,ISO-8859-1,general
                       GMFFExportParms,html,ON,htmldef,GMFF\html,.html,GMFF\models\html,A,ISO-8859-1,


       GMFF uses the typesetting information embedded in Metamath files
       such as set.mm -- see Metamath Comment statement containing "$t"
       -- to export files in other formats, such as as html and Latex.
       At this time only html files have been generated but the GMFF
       enhancement uses "Model" files in the mmj2 release to generate
       its output and the types of files output are not restricted as
       long as:

       a) the output formula text is based on text strings, not parse
          trees (as would be the case, for example, with MathML
          output). And...

       b) the structure of an individual export file can be made to fit
          the structure of the available Model files. At this point
          only Model "A" is available, but considerable effort was made
          in programming to build in flexibility in the way a Model
          file is used.

       Modification of mmj2 code will be necessary if new Models are
       required. Modification to use parse trees instead of formula
       strings is doable but will require non-trivial changes. '

       Refer to mmj2\doc\GMFFDoc\* for details.


    ----------------------------------------------
    4. Incomplete Step Cursor Positioning Bug Fix.
    ----------------------------------------------

       After Unification (Ctrl-U) the cursor was being moved in spite
       of RunParm "ProofAsstIncompleteStepCursor,AsIs". And worse, the
       ViewPort output lines were being scrolled so that the first line
       on the screen matched the cursor location every time. Now, with
       "AsIs" the cursor is repositioned only when there are proof
       errors, or when unification is successful and a Metamath RPN
       proof is generated.

       See: mmj2/doc/IncompleteStepCursorPositioning.html

       and  mmj2/doc/ProofAsstGUICursorHandling.html

       NOTE: The RunParm "ProofAsstIncompleteStepCursor" default
             setting is now "AsIs" instead of "Last". If you prefer the
             old setting you can customize RunParms.txt by adding:

                 ProofAsstIncompleteStepCursor,Last

             just before the "RunProofAsstGUI" RunParm (the other
             option is "First").


Documentation:

    New:

        mmj2\QuickStart.html

        mmj2\doc\GMFFDoc\
        mmj2\doc\GMFFDoc\GMFFFolders.txt
        mmj2\doc\GMFFDoc\GMFFModels.txt
        mmj2\doc\GMFFDoc\GMFFRunParms.txt
        mmj2\doc\GMFFDoc\README.html
        mmj2\doc\GMFFDoc\SampleRunParms.txt
        mmj2\doc\GMFFDoc\GMFF.jpg

        mmj2\doc\ReleaseNotes20111101.html

        mmj2\mmj2jar\PATutorial\Page413.mmp


    Changed:

        mmj2\CHGLOG.TXT
        mmj2\doc\BottomUpProving-ByNormMegill.html
        mmj2\doc\FinalizeReleaseTodos.txt
        mmj2\doc\mmj2CommandLineArguments.html
        mmj2\doc\RegressionTestResults.txt
        mmj2\doc\RunningTheMMJ2TestSuite.html

        mmj2\INSTALL.html
        mmj2\LicenseEnclosure.java
        mmj2\mmj2.html
        mmj2\README.html

        mmj2\mmj2jar\PATutorial\Page101.mmp
        mmj2\mmj2jar\PATutorial\Page102.mmp
        mmj2\mmj2jar\PATutorial\Page103.mmp
        mmj2\mmj2jar\PATutorial\Page201.mmp
        mmj2\mmj2jar\PATutorial\Page202.mmp
        mmj2\mmj2jar\PATutorial\Page203.mmp
        mmj2\mmj2jar\PATutorial\Page204.mmp
        mmj2\mmj2jar\PATutorial\Page301.mmp
        mmj2\mmj2jar\PATutorial\Page302.mmp
        mmj2\mmj2jar\PATutorial\Page303.mmp
        mmj2\mmj2jar\PATutorial\Page304.mmp
        mmj2\mmj2jar\PATutorial\Page401.mmp
        mmj2\mmj2jar\PATutorial\Page402.mmp
        mmj2\mmj2jar\PATutorial\Page403.mmp
        mmj2\mmj2jar\PATutorial\Page404.mmp
        mmj2\mmj2jar\PATutorial\Page405.mmp
        mmj2\mmj2jar\PATutorial\Page406.mmp
        mmj2\mmj2jar\PATutorial\Page407.mmp
        mmj2\mmj2jar\PATutorial\Page408.mmp
        mmj2\mmj2jar\PATutorial\Page409.mmp
        mmj2\mmj2jar\PATutorial\Page410.mmp
        mmj2\mmj2jar\PATutorial\Page411.mmp
        mmj2\mmj2jar\PATutorial\Page412.mmp (all new content!!!)


    Deleted:

        mmj2\MacOSXIssues.txt
        mmj2\mmj2jar\LICENSE.TXT
        mmj2\mmj2jar\LicenseEnclosure.java
        mmj2\mmj2jar\SunJavaTutorialLicense.html


Source Code:

    New:

        mmj2\src\mmj\gmff\GMFFUserTextEscapes.java
        mmj2\src\mmj\gmff\MinCommentStmt.java
        mmj2\src\mmj\gmff\GMFFException.java
        mmj2\src\mmj\gmff\MinDerivationStep.java
        mmj2\src\mmj\gmff\GMFFExportFile.java
        mmj2\src\mmj\gmff\GMFFExporterTypesetDefs.java
        mmj2\src\mmj\gmff\GMFFExportParms.java
        mmj2\src\mmj\gmff\GMFFFileNotFoundException.java
        mmj2\src\mmj\gmff\GMFFInputFile.java
        mmj2\src\mmj\gmff\GMFFExporter.java
        mmj2\src\mmj\gmff\GMFFMandatoryModelNotFoundException.java
        mmj2\src\mmj\gmff\GMFFFolder.java
        mmj2\src\mmj\gmff\GMFFFileFilter.java
        mmj2\src\mmj\gmff\GMFFManager.java
        mmj2\src\mmj\gmff\GMFFUserExportChoice.java
        mmj2\src\mmj\gmff\ProofWorksheetCache.java
        mmj2\src\mmj\gmff\GMFFConstants.java
        mmj2\src\mmj\gmff\TypesetDefCommentParser.java
        mmj2\src\mmj\gmff\EscapePair.java
        mmj2\src\mmj\gmff\MinDistinctVariablesStmt.java
        mmj2\src\mmj\gmff\MinHeaderStmt.java
        mmj2\src\mmj\gmff\MinFooterStmt.java
        mmj2\src\mmj\gmff\MinGeneratedProofStmt.java
        mmj2\src\mmj\gmff\MinProofStepStmt.java
        mmj2\src\mmj\gmff\MinProofWorkStmt.java
        mmj2\src\mmj\gmff\MinProofWorksheet.java
        mmj2\src\mmj\gmff\MinHypothesisStep.java
        mmj2\src\mmj\gmff\ModelAExporter.java

        mmj2\src\mmj\util\GMFFBoss.java
        mmj2\src\mmj\util\MMJ2FailPopupWindow.java
        mmj2\src\mmj\util\CommandLineArguments.java
        mmj2\src\mmj\util\Paths.java


    Changed:

        mmj2\src\mmj\lang\Axiom.java
        mmj2\src\mmj\lang\LangConstants.java
        mmj2\src\mmj\lang\LogHyp.java
        mmj2\src\mmj\lang\LogicalSystem.java
        mmj2\src\mmj\lang\SystemLoader.java
        mmj2\src\mmj\lang\Theorem.java

        mmj2\src\mmj\mmio\IncludeFile.java
        mmj2\src\mmj\mmio\MMIOConstants.java
        mmj2\src\mmj\mmio\Statementizer.java
        mmj2\src\mmj\mmio\Systemizer.java

        mmj2\src\mmj\pa\AuxFrameGUI.java
        mmj2\src\mmj\pa\PaConstants.java
        mmj2\src\mmj\pa\ProofAsst.java
        mmj2\src\mmj\pa\ProofAsstCursor.java
        mmj2\src\mmj\pa\ProofAsstGUI.java
        mmj2\src\mmj\pa\ProofWorksheet.java

        mmj2\src\mmj\tl\MMTFolder.java
        mmj2\src\mmj\tl\TlConstants.java
        mmj2\src\mmj\tl\TlPreferences.java

        mmj2\src\mmj\tmff\TMFFConstants.java
        mmj2\src\mmj\tmff\TMFFPreferences.java

        mmj2\src\mmj\util\BatchFramework.java
        mmj2\src\mmj\util\BatchMMJ2.java
        mmj2\src\mmj\util\Boss.java
        mmj2\src\mmj\util\Dump.java
        mmj2\src\mmj\util\LogicalSystemBoss.java
        mmj2\src\mmj\util\OutputBoss.java
        mmj2\src\mmj\util\ProofAsstBoss.java
        mmj2\src\mmj\util\RunParmFile.java
        mmj2\src\mmj\util\SvcBoss.java
        mmj2\src\mmj\util\TheoremLoaderBoss.java
        mmj2\src\mmj\util\UtilConstants.java

        mmj2\src\mmj\verify\GrammarConstants.java
        mmj2\src\mmj\verify\ProofConstants.java
        mmj2\src\mmj\verify\VerifyProofs.java

Data:

    New:

        mmj2\data\gmfftest\
        mmj2\data\gmfftest\19.21adv.mmp
        mmj2\data\gmfftest\a2i.mmp
        mmj2\data\gmfftest\pm2.38.mmp
        mmj2\data\gmfftest\syllogism.mmp
        mmj2\data\gmfftest\a1i.mmt

        mmj2\data\gmfftest\models\althtml\AM-file0.txt
        mmj2\data\gmfftest\models\althtml\AM-file2.txt
        mmj2\data\gmfftest\models\althtml\AM-step0.txt
        mmj2\data\gmfftest\models\althtml\AM-step1X.txt
        mmj2\data\gmfftest\models\althtml\AM-step2.txt
        mmj2\data\gmfftest\models\althtml\AM-step3X.txt
        mmj2\data\gmfftest\models\althtml\AM-step4.txt
        mmj2\data\gmfftest\models\althtml\AO-comment0.txt
        mmj2\data\gmfftest\models\althtml\AO-comment1X.txt
        mmj2\data\gmfftest\models\althtml\AO-comment2.txt
        mmj2\data\gmfftest\models\althtml\AO-distinctvar0.txt
        mmj2\data\gmfftest\models\althtml\AO-distinctvar1X.txt
        mmj2\data\gmfftest\models\althtml\AO-distinctvar2.txt
        mmj2\data\gmfftest\models\althtml\AO-distinctvar3X.txt
        mmj2\data\gmfftest\models\althtml\AO-distinctvar4.txt
        mmj2\data\gmfftest\models\althtml\AO-footer0.txt
        mmj2\data\gmfftest\models\althtml\AO-genproof0.txt
        mmj2\data\gmfftest\models\althtml\AO-genproof1X.txt
        mmj2\data\gmfftest\models\althtml\AO-genproof2.txt
        mmj2\data\gmfftest\models\althtml\AO-header0.txt
        mmj2\data\gmfftest\models\althtml\AO-header1X.txt
        mmj2\data\gmfftest\models\althtml\AO-header2.txt
        mmj2\data\gmfftest\models\althtml\AO-header3X.txt
        mmj2\data\gmfftest\models\althtml\AO-header4.txt
        mmj2\data\gmfftest\models\althtml\AO-header5X.txt
        mmj2\data\gmfftest\models\althtml\AO-header6.txt
        mmj2\data\gmfftest\models\althtml\AO-header7.txt

        mmj2\data\gmfftest\models\html\AM-file0.txt
        mmj2\data\gmfftest\models\html\AM-file2.txt
        mmj2\data\gmfftest\models\html\AM-step0.txt
        mmj2\data\gmfftest\models\html\AM-step1X.txt
        mmj2\data\gmfftest\models\html\AM-step2.txt
        mmj2\data\gmfftest\models\html\AM-step3X.txt
        mmj2\data\gmfftest\models\html\AM-step4.txt
        mmj2\data\gmfftest\models\html\AO-comment0.txt
        mmj2\data\gmfftest\models\html\AO-comment1X.txt
        mmj2\data\gmfftest\models\html\AO-comment2.txt
        mmj2\data\gmfftest\models\html\AO-distinctvar0.txt
        mmj2\data\gmfftest\models\html\AO-distinctvar1X.txt
        mmj2\data\gmfftest\models\html\AO-distinctvar2.txt
        mmj2\data\gmfftest\models\html\AO-distinctvar3X.txt
        mmj2\data\gmfftest\models\html\AO-distinctvar4.txt
        mmj2\data\gmfftest\models\html\AO-footer0.txt
        mmj2\data\gmfftest\models\html\AO-genproof0.txt
        mmj2\data\gmfftest\models\html\AO-genproof1X.txt
        mmj2\data\gmfftest\models\html\AO-genproof2.txt
        mmj2\data\gmfftest\models\html\AO-header0.txt
        mmj2\data\gmfftest\models\html\AO-header1X.txt
        mmj2\data\gmfftest\models\html\AO-header2.txt
        mmj2\data\gmfftest\models\html\AO-header3X.txt
        mmj2\data\gmfftest\models\html\AO-header4.txt
        mmj2\data\gmfftest\models\html\AO-header5X.txt
        mmj2\data\gmfftest\models\html\AO-header6.txt
        mmj2\data\gmfftest\models\html\AO-header7.txt

        mmj2\data\gmfftest\myproofs\a2i.mmp

        mmj2\data\mm\DollarT099.mm
        mmj2\data\mm\DollarT046.mm
        mmj2\data\mm\DollarT033.mm
        mmj2\data\mm\big-unifier.mm
        mmj2\data\mm\DollarT045.mm
        mmj2\data\mm\DollarT032.mm
        mmj2\data\mm\DollarT022.mm
        mmj2\data\mm\DollarTPreface.mm
        mmj2\data\mm\DollarTFirst100.mm
        mmj2\data\mm\DollarT026.mm
        mmj2\data\mm\DollarT025.mm
        mmj2\data\mm\DollarT024.mm
        mmj2\data\mm\DollarT023.mm
        mmj2\data\mm\DollarT011.mm
        mmj2\data\mm\DollarT098.mm
        mmj2\data\mm\DollarT012.mm
        mmj2\data\mm\DollarT021.mm
        mmj2\data\mm\DollarT019.mm
        mmj2\data\mm\DollarT020.mm
        mmj2\data\mm\DollarT017.mm
        mmj2\data\mm\DollarT015.mm
        mmj2\data\mm\DollarT016.mm
        mmj2\data\mm\DollarT018.mm
        mmj2\data\mm\DollarT013.mm
        mmj2\data\mm\DollarT014.mm
        mmj2\data\mm\DollarT002.mm
        mmj2\data\mm\DollarT010.mm
        mmj2\data\mm\DollarT001.mm
        mmj2\data\mm\DollarT008.mm
        mmj2\data\mm\DollarT007.mm
        mmj2\data\mm\DollarT009.mm
        mmj2\data\mm\DollarT006.mm
        mmj2\data\mm\DollarT005.mm
        mmj2\data\mm\DollarT003.mm
        mmj2\data\mm\DollarT004.mm
        mmj2\data\mmp\tests\esnnei.mmp

        mmj2\data\runparm\windows\VT2aPA002.txt
        mmj2\data\runparm\windows\UT11GMFF01.txt
        mmj2\data\runparm\windows\UT11GMFF02.txt
        mmj2\data\runparm\windows\UT11GMFF03.txt
        mmj2\data\runparm\windows\UT11GMFF04.txt
        mmj2\data\runparm\windows\UT11GMFF05.txt
        mmj2\data\runparm\windows\UT11GMFF06.txt
        mmj2\data\runparm\windows\UT11GMFF07.txt
        mmj2\data\runparm\windows\UT11GMFF08.txt

        mmj2\mmj2jar\gmff\

        mmj2\mmj2jar\gmff\althtml\general.html
        mmj2\mmj2jar\gmff\althtml\langle.gif (from Metamath Symbols.zip)
        mmj2\mmj2jar\gmff\althtml\rangle.gif (from Metamath Symbols.zip)

        mmj2\mmj2jar\gmff\html\general.html
        mmj2\mmj2jar\gmff\html\*.gif         (from Metamath Symbols.zip)

        mmj2\mmj2jar\gmff\models\althtml\AM-file0.txt
        mmj2\mmj2jar\gmff\models\althtml\AM-file2.txt
        mmj2\mmj2jar\gmff\models\althtml\AM-step0.txt
        mmj2\mmj2jar\gmff\models\althtml\AM-step1X.txt
        mmj2\mmj2jar\gmff\models\althtml\AM-step2.txt
        mmj2\mmj2jar\gmff\models\althtml\AM-step3X.txt
        mmj2\mmj2jar\gmff\models\althtml\AM-step4.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-comment0.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-comment1X.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-comment2.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar0.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar1X.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar2.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar3X.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-distinctvar4.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-footer0.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-genproof0.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-genproof1X.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-genproof2.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-header0.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-header1X.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-header2.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-header3X.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-header4.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-header5X.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-header6.txt
        mmj2\mmj2jar\gmff\models\althtml\AO-header7.txt

        mmj2\mmj2jar\gmff\models\html\AM-file0.txt
        mmj2\mmj2jar\gmff\models\html\AM-file2.txt
        mmj2\mmj2jar\gmff\models\html\AM-step0.txt
        mmj2\mmj2jar\gmff\models\html\AM-step1X.txt
        mmj2\mmj2jar\gmff\models\html\AM-step2.txt
        mmj2\mmj2jar\gmff\models\html\AM-step3X.txt
        mmj2\mmj2jar\gmff\models\html\AM-step4.txt
        mmj2\mmj2jar\gmff\models\html\AO-comment0.txt
        mmj2\mmj2jar\gmff\models\html\AO-comment1X.txt
        mmj2\mmj2jar\gmff\models\html\AO-comment2.txt
        mmj2\mmj2jar\gmff\models\html\AO-distinctvar0.txt
        mmj2\mmj2jar\gmff\models\html\AO-distinctvar1X.txt
        mmj2\mmj2jar\gmff\models\html\AO-distinctvar2.txt
        mmj2\mmj2jar\gmff\models\html\AO-distinctvar3X.txt
        mmj2\mmj2jar\gmff\models\html\AO-distinctvar4.txt
        mmj2\mmj2jar\gmff\models\html\AO-footer0.txt
        mmj2\mmj2jar\gmff\models\html\AO-genproof0.txt
        mmj2\mmj2jar\gmff\models\html\AO-genproof1X.txt
        mmj2\mmj2jar\gmff\models\html\AO-genproof2.txt
        mmj2\mmj2jar\gmff\models\html\AO-header0.txt
        mmj2\mmj2jar\gmff\models\html\AO-header1X.txt
        mmj2\mmj2jar\gmff\models\html\AO-header2.txt
        mmj2\mmj2jar\gmff\models\html\AO-header3X.txt
        mmj2\mmj2jar\gmff\models\html\AO-header4.txt
        mmj2\mmj2jar\gmff\models\html\AO-header5X.txt
        mmj2\mmj2jar\gmff\models\html\AO-header6.txt
        mmj2\mmj2jar\gmff\models\html\AO-header7.txt

        mmj2\mmj2jar\MacRunParmsPATutorial.txt
        mmj2\mmj2jar\RunParmsQL.txt
        mmj2\mmj2jar\RunParmsComplete.txt

    Changed:

        mmj2\data\runparm\windows\PTAPGc7s1p146.txt
        mmj2\data\runparm\windows\PTAPGc7s1p148.txt
        mmj2\data\runparm\windows\PTAPGc7s2p160.txt
        mmj2\data\runparm\windows\Sample001.txt
        mmj2\data\runparm\windows\Sample002.txt
        mmj2\data\runparm\windows\Sample003.txt
        mmj2\data\runparm\windows\UT2PA001.txt
        mmj2\data\runparm\windows\UT3LA001.txt
        mmj2\data\runparm\windows\UT10001.txt
        mmj2\data\runparm\windows\UT4001.txt
        mmj2\data\runparm\windows\UT5001.txt
        mmj2\data\runparm\windows\UT6001.txt
        mmj2\data\runparm\windows\UT7001.txt
        mmj2\data\runparm\windows\UT9001.txt
        mmj2\data\runparm\windows\UT9002.txt
        mmj2\data\runparm\windows\UT9003.txt
        mmj2\data\runparm\windows\UT10002.txt
        mmj2\data\runparm\windows\UT10003.txt
        mmj2\data\runparm\windows\UT10021.txt
        mmj2\data\runparm\windows\UT10022.txt
        mmj2\data\runparm\windows\UT10023.txt
        mmj2\data\runparm\windows\UT10031.txt
        mmj2\data\runparm\windows\UT10032.txt
        mmj2\data\runparm\windows\UT10033.txt
        mmj2\data\runparm\windows\UT10041.txt
        mmj2\data\runparm\windows\UT10042.txt
        mmj2\data\runparm\windows\UT10043.txt
        mmj2\data\runparm\windows\UT10051.txt
        mmj2\data\runparm\windows\UT10052.txt
        mmj2\data\runparm\windows\UT10053.txt
        mmj2\data\runparm\windows\UT19100.txt
        mmj2\data\runparm\windows\UTGR1c01.txt
        mmj2\data\runparm\windows\UTGR1c02.txt
        mmj2\data\runparm\windows\UTGR1c03.txt
        mmj2\data\runparm\windows\UTGR1c04.txt
        mmj2\data\runparm\windows\UTGR1c05.txt
        mmj2\data\runparm\windows\UTGR1c05.txt
        mmj2\data\runparm\windows\UTGR1c06.txt
        mmj2\data\runparm\windows\UTIO1c01.txt
        mmj2\data\runparm\windows\UTIO1c02.txt
        mmj2\data\runparm\windows\UTIO1c03.txt
        mmj2\data\runparm\windows\UTIO1c04.txt
        mmj2\data\runparm\windows\UTIO1c05.txt
        mmj2\data\runparm\windows\UTIO1c06.txt
        mmj2\data\runparm\windows\UTIO1c07.txt
        mmj2\data\runparm\windows\UTIO1c08.txt
        mmj2\data\runparm\windows\UTLA1c01.txt
        mmj2\data\runparm\windows\UTLA1c02.txt
        mmj2\data\runparm\windows\UTPR1c01.txt
        mmj2\data\runparm\windows\VT2bPA002.txt
        mmj2\data\runparm\windows\VT2cPA002.txt
        mmj2\data\runparm\windows\VT2dPA002.txt
        mmj2\data\runparm\windows\VT2ePA002.txt

        mmj2\doc\mmj2Service\TSvcCallbackCalleeRunParms.txt
        mmj2\doc\mmj2Service\TSvcCallbackCallerRunParms.txt

        mmj2\mmj2jar\AnnotatedRunParms.txt
        mmj2\mmj2jar\RunParms.txt
        mmj2\mmj2jar\RunParmsPATutorial.txt
        mmj2\mmj2jar\RunParmsPeanoInfix.txt

        mmj2\mmj2jar\setFirst100.mm

    Deleted:

        mmj2\data\runparm\windows\VT2PA002.txt

Object Code:

    Changed:

        mmj2jar\mmj2.jar

Other:

    New:

        mmj2\compile\mmj\gmff\gmffClasses.txt
        mmj2\mmj2jar\CopySymbols.bat
        mmj2\mmj2jar\MacMMJ2.command
        mmj2\mmj2jar\MacMMJ2PATutorial.command
        mmj2\mmj2jar\mmj2QL.bat

    Changed:

        mmj2\compile\mmj\util\utilClasses.txt
        mmj2\compile\windows\CompMMJ.bat
        mmj2\compile\windows\EraseMMJObjCode.bat
        mmj2\compile\windows\mkjarargs.txt

        mmj2\doc\mmj2Service\TjavacTCompilePaths.txt
        mmj2\doc\mmj2Service\TSvcCallbackCallee.bat
        mmj2\doc\mmj2Service\TSvcCallbackCaller.bat

        mmj2\doc\windows\DocPackages.txt

        mmj2\mmj2jar\mmj2.bat
        mmj2\mmj2jar\mmj2PATutorial.bat
        mmj2\mmj2jar\mmj2PeanoInfix.bat

        mmj2\test\windows\RunBatchTest.bat
        mmj2\test\windows\RunSample001.bat
        mmj2\test\windows\RunSample002.bat
        mmj2\test\windows\RunSample003.bat
        mmj2\test\windows\RunUnitTest1.bat
        mmj2\test\windows\RunUnitTest2.bat
        mmj2\test\windows\RunUnitTest3.bat
        mmj2\test\windows\RunUnitTest4.bat
        mmj2\test\windows\RunUnitTest5.bat
        mmj2\test\windows\RunUnitTest6.bat
        mmj2\test\windows\RunUnitTest10.bat
        mmj2\test\windows\RunUnitTest11.bat
        mmj2\test\windows\RunUnitTest7.bat
        mmj2\test\windows\RunUnitTest8.bat
        mmj2\test\windows\RunUnitTest9.bat
        mmj2\test\windows\RunUT1.bat
        mmj2\test\windows\RunUT2.bat
        mmj2\test\windows\RunUT3.bat
        mmj2\test\windows\RunUT4.bat
        mmj2\test\windows\RunUT5.bat
        mmj2\test\windows\RunUT6.bat
        mmj2\test\windows\RunUT7.bat
        mmj2\test\windows\RunUT8.bat
        mmj2\test\windows\RunUT10.bat
        mmj2\test\windows\RunUT11.bat
        mmj2\test\windows\RunUT9.bat
        mmj2\test\windows\RunVolumeTest2a.bat
        mmj2\test\windows\RunVolumeTest2b.bat
        mmj2\test\windows\RunVolumeTest2c.bat
        mmj2\test\windows\RunVolumeTest2d.bat
        mmj2\test\windows\RunVolumeTest2e.bat
        mmj2\test\windows\RunVT2a.bat
        mmj2\test\windows\RunVT2b.bat
        mmj2\test\windows\RunVT2c.bat
        mmj2\test\windows\RunVT2d.bat
        mmj2\test\windows\RunVT2e.bat
        mmj2\test\windows\Sample001.bat
        mmj2\test\windows\Sample002.bat
        mmj2\test\windows\Sample003.bat

    Deleted:

        mmj2\test\windows\BatchMMJ2Sample001.bat
        mmj2\test\windows\BatchMMJ2Sample002.bat
        mmj2\test\windows\BatchMMJ2Sample003.bat
        mmj2\test\windows\RunBatchFramework.bat
        mmj2\test\windows\RunPAGUI.bat
        mmj2\test\windows\RunUnitTest.bat
        mmj2\test\windows\RunVolumeTest2.bat
        mmj2\test\windows\RunVT2.bat



==================================================================
1-Jul-2011:

    CHANGES:

    This is a bug fix release.

    1. Miscellaneous Bug Fixes:

        a) Fixed a bug in the parser which prevented construction
           of a parse tree for formulas consisting of just one
           constant symbol (in addition to the type code constant.)
           A "pre-parse" optimization handles "Named-Typed
           Constants" which appear in only one syntax axiom. In
           the special case where this was the only parsing action
           required, EarleyParser.java sent the affected formulas
           into the regular parsing algorithm following the pre-parse
           optimization. Unfortunately. the regular algoritm didn't
           "see" any parsing left to do and did not construct a
           parse tree. An example formula is "trutru". The relevant
           (defective) unit test .mm file has been updated.

    2. Added mmj2\data\mm\RegressionTest1set.mm -- which is the
       Feb. 25, 2008 version of set.mm. This archived copy of
       set.mm is now used for running the MMJ2 Test Suite.

       Due to label and symbol changes over time the mmj2 Test
       Suite suffers entropic decay! So, a fixed copy of set.mm
       will be used for regression testing (excluding the volume
       tests).

    3. Adjusted RunParm data and code defaults for the increased
       sizes of SymTbl and StmtTbl (1500 and 45000 respectively.)

       Also increased memory allocations in C:\mmj2\mmj2jar\mmj2.bat
       as follows: Total Memory   = 128M (was 64M),
                   Maximum Memory = 256M (was 128M).

    4. Added mmj2\doc\RegressionTestResults.txt and
             mmj2\doc\RegressionTestResultsForm.txt

       Documents differences between the new and old software output
       when run using mmj2\data\mm\RegressionTest1set.mm.


Documentation:

    New:

        mmj2\doc\RegressionTestResults.txt
        mmj2\doc\RegressionTestResultsForm.txt

    Changed:

        CHGLOG.TXT
        doc\FinalizeReleaseTodos.txt
        INSTALL.html
        mmj2.html
        README.html
        doc\RunningTheMMJ2TestSuite.html


Source Code:

    New:

        N/A

    Changed:

        src\mmj\lang\LangConstants.java
        src\mmj\pa\PaConstants.java
        src\mmj\verify\EarleyParser.java

Data:

    New:

        mmj2\data\mm\RegressionTest1set.mm

    Changed:

        mmj2\data\mm\UTGR1c02.mm
        mmj2\mmj2jar\AnnotatedRunParms.txt
        mmj2\mmj2jar\RunParms.txt
        mmj2\mmj2jar\RunParmsPATutorial.txt
        mmj2\mmj2jar\RunParmsPeanoInfix.txt

Object Code:

    Changed:

        mmj2jar\mmj2.jar

Other:

    New:

        N/A

    Changed:

        mmj2\mmj2jar\mmj2.bat



==================================================================
1-Aug-2008:

    CHANGES:

    This is a significant release.

    1. The "mmj2 Service" feature adds a new "svc" package to
       mmj2 and provides a foundation for other, non-mmj2
       code to access Metamath data and mmj2 facilities. The
       primary use envisioned is extracting Metamath data,
       as the mmj2 Service feature provides easy access to
       the critical ingredient: formula parse trees!

       Access to mmj2 facilities is made available for "caller"
       and "callee" programs. In both scenarios the BatchMMJ2
       program is used to initialize mmj2 with a loaded .mm
       file which is validated, parsed, etc. Callers actually
       call BatchMMJ2 passing a "SvcCallback" object which is called
       by mmj2 once initialization is complete (when the "SvcCall"
       RunParm is processed.) "Callee" programs simply write
       a class which implements the SvcCallback interface -- just
       as "caller" programs do -- but instead of directly calling
       BatchMMJ2, the user specifies the name of their SvcCallback-
       implementing class via a "SvcCallback" RunParm.

       Whether accessing mmj2 as a "caller" or "callee", complete
       access to mmj2's main facilities is provided in the
       SvcCallback.go interface method. The "go()" method is passed
       references to the biggie mmj2 objects, including
       ProofAsst, Grammar, VerifyProofs, etc.

       Within the SvcCallback.go() method the user-code can
       execute calls to mmj2 methods but must single-thread
       the accesses as mmj2 is not, in general, written for
       total multi-threaded access throughout (some code
       could be multi-threaded but not all.)

       When finished accessing the mmj2 Services, the user-code
       simply needs to execute a "return" from the
       SvcCallback.go() method.

       New RunParms added to mmj2 for use with BatchMMJ2
       (see mmj.util.SvcBoss) are SvcFolder, SvcCallbackClass,
       SvcArg, and SvcCall. The SrvArg RunParm provides a
       way for the user-code to obtain Key-Value parameter
       pairs via the input RunParms file; they are loaded by
       BatchMMJ2 (with minimal validation) into a HashMap
       and passed via the SvcCallback.go() method. More
       information about these new RunParms is provided in
       the mmj2jar\AnnotatedRunParms.txt documentation file.


    2. Modified function of the LoadComments RunParm to now
       pick up the descriptive comment immediately preceding
       axioms (including syntax). Previously, only theorem
       ($p) statement descriptions were picked up. (Small
       changes to Statementizer.java and Systemizer.java :-)


    3. Moved ProvableLogicStmtType and LogicStmtType RunParm
       processing to LogicalSystemBoss from GrammarBoss.

       These RunParms must be input prior to the LoadFile
       RunParm (normally the default settings are used so
       don't worry about this unless you are authoring an
       unorthodox new logic system).

       Also note that "LoadFile" does an implicit
       "Clear" of old RunParms from other facilities such
       as the Grammar, so it is generally necessary to
       re-input RunParms which override defaults prior
       to a 2nd LoadFile command (multiple LoadFile commands
       are rare -- but two in a row can be used to load
       two files together.)


    4. Added BookManager.java, Chapter.java and Section.java
       to mmj.lang. These classes provide a way to group
       Metamath statements and to store descriptive titles
       with their associated Metamath objects (MObj's).

       Each input MObj is assigned to a Section and is given
       a "sectionMObjNbr" ranging for 1 thru 'm' within the
       Section.

       Sections are assigned Section Numbers ranging from 1 thru 'n'
       across the entire input Metamath .mm file. Each Section
       is assigned to a Chapter.

       Chapters are assigned Chapter Numbers ranging from 1 thru 'p'
       across the entire input Metamath .mm file.

       A new optional RunParm, "BookManagerEnabled" ("yes" or "no")
       was added. The default is "no" because BookManager
       provides no benefit at this time for mmj2 Proof Assistant
       users and in the (perhaps) rare situation wherein a new
       theorem is loaded via the new Theorem Loader feature and
       then an existing theorem's proof is modified to use the
       new theorem, the logical sequence of objects within the
       BookManager Section becomes invalid (a forward reference
       in the existing theorem's proof.) To resolve the forward
       reference(s), a resequencing of the objects within the
       Section(s) is required -- which would be a wasteful use
       of resources for mmj2 Proof Assistant users who have no
       interest in BookManager data. BookManager does use a small
       amount of RAM and CPU time and it can be enabled if the user
       desires. (data extracts via the mmj2 Service feature will
       likely be the main users of BookManager data.)

       Considerable additional information about BookManager,
       Chapters and Sections is provided in BookManager.java's
       JavaDoc (Java comments in the source code.)


    5. Added SeqAssigner.java for assigning sequence numbers to
       Metamath objects (MObj's) as they are loaded and inserted
       in the mmj2 Logical System. Sequence numbers are assigned
       sequentially and provide the basis for the mechanism
       which ensures that cyclic or forward references by
       Metamath objects are rejected (as invalid).

       The motivation for this new feature is assignment of sequence
       numbers for theorems inserted by the new Theorem Loader
       enhancement. Previously all Metamath objects were appended
       to the "end" of the Logical System and sequence numbers
       were assigned from 10 by 10 up to the maximum of 2**31 - 1.

       The Theorem Loader aims to "insert" theorems and logical
       hypotheses into the sequence number "gaps" left over from
       the initial Metamath .mm file load(s) (RunParm "LoadFile").
       The Theorem Loader determines the Metamath object
       dependencies of objects to be inserted and instructs
       SeqAssigner to assign in the gap after the referenced
       object with the highest sequence number. The SeqAssigner
       determines whether or not the "gap" is full and
       assigns the appropriate sequence number for each new
       object. A full gap results in an "append"ed sequence
       number, which may or may not be suitable -- if a new
       theorem is referred to by an existing theorem, then
       appending the new theorem is not acceptable (which
       results in an error and backout of all changes prior
       to detection of the error.)

       Associated with SeqAssigner.java is a new RunParm,

            SeqAssignerIntervalSize,9999

       The default sequence number interval is 1000, thus
       allowing for 999 inserts into every gap. It also
       provides the capability to load at least 1 million
       Metamath objects (perhaps more) into the mmj2 Logical
       System. (An interval size of 100 would be suitable for
       almost every purpose -- the exception being automated
       updates from an external system via the new "mmj2 Service"
       feature.


    6. Added "Theorem Loader". The main function of Theorem
       Loader is to enable a user of the mmj2 Proof Assistant GUI
       to store a newly completed proof or theorem into the
       Logical System in memory.

       Theorem Loader does not update the input Metamath .mm
       file(s). However, it stores new proofs and theorems
       in .mm format in the user-designated "MMT Folder", which
       thus simplifies manual update of a Metamath .mm file.

       Files are stored in the MMT Folder by the Theorem Loader
       with file name = theorem label + file type ".mmt" (i.e.
       "syl.mmt"). Theorems can also be manually edited into
       ".mmt" files and stored in the MMT Folder; these theorems
       are allowed to contain incomplete (containing a "?"
       label) or invalid proofs (the mmj2 Proof Assistant GUI
       will not store incomplete or invalid proofs in the
       MMT Folder (by design.)

       The "MMT Folder" is used in another valuable Theorem
       Loader function. At mmj2 start-up the contents of the
       MMT Folder can be automatically loaded after the main
       input Metamath .mm file is loaded. This is accomplished
       by inserting a "*LoadTheoremsFromMMTFolder,*" RunParm
       in the start-up RunParms.txt file used by the mmj2.bat
       job. Thus, the MMT Folder provides a "sandbox"ing
       capability and may be used as a repository for
       theorems and proofs developed over many mmj2 sessions.

       All of the Theorem Loader RunParms are available as
       functions of the mmj2 Proof Assistant GUI "TL" menu.
       Thus, it is not necessary to always load the entire
       contents of the MMT Folder(s) at start-up -- this
       can be requested from the GUI, if desired (for this
       reason "Verify All Proofs" was added to the TL menu.)

       Additional documentation about the Theorem Loader is
       contained in

            doc\TheoremLoaderOverview.html

       and

            mmj2jar\AnnotatedRunParms.txt

       as well as the Proof Assistant GUI "Help" screen.

       Examples of all new RunParms, with their default settings
       are provided in the start-up RunParms file,

            mmj2jar\RunParms.txt.


    7. Miscellaneous Bug Fixes:

        a) Modified the Proof Assistant to not redundantly
           generate sets of $d statements each time the Proof
           Worksheet is unified. Now the code looks at each
           individual generated $d statement to see if it is
           redundant with any other single $d statement already
           contained in the proof worksheet (this is not a
           theoretically complete fix for eliminating all
           redundancy across $d statements.)

        b) Fixed (theoretical) numerical overflow bug in binary
           search in mmj.pa.StepSelectorSearch.java by changing

                mid = (low + high) / 2;
           to
                mid = low + ((high - low) / 2);

        c) Fixed a bug in the Proof Assistant  which allowed a
           defined but "inactive" variable to be used in a new
           $d statement on the Proof Assistant GUI screen. To
           verify this, enter the GUI. It pops up a hypothetical
           new theorem, "syllogism" with a blank "LOC_AFTER"
           meaning that the theorem is logically located at the
           end of the Logical System. Add a line, "$d et ph" and
           press Ctrl-U. No error message is registered, but
           adding a proof step such as "99:? |- ( ph ? et )" does
           trigger an error message.

        d) To prevent future problems, most RunParm options which
           typically follow the "LoadFile" RunParm are reset (nulled)
           when the LoadFile is executed. This is because the
           subsequent processing facilities have numerous
           interdependencies, some of which involve the data which
           is loaded by LoadFile. In effect, LoadFile is treated
           the same way that "Clear" is handled for the subsequent
           processing facilities. As a practical matter this means
           that, should anyone even want to process multiple
           Metamath .mm files independently, they will need to
           re-enter the RunParms used for the first Metamath file
           after doing a LoadFile for the second.

        e) eliminated stmtHasError() from ProofWorksheet statement
           classes.



Documentation:

    New:

        doc\TheoremLoaderOverview.dia
        doc\TheoremLoaderOverview.html
        doc\TheoremLoaderOverview.jpg
        doc\mmj2Service\TjavacTCompilePaths.txt
        doc\mmj2Service\TSvcCallbackCallee.bat
        doc\mmj2Service\TSvcCallbackCallee.class
        doc\mmj2Service\TSvcCallbackCallee.java
        doc\mmj2Service\TSvcCallbackCalleeClasses.txt
        doc\mmj2Service\TSvcCallbackCalleeRunParms.txt
        doc\mmj2Service\TSvcCallbackCaller.bat
        doc\mmj2Service\TSvcCallbackCaller.class
        doc\mmj2Service\TSvcCallbackCaller.java
        doc\mmj2Service\TSvcCallbackCallerClasses.txt
        doc\mmj2Service\TSvcCallbackCallerRunParms.txt


    Changed:

        CHGLOG.TXT
        doc\FinalizeReleaseTodos.txt
        INSTALL.html
        doc\MMJ2DirectoryStructure.txt
        mmj2.html
        mmj2jar\AnnotatedRunParms.txt
        mmj2jar\PATutorial\Page103.mmp
        README.html
        doc\RunningTheMMJ2TestSuite.html


Source Code:

    New:

        src\mmj\lang\BookManager.java
        src\mmj\lang\Chapter.java
        src\mmj\lang\Section.java
        src\mmj\lang\SeqAssigner.java
        src\mmj\lang\TheoremLoaderException.java

        src\mmj\svc\SvcCallback.java

        src\mmj\tl\MMTFileFilter.java
        src\mmj\tl\MMTFolder.java
        src\mmj\tl\MMTTheoremExportFormatter.java
        src\mmj\tl\MMTTheoremFile.java
        src\mmj\tl\MMTTheoremSet.java
        src\mmj\tl\StoreInLogSysAndMMTFolderTLRequest.java
        src\mmj\tl\StoreInMMTFolderTLRequest.java
        src\mmj\tl\TLRequest.java
        src\mmj\tl\TheoremLoader.java
        src\mmj\tl\TheoremLoaderCommitListener.java
        src\mmj\tl\TheoremStmtGroup.java
        src\mmj\tl\TlConstants.java
        src\mmj\tl\TlPreferences.java

        src\mmj\util\MergeSortedArrayLists.java
        src\mmj\util\SvcBoss.java
        src\mmj\util\TheoremLoaderBoss.java


    Changed:

        src\mmj\lang\Assrt.java
        src\mmj\lang\DjVars.java
        src\mmj\lang\Formula.java
        src\mmj\lang\LangConstants.java
        src\mmj\lang\LogicalSystem.java
        src\mmj\lang\MObj.java
        src\mmj\lang\MandFrame.java
        src\mmj\lang\SystemLoader.java
        src\mmj\lang\Theorem.java
        src\mmj\lang\Var.java

        src\mmj\mmio\MMIOConstants.java
        src\mmj\mmio\Statementizer.java
        src\mmj\mmio\Tokenizer.java
        src\mmj\mmio\Systemizer.java

        src\mmj\pa\CommentStmt.java
        src\mmj\pa\DerivationStep.java
        src\mmj\pa\DistinctVariablesStmt.java
        src\mmj\pa\FooterStmt.java
        src\mmj\pa\GeneratedProofStmt.java
        src\mmj\pa\HeaderStmt.java
        src\mmj\pa\HypothesisStep.java
        src\mmj\pa\PaConstants.java
        src\mmj\pa\ProofAsst.java
        src\mmj\pa\ProofAsstGUI.java
        src\mmj\pa\ProofAsstPreferences.java
        src\mmj\pa\ProofStepStmt.java
        src\mmj\pa\ProofUnifier.java
        src\mmj\pa\ProofWorkStmt.java
        src\mmj\pa\ProofWorksheet.java
        src\mmj\pa\StepSelectorSearch.java

        src\mmj\util\BatchFramework.java
        src\mmj\util\BatchMMJ2.java
        src\mmj\util\Boss.java
        src\mmj\util\Dump.java
        src\mmj\util\GrammarBoss.java
        src\mmj\util\LogicalSystemBoss.java
        src\mmj\util\OutputBoss.java
        src\mmj\util\ProofAsstBoss.java
        src\mmj\util\UtilConstants.java
        src\mmj\util\VerifyProofBoss.java

Data:

    New:

        data\mm\UT9001.mm
        data\mm\UT9002.mm
        data\mm\UT9003.mm

        data\mmt\testin\t101\a1d.mmt
        data\mmt\testin\t101\syllogism4.mmt
        data\mmt\testin\t101\syllogism3.mmt
        data\mmt\testin\t102\imim1i.mmt
        data\mmt\testin\t102\imim1.mmt
        data\mmt\testin\t102\imim2.mmt
        data\mmt\testin\t102\a2d.mmt
        data\mmt\testin\t102\a1d.mmt
        data\mmt\testin\t102\com12.mmt
        data\mmt\testin\t102\syllogism3.mmt
        data\mmt\testin\t102\syllogism.mmt
        data\mmt\testin\t102\lockOnA.mmt
        data\mmt\testin\t102\lockOnB.mmt
        data\mmt\testin\t103\a1d.mmt
        data\mmt\testin\t103\com12.mmt
        data\mmt\testin\t103\syllogism3.mmt
        data\mmt\testin\t103\syllogism.mmt
        data\mmt\testin\t103\imim1i.mmt
        data\mmt\testin\t103\imim1.mmt
        data\mmt\testin\t103\imim2.mmt
        data\mmt\testin\t103\a2d.mmt
        data\mmt\testin\t191\csbima12g.mmt

        data\runparm\windows\UT9001.txt
        data\runparm\windows\UT9002.txt
        data\runparm\windows\UT9003.txt
        data\runparm\windows\UT10001.txt
        data\runparm\windows\UT10002.txt
        data\runparm\windows\UT10003.txt
        data\runparm\windows\UT10021.txt
        data\runparm\windows\UT10022.txt
        data\runparm\windows\UT10023.txt
        data\runparm\windows\UT10031.txt
        data\runparm\windows\UT10032.txt
        data\runparm\windows\UT10033.txt
        data\runparm\windows\UT10041.txt
        data\runparm\windows\UT10042.txt
        data\runparm\windows\UT10043.txt
        data\runparm\windows\UT10051.txt
        data\runparm\windows\UT10052.txt
        data\runparm\windows\UT10053.txt
        data\runparm\windows\UT19100.txt

    Changed:

        data\runparm\windows\Sample002.txt
        data\runparm\windows\UT2PA001.txt
        mmj2jar\RunParms.txt
        mmj2jar\RunParmsPATutorial.txt


Object Code:

    Changed:

        mmj2jar\mmj2.jar

Other:

    New:

        compile\mmj\svc\svcClasses.txt
        compile\mmj\tl\tlClasses.txt
        test\windows\RunUnitTest8.bat
        test\windows\RunUT8.bat
        test\windows\RunUnitTest9.bat
        test\windows\RunUT9.bat
        test\windows\RunUnitTest10.bat
        test\windows\RunUT10.bat

    Changed:

        compile\mmj\lang\langClasses.txt
        compile\mmj\util\utilClasses.txt
        compile\windows\CompMMJ.bat
        compile\windows\EraseMMJObjCode.bat
        compile\windows\mkjarargs.txt
        doc\windows\DocPackages.txt


==================================================================
1-Mar-2008:

    CHANGES:

    This is a minor release but with super enhancements!

    1. Add "Step Selector Search" feature to replace
       "Unify + Get Hints" and "alternate unification" messages.

       The Step Selector Search is another step-specific function
       and can be initiated with a right(alt) mouse button when
       the mouse cursor is positioned on top of a Derivation
       proof step. It is also available on the Unify menu, in which
       case the targeted Derivation step is designated by the
       input (keyboard) cursor location. Ctrl-8 is also available,
       and in fact, this is the recommended way to initiate
       Step Selector Search.

       The Step Selector Search performs a search for assertions
       which can be unified with the specified Derivation step and
       its hypotheses. It works even if Work Variables are present
       and if the Derivation Step has incomplete hypotheses (i.e.
       a "?" in the Hyp field.) Note: the standard Unification
       Search does not work for proof steps containing Work Variables
       in their formulas (or their hypotheses' formulas.)

       The results of the Step Selector Search are displayed on
       the Step Selector Dialog screen, which is a non-modal
       dialog, meaning that it hangs around but does not prevent
       other windows from being used. Selecting an item from
       the Step Selector Dialog can be done using a double-click
       or by moving the cursor to the desired item and then
       clicking the dialog button labelled "Apply Selection To Step
       And Unify Proof". Note: an assertion with hypotheses is
       displayed on multiple lines on the Step Selector Dialog;
       selecting any of the lines associated with an assertion
       is sufficient to select the assertion itself (they assertion
       conclusion and hypothesis formulas are broken out into
       multiple lines for readability but point to the same
       Assertion.)

       When an item is selected on the Step Selector Dialog the
       associated assertion's label is "pasted" into the Ref field
       of the Derivation Step for which the Step Selector Search
       was run -- then Unification is performed in the usual
       manner. If the selected item proves to be unsuitable --
       perhaps because of a Distinct Variables error (not checked
       in Step Selector Search), press Ctrl-Z (Edit Undo) twice
       to restore the Proof Worksheet to the pre-selection
       condition.


    2. Add "Unify + Erase And Rederive Formulas" to the Unify menu.
       This feature is handy (primarily for "advanced" users) in
       situations where the Step/Hyp/Ref fields are correct but
       the associated formulas contain inconsistent substitutions,
       normally of the Work Variable or "optional" variable
       varieties. This feature is treated as a "preprocessing"
       editing function which, prior to unification, erases the
       formulas from Derivation steps, except the 'qed' step
       and Derivation Steps which have a blank Ref field. Then
       Unification is performed, which automatically re-derives
       the missing formulas. As usual, if the results are
       unsatisfactory, press Ctrl-Z (Edit-Undo) twice to restore
       the Proof Worksheet to its prior state.


    3. Several data items involved in unification are pre-computed
       to speed up the unification loops and to avoid "dirty buffers"
       (the latter being intended to improve operation on multi-core
       processors in the future -- specifically, when new features
       are added which run simultaneously in independent threads.)
       These data items include sorting the logical hypotheses for
       each assertion, computing the Max Depth of each parse tree,
       and computing "fast fail" signatures for assertions (these
       are partial keys built from parse trees of assertions.)

       The perceived net effect now is primarily an increase in start-up
       elapsed time by about 10%, plus some small additional memory
       utilization. However, the Step Selector Search feature is
       really fast :-)


    4. The loop algorithm in the main unification search process was
       tweaked to be less inefficient.

Documentation:

    New:
x       doc\BottomUpProving-ByNormMegill.html
x       doc\StepSelectorSearch.html
x       doc\UnifyEraseAndRederiveFormulasFeature.html
x       mmj2jar\PATutorial\Page408.mmp
x       mmj2jar\PATutorial\Page409.mmp
x       mmj2jar\PATutorial\Page410.mmp
x       mmj2jar\PATutorial\Page411.mmp
x       mmj2jar\PATutorial\Page412.mmp

    Changed:

x       CHGLOG.TXT
x       doc\FinalizeReleaseTodos.txt
x       doc\ProofAssistantGUIDeriveFeature.html
x       doc\ProofAssistantGUIDetailedInfo.html
x       doc\ProofAssistantGUIQuickHOWTO.html
x       doc\RunningTheMMJ2TestSuite.html
x       INSTALL.html
?       mmj2.html
?       mmj2jar\AnnotatedRunParms.txt
        mmj2jar\PATutorial\Page304.mmp
        mmj2jar\PATutorial\Page404.mmp
        mmj2jar\PATutorial\Page407.mmp
x       README.html


Source Code:

    New:

        src\mmj\pa\EraseWffsPreprocessRequest.java
        src\mmj\pa\PreprocessRequest.java
        src\mmj\pa\StepRequest.java
        src\mmj\pa\StepSelectorDialog.java
        src\mmj\pa\StepSelectorItem.java
        src\mmj\pa\StepSelectorResults.java
        src\mmj\pa\StepSelectorSearch.java
        src\mmj\pa\StepSelectorStore.java

    Changed:

        src\mmj\lang\Assrt.java
        src\mmj\lang\ParseNode.java
        src\mmj\lang\ParseTree.java

        src\mmj\pa\DerivationStep.java
        src\mmj\pa\PaConstants.java
        src\mmj\pa\ProofAsst.java
        src\mmj\pa\ProofAsstGUI.java
        src\mmj\pa\ProofAsstPreferences.java
        src\mmj\pa\ProofUnifier.java
        src\mmj\pa\ProofWorksheet.java
        src\mmj\pa\ProofWorksheetParser.java
        src\mmj\pa\StepUnifier.java

        src\mmj\util\ProofAsstBoss.java
        src\mmj\util\UtilConstants.java

        src\mmj\verify\Grammar.java


Data:

    New:

        data\runparm\windows\UT7001.txt
        data\mmp\tests\UT7000.mmp
        data\mmp\tests\UT7001.mmp
        data\mmp\tests\UT7002.mmp
        data\mmp\tests\UT7003.mmp
        data\mmp\tests\UT7004.mmp
        data\mmp\tests\UT7101.mmp

    Changed:

?       mmj2jar\RunParms.txt
?       mmj2jar\RunParmsPATutorial.txt


Object Code:

    Changed:

?       mmj2jar\mmj2.jar

Other:

    New:

        test\windows\RunUT7.bat
        test\windows\RunUnitTest7.bat

    Changed:


==================================================================

1-Feb-2008:

    CHANGES:

    This is a minor upgrade to mmj2 to satisfy user requests that
    didn't quite make it into Release20071101.

    1. Provide "First", "Last" or "AsIs" positioning of the
       cursor when there are no errors. Release20071101 provided
       "Last" positioning, which puts the cursor at the /last/
       incomplete proof step's Ref field if there are no errors,
       (and the 'qed' step's Ref if there are no incomplete
       proof steps.) "First" positions to the first incomplete
       proof step, if no errors, while "AsIs" does not move the
       cursor from the proof step (but does position it to the
       Ref field.)

       This feature is controlled by a RunParm:

           ProofAsstIncompleteStepCursor,Last

       (See AnnotatedRunParms.txt for more details.)

       An Edit Menu option, "Set Incomplete Step Cursor" is
       also provided.


    2. Enable user to disable automatic (TMFF) reformatting of
       formulas containing work variables which are resolved
       during Unification (this is, in fact, the only time
       automatic reformatting of formulas is performed by mmj2
       in an "in progress" proof -- the program /respects/ the
       user's formatting in all other instances unless
       reformatting is specifically requested.)

       This feature is controlled by a RunParm:

           ProofAsstAutoReformat,no

       (See AnnotatedRunParms.txt for more details.)


    3. Provide single proof step reformatting via two new
       (alt) right-mouse button "pop-up" menu options:

           ReformatStep

           ReformatStep:Swap Alt

       These operate identically to the regular Edit Menu
       options, "Reformat Proof" and "Reformat Proof:Swap Alt".

       To make these new step-level reformatting options work
       in an acceptable manner, the functioning of Edit Menu
       options "Set Format Nbr" and "Set Indent" were modified
       to /not/ automatically reformat the entire proof after
       a change in parameter setting. This may result in
       some perplexities when the new step reformatting options
       are used, so a discussion is now required...

       The Proof Assistant has one set of memory registers
       to keep track of the Current Format Number, the
       Current Indent Amount, and a "toggle switch" recording
       whether or not the /alternate/ format is now in use.
       Previously, this was not confusing. But now when the
       "Reformat Step:Swap Alt" option is invoked the entire
       proof format is considered to be in /alternate/ format
       mode -- the program does NOT keep track of the format
       number and indent amount in use for each proof step!

       The /least/ confusing method for using "Reformat Step:Swap Alt"
       is to use it (toggle it) twice on a single proof step,
       thus switching the format options to the /alternate/
       settings, and then back again.

       Note also: in my environment, at least, it is necessary
                  to first left-mouse click a proof step to
                  change the cursor position...and then use the
                  right-mouse click pop-up menu. Java does not
                  re-establish cursor position at the location
                  of the mouse when the right-mouse button is
                  clicked!


    4. Two new Ctrl key options are provided for fast font
       size changes. "Ctrl+" increases font size and "Ctrl-"
       decreases font size. For "technical reasons" these
       are shown as "Ctrl-Equals" and "Ctrl-Minus" on the
       Edit Menu.

       Note: This change is compatible with the way the Mozilla
       browser works, and that works just fine...


    5. Error messages are now displayed before "Info" messages
       on the Proof Assistant GUI screen. Previously info
       messages appeared first, which resulted in some
       amount of dissatisfaction -- which need not be discussed
       here, but....the goal is that if there are errors in a Proof
       Worksheet, the (output) cursor is positioned to the
       first error on the screen, and the first error message
       shown corresponds to the cursor position...therefore
       it is preferable that the info messages not get in the
       way if there are errors.


    6. A new RunParm generating an info message about the
       output cursor position was added. This feature is
       intended to provide instrumentation output for use
       in regression testing, and is probably of no use to
       anyone else:

           ProofAsstOutputCursorInstrumentation,no

       (See AnnotatedRunParms.txt for more details.)



    DEFERRED CHANGES:

    1. Technical (transparent to users): Use Java "Generics"
       language feature. Contribution from Dan Getz. This is
       a Java JDK 1.5 (AKA "5.0") language feature.

       a) Use <typed> Collections
       b) Eliminate as many (newly) redundant typecasts as
          possible
       c) Note: don't automatically change all "for loop" statements
                to take advantage of the newly "generified"
                code when iterating over "Iterable" objects.


Documentation:

    New:

    Changed:

        CHGLOG.TXT
        doc\FinalizeReleaseTodos.txt
        doc\PAUserGuide\cmdwindow.html
        doc\PAUserGuide\Start.html
        doc\PAUserGuide\mmj2ProofAsst.html
        doc\ProofAsstGUICursorHandling.html
        doc\RunningTheMMJ2TestSuite.html
        INSTALL.html
        mmj2.html
        mmj2jar\AnnotatedRunParms.txt
        README.html

    Deleted:

        doc\OldProofUnifierComments.java
        doc\READMEPATCH20060725.TXT

Source Code:

    Changed:

        src\mmj\lang\Formula.java
        src\mmj\lang\LangConstants.java
        src\mmj\lang\ParseNode.java
        src\mmj\pa\CommentStmt.java
        src\mmj\pa\DerivationStep.java
        src\mmj\pa\DistinctVariablesStmt.java
        src\mmj\pa\FooterStmt.java
        src\mmj\pa\GeneratedProofStmt.java
        src\mmj\pa\HeaderStmt.java
        src\mmj\pa\PaConstants.java
        src\mmj\pa\ProofAsst.java
        src\mmj\pa\ProofAsstCursor.java
        src\mmj\pa\ProofAsstGUI.java
        src\mmj\pa\ProofAsstPreferences.java
        src\mmj\pa\ProofStepStmt.java
        src\mmj\pa\ProofUnifier.java
        src\mmj\pa\ProofWorkStmt.java
        src\mmj\pa\ProofWorksheet.java
        src\mmj\pa\ProofWorksheetParser.java
        src\mmj\tmff\TMFFPreferences.java
        src\mmj\util\Boss.java
        src\mmj\util\ProofAsstBoss.java
        src\mmj\util\UtilConstants.java


Data:

    New:

        data\runparm\windows\UT6001.txt
        data\runparm\windows\VT2ePA002.txt
        data\mmp\tests\UT6001.mmp
        data\mmp\tests\UT6002.mmp
        data\mmp\tests\UT6003.mmp


    Changed:

        data\runparm\windows\UT4001.txt
        mmj2jar\LicenseEnclosure.java
        mmj2jar\RunParms.txt
        mmj2jar\RunParmsPATutorial.txt


Object Code:

    Changed:

        mmj2jar\mmj2.jar

Other:

    New:

        test\windows\RunUT6.bat
        test\windows\RunUnitTest6.bat
        test\windows\RunVT2e.bat
        test\windows\RunVolumeTest2e.bat

    Changed:

        test\windows\RunUnitTest4.bat

==================================================================
1-Nov-2007:

    CHANGES: (note: #1 -> #5 apply to the ProofAsstGUI)

    1. If no errors position cursor to *last* incomplete proof step,
       and instead of always positioning cursor to column 1 of the
       incomplete step, position it to the start of the Ref subfield.

    2. Support indenting of proof levels as follows:

       a) Add new RunParms "TMFFUseIndent" and
          new Edit Menu item, "Set Indent Amount".
          The default is 0, meaning zero number of columns
          indentation for each level down in the proof tree.

       b) Add new RunParm "TMFFAltFormat" and "TMFFAltIndent"
          providing the preferred "alternate" Format Number
          and Level Indent Amount. The defaults are "7" and
          "1", respectively meaning "Flat" format and indent
          one column per level.

          And add new Edit Menu item, "Reformat Proof: Alt Swap" --
          with special "Alt" and "Ctrl" key binding to the
          letter "o", so that Alt-E-O and Ctrl-O will switch
          to the input RunParm TMFFAltFormat and TMFFAltIndent
          parameters and then back again to the previous
          settings if requested a second time.

       NOTE: These features generalize upon the request for a
             single "Flat/Indented" formatting option. The "Flat"
             format displays each proof step on one line, and
             indentation by proof level is expected to be very
             useful with the "Flat" Format (perhaps not so much
             with the other formats.)

       NOTE: There will be no Edit Menu option(s) corresponding
             to the new "TMFFAltFormat" and "TMFFAltIndent" RunParms.
             The default value of "7,1" is expected to be satisfactory
             and the need for a GUI setting is ... not so much...

       NOTE: The 'qed' step is considered Level 0, and will
             have zero indentation -- as will "island" proof
             steps that are not connected as hypotheses to
             any other proof steps. If a proof step is used
             as an hypothesis more than once, the first
             instance of its usage -- counting from the 'qed'
             step upwards in the proof -- is treated as *the*
             indicative level. Thus a step used as an hypothesis
             by the 'qed' step has Level 1 and indented by
             1 times the Indent Amount, and a step used by
             it as an hypothesis is at Level 2, and so on.

    3. Add new "Local Ref" escape character, "#". May be used
       as the prefix to a Derivation Step Ref field which contains
       either a Step Number or the .mm label of one of the
       Logical (aka "Essential") hypotheses of the theorem being
       proved. When Unification (Ctrl-U, etc.) is performed, during
       the "finale" of the initial LoadWorksheet processing (before
       unification search, Derive processing, etc.), all Hyp
       references pointing to the step containing the "#" are
       changed to point to the Local Ref step.

       Here is an example with a detailed explanation:

            -----

            For example, after entering the first ax-mp then Ctrl-U
            for syl, we see:

               h1::syl.1          |- ( ph -> ps )
               h2::syl.2          |- ( ps -> ch )
               1002:?:            |- &W1
               2002:?:            |- ( &W1 -> ( ph -> ch ) )
               qed:1002,2002:ax-mp     |- ( ph -> ch )

            Then, the user recognizes that 1002 is really #1, he
            types "#1" or "#syl.1" after the "1002:?:" as
            follows, and presses Ctrl-U:

               1002:?:#syl.1      |- &W1

            or

               1002:?:#1          |- &W1


            The program performs the requested Local Ref *text editing*
            operation during the "finale" of the LoadWorksheet
            validation process (prior to unification). If there
            are no errors with the request so far, it makes the
            *text editing* updates, so that after pressing Ctrl-U,
            we see:

               h1::syl.1          |- ( ph -> ps )
               h2::syl.2          |- ( ps -> ch )
               2002:?:            |- ( ( ph -> ps ) -> ( ph -> ch ) )
               qed:1,2002:ax-mp     |- ( ph -> ch )


            NOTE 1: In the event of the Local Ref was input
            incorrectly, or if there is a subsequent error, say
            during Unification, the user then has the option of
            either manually correcting the proof *or* using
            Edit/Undo to restore the Proof Worksheet to the
            pre-*text editing* state. And, as is the case today,
            if mmj2 detects an error during the Load Worksheet
            validation phase, the input Proof Worksheet is
            redisplayed without any of the program's updates
            to the data (processing halts immediately during
            Load Worksheet if an error is found and no changes
            are made.)

       Note: A tutorial page has been added demonstrating the
             "Local Ref" feature. To use it, run the
             mmj2PaTutorial.bat batch command while in the
             mmj2jar directory. Then in the Proof Assistant GUI,
             use the File/Open Proof File menu item to open
             file "mmj2\mmj2jar\PATutorial\PageLocalRef.mmp".


    4. Add error messages area to main proof window frame.

       This change involves creating a "JSplitPane" in the
       ProofAsstGUI main window frame. The Proof Text area
       can be at the top, with the error messages area at
       the bottom, or vice-versa, as specified by this new
       RunParm (default value is "Y"):

            ProofAsstTextAtTop,yes

       In addition, the number of text rows for both the Proof
       Text area and the error messages text area can be
       specified via RunParm. These merely provide information
       to the system about how big to make the windows -- they
       do not limit the amount of output (and scroll bars
       appear as needed anyway.) The default settings are shown
       below:

            ProofAsstTextRows,21
            ProofAsstErrorMessageRows,4
            ProofAsstErrorMessageColumns,80

       Finally, please note that the existing Request Messages
       Window still exists and is populated with all of the
       messages displayed in the new error message text area
       on the ProofAsstGUI window. However, it is displayed
       *behind* the ProofAsstGUI window and is reachable at
       any time by hitting Alt-Tab (press Alt-Tab again to
       return to the ProofAsstGUI window.) While this may seem
       redundant, and unorthodox, at best, the idea is that
       in some cases multiple messages of significant size may
       be produced, and in those situations it will be easier
       to view them in their entirety, in full screen mode (also
       it is much easier to add code than to remove code :-)


    5. Eliminate the "dummy" derivation step containing
       a "?" formula when File/New Proof or File/New Next Proof
       is requested for a theorem that already exists in
       the input .mm file. Instead, just output the
       theorem's hypotheses and 'qed' step, and position
       the cursor to the 'qed' step's Ref field.

    6. Generates "info" message
       "I-PA-0119 Theorem xyz RPN-format Metamath proof generated!"
       when Ctrl-U (unification) is successful and the RPN-format
       proof is generated. Previously, no message was output. Also,
       positions to the last remaining (if any) incomplete proof
       step -- or the 'qed' step if there are no incomplete proof
       steps and the cursor has not already been set.

       This modification allows a user to use a "dummy" 'qed'
       step and incrementally build a proof, with cursor
       positioning somewhere reasonable (a "dummy" incomplete
       proof step could be manually input for this purpose.)
       The new info message is intended to provide confirmation
       of the success of unification -- which was previously
       provided by positioning the cursor at the end of the
       generated RPN-format proof.

    7. Miscellany:

        doc\ProofAssistantGUIDeriveFeature.html
            - In the dfuz example, "eqri" was recently name-changed
              in set.mm to become "eqriv".
            - Also, the &W1 is now named &S1 by mmj2.

        doc\PAUserGuide\mmMetamathFile.html
            - $e and $f swapped

        mmj2jar\AnnotatedRunParms.txt
            - Added documentation for new RunParms:
              * TMFFUseIndent
              * TMFFAltFormat
              * TMFFAltIndent

        mmj2jar\PATutorial\Page303.mmp
            - "experiment erase the "a21" in LOC_AFTER" - should be a2i

        mmj2jar\PATutorial\Page402.mmp
            - typo missing " " between "that" and "can".

        mmj2jar\PATutorial\Page403.mmp
            - clarification.

        mmj2jar\RunParms.txt
            - Added new RunParms:
              * TMFFUseIndent
              * TMFFAltFormat
              * TMFFAltIndent

        mmj2jar\RunParmsPATutorial.txt
            - Added new RunParms:
              * TMFFUseIndent
              * TMFFAltFormat
              * TMFFAltIndent


Documentation:

    New:

        mmj2jar\PATutorial\PageLocalRef.mmp

    Renamed:

    Changed:

        CHGLOG.TXT
        doc\FinalizeReleaseTodos.txt
        doc\PAUserGuide\mmMetamathFile.html
        doc\ProofAssistantGUIDeriveFeature.html
        doc\ProofAssistantGUIDetailedInfo.html
        doc\ProofAssistantGUIQuickHOWTO.html
        doc\ProofAsstGUICursorHandling.html
        doc\RunningTheMMJ2TestSuite.html
        INSTALL.html
        mmj2.html
        mmj2jar\AnnotatedRunParms.txt
        mmj2jar\PATutorial\Page102.mmp
        mmj2jar\PATutorial\Page204.mmp
        mmj2jar\PATutorial\Page303.mmp
        mmj2jar\PATutorial\Page401.mmp
        mmj2jar\PATutorial\Page402.mmp
        mmj2jar\PATutorial\Page403.mmp
        mmj2jar\PATutorial\Page404.mmp
        mmj2jar\PATutorial\Page407.mmp
        README.html

    Deleted:
        doc\ProofAssistantHelp.txt
        doc\ProofAssistantHelp.html


Source Code:

    New:

    Changed:

        src\mmj\pa\CommentStmt.java
        src\mmj\pa\DerivationStep.java
        src\mmj\pa\DistinctVariablesStmt.java
        src\mmj\pa\FooterStmt.java
        src\mmj\pa\GeneratedProofStmt.java
        src\mmj\pa\HeaderStmt.java
        src\mmj\pa\HypothesisStep.java
        src\mmj\pa\PaConstants.java
        src\mmj\pa\ProofAsst.java
        src\mmj\pa\ProofAsstCursor.java
        src\mmj\pa\ProofAsstGUI.java
        src\mmj\pa\ProofAsstPreferences.java
        src\mmj\pa\ProofStepStmt.java
        src\mmj\pa\ProofUnifier.java
        src\mmj\pa\ProofWorksheet.java
        src\mmj\pa\ProofWorkStmt.java
        src\mmj\tmff\TMFFConstants.java
        src\mmj\tmff\TMFFPreferences.java
        src\mmj\tmff\TMFFStateParams.java
        src\mmj\util\Boss.java
        src\mmj\util\Dump.java
        src\mmj\util\OutputBoss.java
        src\mmj\util\ProofAsstBoss.java
        src\mmj\util\TMFFBoss.java
        src\mmj\util\UtilConstants.java
        src\mmj\verify\ProofDerivationStepEntry.java
        src\mmj\verify\VerifyProofs.java


Data:

    New:

        data\mmp\tests\UT4701.mmp
        data\mmp\tests\UT4702.mmp

    Changed:

        data\runparm\windows\UT4001.txt
        data\runparm\windows\VT2PA002.txt
        data\runparm\windows\VT2bPA002.txt
        data\runparm\windows\VT2cPA002.txt
        data\runparm\windows\VT2dPA002.txt
        mmj2jar\AnnotatedRunParms.txt
        mmj2jar\RunParms.txt
        mmj2jar\RunParmsPATutorial.txt

Other:

    New:

    Changed:



==================================================================
1-Aug-2007:

New/Changed Features -- Proof Assistant and general mmj2:

    New Features:
    =============

    * The "dummy variables" used in the old Proof Assistant
      which were output as $1, $2, ..., are now programmed
      to behave as real variables with global scope. Their
      names are Type Code dependent, and the default for
      type "wff" is &W1, &W2, ... &W200; "class" Work Variables
      are named &C1, &C2, ...; and "set" Work Variables are
      named &S1, &S2, ... A great deal of documentation about
      Work Variables is available in mmj2\doc\WorkVariables.html.

    * A new unification algorithm is used in the Proof Assistant
      for proof steps involving Work Variables in the step
      formula (conclusion) or hypotheses -- and for proof
      steps on which the "DeriveFormula" and/or "DeriveHypotheses"
      features are invoked. The new algorithm is documented
      in mmj2\doc\StepUnifier.html, and it provides great
      power and convenience! Now when DeriveFormula or
      DeriveHypotheses are invoked, Work Variables are
      output instead of "dummy variables", and these can take
      part in unification across all steps in the proof
      (e.g. if &W1 is used in multiple formulas, simply
      update one of them and unification will resolve
      them all automatically -- in fact, you may not even
      need to manually input an update to &W1 if you specify
      a unifying Ref assertion label!!!)

    * Option "AsciiRetest" ("NoAsciiRetest") added to
      RunParm "ProofAsstBatchTest". Ascii Retest reprocesses
      a completed Proof Worksheet using the output text
      as input. The primary motivation for adding it was
      to eliminate batch testing error messages involving
      "soft" $d errors and dummy variables when the Soft Dj
      Vars Edit option is set to "GenerateReplacements" or
      "GenerateNew".


    Changed Features:
    =================

    * The Request Messages GUI window is not re-built every
      time there is an error message. This allows the user
      to resize and reposition the Proof Assistant GUI and
      Request Messages GUI windows so that both are visible
      on the desktop at the same time (assuming the user doesn't
      close one of them :-) The motivation for this change is
      to eliminate the annoyance to the user of having to Alt-Tab
      back and forth between the two. Experimentation reveals
      that perhaps the best arrangement is to put the Request
      Messages window at the bottom of the screen and to
      reduce its height so that 3 lines of message text are
      visible within it -- the height of Proof Assistant GUI
      is then shrunk by about 7 rows, but the loss is
      acceptable. Users with large screens can especially
      benefit from this enhancement (and note that the RunParm
      "ProofAsstFontSize" can be set to 10 or 12 instead of the
      default, 14, to squeeze more proof lines onto the screen.)

    * The default for the "ProofAsstDjVarsSoftErrors" RunParm
      was changed to "GenerateReplacements" from "Report".
      Option "GenerateReplacements" automatically creates $d
      statements for a completed Proof Worksheet instead of
      error messages if "soft" Dj Var errors are found. This
      option is especially helpful when a proof uses
      dummy/optional variables because the process by which
      mmj2 converts leftover Work Variables into dummy/optional
      variables after successful unification does not, in general,
      use dummy variables that match the $d statements on the
      theorem being proved. Note: changing $d statements on
      a theorem is not problematic in this situation because
      $d's for dummy/optional variables are not inherited by
      subsequent theorems.

    * RunParm "ProofAsstDummyVarPrefix" is ignored (because
      new Work Variable RunParms are used instead.) Remove
      any ProofAsstDummyVarPrefix RunParms in your RunParms.txt
      files -- at your convenience, as the RunParm is being
      deprecated.



Documentation:

    New:

        doc\StepUnifier.html
        doc\WorkVariables.html

    Renamed:


    Changed:

        CHGLOG.TXT
        INSTALL.html
        README.html
        doc\FinalizeReleaseTodos.txt
        doc\ProofAssistantGUIDeriveFeature.html
        doc\ProofAssistantGUIDetailedInfo.html
        doc\ProofAssistantGUIQuickHOWTO.html
        doc\RunningTheMMJ2TestSuite.html
        mmj2jar\AnnotatedRunParms.txt
        mmj2jar\PATutorial\Page405.mmp


Source Code:

    New:

        src\mmj\lang\WorkVar.java
        src\mmj\lang\WorkVarHyp.java
        src\mmj\lang\WorkVarManager.java

        src\mmj\pa\StepUnifier.java
        src\mmj\pa\UnifySubst.java

        src\mmj\util\WorkVarBoss.java


    Changed:

        src\mmj\lang\Cnst.java
        src\mmj\lang\Assrt.java
        src\mmj\lang\Formula.java
        src\mmj\lang\Hyp.java
        src\mmj\lang\LangConstants.java
        src\mmj\lang\LogHyp.java
        src\mmj\lang\ParseNode.java
        src\mmj\lang\Stmt.java
        src\mmj\lang\Var.java
        src\mmj\lang\VarHyp.java

        src\mmj\pa\AuxFrameGUI.java
        src\mmj\pa\DerivationStep.java
        src\mmj\pa\HypothesisStep.java
        src\mmj\pa\PaConstants.java
        src\mmj\pa\ProofAsst.java
        src\mmj\pa\ProofAsstGUI.java
        src\mmj\pa\ProofAsstPreferences.java
        src\mmj\pa\ProofStepStmt.java
        src\mmj\pa\ProofUnifier.java
        src\mmj\pa\ProofWorksheet.java

        src\mmj\mmio\Statementizer.java

        src\mmj\tmff\TMFFAlignColumn.java
        src\mmj\tmff\TMFFTwoColumnAlignment.java

        src\mmj\util\BatchFramework.java
        src\mmj\util\ProofAsstBoss.java
        src\mmj\util\UtilConstants.java

        src\mmj\verify\EarleyParser.java
        src\mmj\verify\Grammar.java
        src\mmj\verify\VerifyProofs.java


Data:

    New:

    Changed:

        compile\mmj\lang\langClasses.txt
        compile\mmj\pa\paClasses.txt
        compile\mmj\util\utilClasses.txt

        data\runparm\windows\Sample003.txt
        data\runparm\windows\Sample002.txt
        data\runparm\windows\Sample001.txt
        data\runparm\windows\VT2bPA002.txt
        data\runparm\windows\VT2cPA002.txt
        data\runparm\windows\VT2PA002.txt
        data\runparm\windows\UT5001.txt
        data\runparm\windows\UT4001.txt
        data\runparm\windows\UT2PA001.txt

        mmj2jar\RunParms.txt
        mmj2jar\RunParmsPATutorial.txt


Other:

    New:

        mmj2jar\CopyMMJ2Jar.bat

    Changed:





==================================================================
1-Jun-2007:

    New/Changed Features -- Proof Assistant and general mmj2:

Changes:
    * New separate "mmj2jar.zip" download provided containing
      bare-minimum of executables plus tutorial and
      AnnotatedRunParms.txt (for reference). The full
      mmj2.zip contains directory mmj2jar as well as
      all documentation, source code, test data, etc.
      Note: the old mmj2\mmj2jar directory was coded
      to run inside the mmj2 directory. Now, it is
      coded to be copied to, say, c:\mmj2jar and
      run independently (changes made to .bat and
      RunParm .txt files specifying file locations).
    * speed up startup by modifying validation
      of font family name on "ProofAsstFontFamily"
      RunParm (actually -- the font name is
      not validated, and if invalid the system
      substitutes a font of its choosing, which
      may be proportional instead of fixed but
      the user can change it in the GUI.)
    * invoke DeriveHyp even if user doesn't
      enter a "?"; if the number of entered
      Hyps is less than the number of logical
      hypotheses used by the entered Ref
      assertion, automatically invoke DeriveHyp
      as if the user entered a "?". Also, if
      a Ref is entered and the correct number
      of Hyps is entered, any "?" or "" Hyp
      entries are ignored (e.g. if "1,2,?"
      entered and 2 hyps are required, then
      "1,2" is used and the "?" is deleted by
      the program.)
    * "silent" start-up mode. Implemented with
      Runparm "OutputVerbosity,9999". The default
      is 9999, which prints input RunParm commands
      so that new users see something happening
      during startup. Input "OutputVerbosity,0"
      (< 9) to turn off printing of input
      RunParms.
    * $d soft/hard error distinction
    * un-nest ProofWorksheet inner classes
      (transparent to users)
    * replace ProofWorkStmt.status field
      (transparent to users)
    * add "instrumentation" to record elapsed time
      and memory utilization of individual RunParm
      commands (or groups of them.) New RunParms:
        StartRunParmTimer
        StopRunParmTimer
      (transparent to users)
    * efficiency and logic fixes in
      mmj.lang.ParseNode.java#unifyWithSubtree() and
      mmj.lang.ParseNode.java#isDeepDup()
      (should be transparent to users)

Documentation:

    New:

        C:?

    Renamed:


    Changed:

        mmj2\CHGLOG.TXT
        mmj2\doc\FinalizeReleaseTodos.txt
        mmj2\doc\MMJ2DirectoryStructure.txt
        mmj2\doc\PAUserGuide\cmdwindow.html
        mmj2\doc\ProofAssistantGUIDeriveFeature.html
        mmj2\doc\ProofAssistantGUIDetailedInfo.html
        mmj2\doc\ProofAssistantHelp.txt
        mmj2\doc\RunningTheMMJ2TestSuite.html
        mmj2\README.html
        mmj2\INSTALL.html
        mmj2\LicenseEnclosure.java
        mmj2\mmj2.html

    Deleted:


Source Code:

    New:

        mmj2\src\mmj\pa\ProofWorkStmt.java
        mmj2\src\mmj\pa\HeaderStmt.java
        mmj2\src\mmj\pa\ProofStepStmt.java
        mmj2\src\mmj\pa\HypothesisStep.java
        mmj2\src\mmj\pa\DerivationStep.java
        mmj2\src\mmj\pa\CommentStmt.java
        mmj2\src\mmj\pa\DistinctVariablesStmt.java
        mmj2\src\mmj\pa\GeneratedProofStmt.java
        mmj2\src\mmj\pa\FooterStmt.java

    Renamed:


    Changed:

        mmj2\src\mmj\lang\LangConstants.java
        mmj2\src\mmj\lang\Theorem.java
        mmj2\src\mmj\lang\Assrt.java
        mmj2\src\mmj\lang\MandFrame.java
        mmj2\src\mmj\lang\DjVars.java

        mmj2\src\mmj\pa\PaConstants.java
        mmj2\src\mmj\pa\ProofAsst.java
        mmj2\src\mmj\pa\ProofAsstCursor.java
        mmj2\src\mmj\pa\ProofAsstGUI.java
        mmj2\src\mmj\pa\ProofAsstPreferences.java
        mmj2\src\mmj\pa\ProofUnifier.java
        mmj2\src\mmj\pa\ProofWorksheet.java

        mmj2\src\mmj\tmff\TMFFUnformatted.java

        mmj2\src\mmj\util\BatchFramework.java
        mmj2\src\mmj\util\Boss.java
        mmj2\src\mmj\util\OutputBoss.java
        mmj2\src\mmj\util\ProofAsstBoss.java
        mmj2\src\mmj\util\UtilConstants.java

        mmj2\src\mmj\verify\VerifyProofs.java


    Deleted:


Data:

    New:

        mmj2\data\mm\big.mm
        mmj2\data\mm\dvtest1ax3.mm
        mmj2\data\mm\dvtest1ax1.mm
        mmj2\data\mm\dvtest1HDR.mm
        mmj2\data\mm\dvtest1ax2.mm
        mmj2\data\mm\dvtest1t2.mm
        mmj2\data\mm\dvtest1t3.mm
        mmj2\data\mm\dvtest1t1.mm
        mmj2\data\mmp\tests\UT4004.mmp
        mmj2\data\mmp\tests\UT4005.mmp
        mmj2\data\mmp\tests\UT4006.mmp
        mmj2\data\mmp\tests\UT4007.mmp
        mmj2\data\mmp\tests\UT4104.mmp
        mmj2\data\mmp\tests\UT4103.mmp
        mmj2\data\mmp\tests\UT4102.mmp
        mmj2\data\mmp\tests\UT4101.mmp
        mmj2\data\mmp\tests\UT4203.mmp
        mmj2\data\mmp\tests\UT4302.mmp
        mmj2\data\mmp\tests\UT4301.mmp
        mmj2\data\mmp\tests\UT4202.mmp
        mmj2\data\mmp\tests\UT4201.mmp
        mmj2\data\runparm\windows\VT2cPA002.txt
        mmj2\test\windows\RunVT2c.bat
        mmj2\test\windows\RunVolumeTest2c.bat


    Renamed:

        mmj2\data\runparm\windows\AnnotatedRunParms.txt TO
        mmj2\mmj2jar\AnnotatedRunParms.txt

        mmj2\data\mm\setFirst100.mm  TO
        mmj2\mmj2jar\setFirst100.mm

        mmj2\data\mmp\PATutorial\*.* TO
        mmj2\mmj2jar\PATutorial


    Changed:

        mmj2\compile\mmj\pa\paClasses.txt

        mmj2\data\runparm\windows\UT4001.txt
        mmj2\data\runparm\windows\VT2bPA002.txt
        mmj2\data\runparm\windows\VT2PA002.txt

        mmj2\mmj2jar\PATutorial\Page101.mmp
        mmj2\mmj2jar\PATutorial\Page407.mmp

    Deleted:


Other:

    New:


    Renamed:


    Changed:

        mmj2\mmj2jar\mmj2.bat
        mmj2\mmj2jar\mmj2PATutorial.bat
        mmj2\mmj2jar\RunParms.txt
        mmj2\mmj2jar\RunParmsPATutorial.txt
        mmj2\test\windows\RunUnitTest4.bat


    Deleted:


Regression test differences:
============================
    1)  mmj2\test\windows\RunUnitTest2.bat ->
        mmj2\data\runparm\windows\UT2PA001.txt ->
        mmj2\data\mmp\tests\EPA0354.mmp

        No longer generates error E-PA-0354 :
        - specifying an extra Hyp = "?" no longer
          an error, Proof Worksheet now unifies
          successfully.

    2) New tests added to UnitTest4:

        mmj2\test\windows\RunUnitTest4.bat ->
        mmj2\data\runparm\windows\UT4001.txt ->
        mmj2\data\mmp\tests\UT4004.mmp
        mmj2\data\mmp\tests\UT4005.mmp
        mmj2\data\mmp\tests\UT4006.mmp
        mmj2\data\mmp\tests\UT4007.mmp



==================================================================
1-Nov-2006:

    New/Changed Features -- Proof Assistant and general mmj2:

    * Text Mode Formula Formatting (TMFF);
    * Proof Get, and Browse Forward/Back through existing proofs
      (no need to export from Metamath or via mmj2 batch).
    * File/New-Next Proof menu item added which is a combination
      of File/New Proof and File/Forward-Get Proof. It creates a
      skeletal proof (like New Proof) for the next theorem in the
      database after location of the current Proof Worksheet
      (with respect to the database). This feature is provided for
      students who wish to work their way through, say, the first
      100 theorems without "cheating".
    * Norm's Theorem Descriptions displayed on File/New, File/Get,
      and File/Browse Forward/Back Proof Worksheets (obtained from
      comment immediately preceding $p statements).
    * Unification Hints - upon request, provides list of assertions
      that unify with just the formula of a proof step, disregarding
      hypotheses. This ought to become a very popular item and its
      addition makes the Derive Feature much more powerful!
    * Cursor Handling fixed (to a great extent).
    * Edit Undo/Redo (can be disabled via RunParm? :).
    * Proof Worksheet Popup Menu (e.g. right mouse/context sensitive)
      providing Cut, Copy and Paste actions.
    * Set Proof Worksheet Foreground/Background Color.
    * Help About showing memory utilization in addition to the
      typical stuff.
    * mmj2 Jar file executable download available + simplified use
      procedures.
    * Implemented 6-24-2006 Metamath.pdf spec change prohibiting
      Stmt.label and Sym.id namespace collisions.
    * Added a new RunParm to specify the Proof Worksheet to be
      displayed when the ProofAsstGUI screen is first shown. This
      was added for the benefit of the new, interactive
      Proof Assistant Tutorial, but may be otherwise useful.
    * Added new interactive Proof Assistant tutorial. See
      \mmj2jar\mmj2PATutorial.bat
    * Added "LoadProofs,no" (default "yes"). Purpose is to allow
      user to minimize memory utilization and startup time. Proofs
      of existing theorems have no use in creating new proofs. If
      set to 'no' the "VerifyProof" RunParm is ignored (but an
      informational warning message is printed.)  Saves about 15MB
      for set.mm (9/14 version).


Documentation:

    New:

        C:\mmj2\mmj2jar\mmj2PATutorial.bat (interactive)
        doc\ProofAsstGUICursorHandling.html
        doc\RunningTheMMJ2TestSuite.html
        doc\SunJavaTutorialLicense.html
        doc\TextModeFormulaFormatting.html

    Changed:

        C:\mmj2\CHGLOG.TXT
        C:\mmj2\INSTALL.html (also, renamed from INSTALL.TXT)
        C:\mmj2\mmj2.html
        C:\mmj2\LICENSE.TXT
        C:\mmj2\README.html (also, renamed from README.TXT)

        doc\BasicsOfSyntaxAxiomsAndTypes.html
        doc\EarleyParseCompletedItemSetsExample.html
        doc\MMJ2DirectoryStructure.txt
        doc\ProofAssistantGUIDetailedInfo.html
        doc\ProofAssistantGUIQuickHOWTO.html

    Deleted:
        doc\BottomUpParseFunctionAlgorithm.html
        doc\PhilosophicalNotesOnParsing.html
        doc\ProofAssistantConsiderations.html

Source Code:

    New:
        mmj\pa\ProofAsstCursor.java

        mmj.tmff package, Text Mode Formula Formatting

        mmj\tmff\TMFFAlignColumn.java
        mmj\tmff\TMFFConstants.java
        mmj\tmff\TMFFException.java
        mmj\tmff\TMFFFlat.java
        mmj\tmff\TMFFFormat.java
        mmj\tmff\TMFFMethod.java
        mmj\tmff\TMFFPreferences.java
        mmj\tmff\TMFFScheme.java
        mmj\tmff\TMFFStateParams.java
        mmj\tmff\TMFFTwoColumnAlignment.java
        mmj\tmff\TMFFUnformatted.java

        mmj\util\TMFFBoss.java

    Renamed:

        mmj\pa\RequestMessagesGUI.java (to)
        mmj\pa\UnificationErrorsGUI.java (from)

    Changed:

        mmj\lang\Assrt.java
        mmj\lang\Axiom.java
        mmj\lang\Cnst.java
        mmj\lang\Formula.java
        mmj\lang\Hyp.java
        mmj\lang\LangConstants.java
        mmj\lang\LogHyp.java
        mmj\lang\LogicalSystem.java
        mmj\lang\ParseNode.java
        mmj\lang\ProofCompression.java
        mmj\lang\MandFrame.java
        mmj\lang\MObj.java
        mmj\lang\Stmt.java
        mmj\lang\Sym.java
        mmj\lang\Theorem.java
        mmj\lang\Var.java
        mmj\lang\VarHyp.java

        mmj\mmio\MMIOConstants.java
        mmj\mmio\SrcStmt.java
        mmj\mmio\Statementizer.java
        mmj\mmio\Systemizer.java

        mmj\pa\PaConstants.java
        mmj\pa\ProofAsst.java
        mmj\pa\ProofAsstGUI.java
        mmj\pa\ProofAsstPreferences.java
        mmj\pa\ProofWorksheet.java
        mmj\pa\ProofUnifier.java

        mmj\util\BatchFramework.java
        mmj\util\BatchMMJ2.java
        mmj\util\Boss.java
        mmj\util\Dump.java
        mmj\util\LogicalSystemBoss.java
        mmj\util\OutputBoss.java
        mmj\util\ProofAsstBoss.java
        mmj\util\RunParmFile.java
        mmj\util\UtilConstants.java

        mmj\verify\GrammarConstants.java
        mmj\verify\ProofConstants.java
        mmj\verify\ProofDerivationStepEntry.java
        mmj\verify\VerifyProofs.java

Data:

    New:
        C:\mmj2\data\mm\setFirst100.mm
        C:\mmj2\data\mmp\PATutorial\*.*
        C:\mmj2\data\runparm\windows\AnnotatedRunParms.txt

    Changed:
        C:\mmj2\data\runparm\windows\RunParms.txt
            (also, renamed from RunParmFileRunPAGUI.txt)

        C:\mmj2\data\runparm\windows\Sample001.txt
        C:\mmj2\data\runparm\windows\Sample002.txt
        C:\mmj2\data\runparm\windows\Sample003.txt
        C:\mmj2\data\runparm\windows\UT2PA001.txt
        C:\mmj2\data\runparm\windows\VT2PA002.txt


Other:

    New:
        C:\mmj2\mmj2jar\*.*
        C:\mmj2\compile\mmj\tmff\tmffClasses.txt
        C:\mmj2\compile\windows\EraseMMJObjCode.bat
        C:\mmj2\compile\windows\MANIFEST.MF
        C:\mmj2\compile\windows\mkjar.bat
        C:\mmj2\compile\windows\mkjarargs.txt
        C:\mmj2\compile\linux\compilescript.txt
        doc\windows\EraseMMJJavaDoc.bat

    Changed:
        C:\mmj2\compile\mmj\pa\paClasses.txt
        C:\mmj2\compile\mmj\util\utilClasses.txt
        C:\mmj2\compile\mmj\verify\verifyClasses.txt
        C:\mmj2\compile\windows\CompMMJ.bat
        C:\mmj2\compile\windows\CompPackage.bat
        doc\windows\BuildDoc.bat
        doc\windows\DocPackages.txt
        C:\mmj2\test\windows\RunUnitTest.bat
        C:\mmj2\test\windows\RunVolumeTest2.bat
        C:\mmj2\test\windows\RunBatchFramework.bat
        C:\mmj2\test\windows\RunVolumeTest2b.bat
        C:\mmj2\test\windows\RunVT2b.bat
        C:\mmj2\test\windows\RunUnitTest2.bat
        C:\mmj2\test\windows\RunUnitTest3.bat

==================================================================
1-Apr-2006:

- Added Derive and Renumber features to Proof Assistant
- Added automatic proof decompression facility to mmj2
  (input .mm files may contain compressed and/or
   uncompressed proofs -- no RunParms changes needed
   by users except perhaps to point directly to set.mm
   instead of expset.mm).

Documentation:

    New:

        doc\ProofAssistantGUIDeriveFeature.html

    Changed:

        C:\mmj2\CHGLOG.TXT
        C:\mmj2\mmj2.html
        C:\mmj2\LICENSE.TXT
        C:\mmj2\README.TXT

        doc\ProofAssistantGUIDetailedInfo.html
        doc\ProofAssistantGUIQuickHOWTO.html

Source Code:

    New:

        mmj\lang\ProofCompression.java

    Changed:

        mmj\lang\Hyp.java
        mmj\lang\LangConstants.java
        mmj\lang\LogHyp.java
        mmj\lang\LogicalSystem.java
        mmj\lang\MObj.java
        mmj\lang\ParseNode.java
        mmj\lang\ParseTree.java
        mmj\lang\Stmt.java
        mmj\lang\SystemLoader.java
        mmj\lang\Theorem.java
        mmj\lang\Var.java
        mmj\lang\VarHyp.java

        mmj\mmio\MMIOConstants.java
        mmj\mmio\SrcStmt.java
        mmj\mmio\Statementizer.java
        mmj\mmio\Systemizer.java

        mmj\pa\PaConstants.java
        mmj\pa\ProofAsst.java
        mmj\pa\ProofAsstGUI.java
        mmj\pa\ProofAsstPreferences.java
        mmj\pa\ProofUnifier.java
        mmj\pa\ProofWorksheet.java

        mmj\util\Boss.java
        mmj\util\ProofAsstBoss.java
        mmj\util\UtilConstants.java

        mmj\verify\ProofConstants.java
        mmj\verify\VerifyProofs.java

Tests:

    New:
        C:\mmj2\test\windows\RunUnitTest3.bat
        C:\mmj2\test\windows\RunUT3.bat
        C:\mmj2\data\mm\UT3.mm
        C:\mmj2\data\runparm\windows\UT3LA001.txt

        C:\mmj2\data\mmp\EPA0370.mmp
        C:\mmj2\data\mmp\EPA0371.mmp
        C:\mmj2\data\mmp\EPA0372.mmp

    Changed:

        C:\mmj2\data\mmp\EPA0354.mmp
        C:\mmj2\data\mmp\EPA0326.mmp
        C:\mmj2\data\mmp\EPA0327.mmp
        C:\mmj2\data\mmp\EPA0328.mmp

        C:\mmj2\data\runparm\windows\Sample001.txt

        C:\mmj2\data\runparm\windows\RunParmFileRunPAGUI.txt

        C:\mmj2\data\runparm\windows\UT2PA001.txt

        C:\mmj2\data\runparm\windows\VT2PA002.txt

        C:\mmj2\test\windows\expandSetMM.bat

Compile:

    Changed:

        C:\mmj2\compile\mmj\lang\langClasses.txt
        C:\mmj2\compile\windows\CompMMJ.bat

=======================================================
Feb-01-2006:

Added Proof Assistant in new package mmj.pa, along with
new tests and some new code in old classes to support
Proof Assistant:

Source Code:

    New:
        mmj.pa package, Proof Assistant

        mmj\pa\ProofAsst.java
        mmj\pa\ProofAsstGUI.java
        mmj\pa\ProofWorksheet.java
        mmj\pa\ProofUnifier.java
        mmj\pa\ProofWorksheetParser.java
        mmj\pa\ProofAsstPreferences.java
        mmj\pa\PaConstants.java
        mmj\pa\AuxFrameGUI.java
        mmj\pa\UnificationErrorsGUI.java
        mmj\pa\HelpGeneralInfoGUI.java
        mmj\pa\ProofAsstException.java

        mmj\util\ProofAsstBoss

        mmj\verify\ProofDerivationStepEntry.java

    Changed:

        mmj\lang\Theorem.java
        mmj\lang\Axiom.java
        mmj\lang\ParseTree.java
        mmj\lang\Assrt.java
        mmj\lang\ParseNode.java
        mmj\lang\Hyp.java
        mmj\lang\Stmt.java
        mmj\lang\LogHyp.java
        mmj\lang\MandFrame.java
        mmj\lang\Formula.java
        mmj\lang\SystemLoader.java
        mmj\lang\SyntaxVerifier.java
        mmj\lang\LogicFormula.java
        mmj\lang\LogicalSystem.java
        mmj\lang\Var.java

        mmj\mmio\MMIOException.java
        mmj\mmio\Systemizer.java
        mmj\mmio\Statementizer.java
        mmj\mmio\MMIOError.java
        mmj\mmio\Tokenizer.java
        mmj\mmio\MMIOConstants.java

        mmj\util\BatchFramework.java
        mmj\util\GrammarBoss.java
        mmj\util\OutputBoss.java
        mmj\util\UtilConstants.java
        mmj\util\VerifyProofBoss.java
        mmj\util\LogicalSystemBoss.java
        mmj\util\Boss.java

        mmj\verify\Grammar.java
        mmj\verify\ProofConstants.java
        mmj\verify\VerifyProofs.java

Tests:
    New:
        C:\mmj2\test\windows\RunUnitTest2.bat
        C:\mmj2\test\windows\RunUT2.bat
        C:\mmj2\test\windows\RunVolumeTest2.bat
        C:\mmj2\test\windows\RunVT2.bat
        C:\mmj2\test\windows\RunPAGUI.bat


Documentation:
    New:
        doc\ProofAssistantGUIQuickHOWTO.html
        doc\ProofAssistantGUIDetailedInfo.html
        doc\ProofAssistantConsiderations.html
        doc\PAFeasibility01RootTotals.txt
        doc\UnificationNotes20051115.txt
        doc\UnificationNotes20060104.txt
        doc\ProofAssistant-Unification.txt
        doc\UnificationProblem1.txt
        doc\UnificationProblem2.txt
        doc\NormsPatchToSetmm.txt
        doc\SolutionOneAndTwo.txt

    Changed:
        C:\mmj2\mmj2.html
        C:\mmj2\CHGLOG.TXT
        C:\mmj2\INSTALL.TXT
        C:\mmj2\README.TXT
        doc\MMJ2DirectoryStructure.txt

==========================================================

Sep-25-2005:
- Added barrage of unit tests that seek to exercise every
  error message involving Metamath files. This excludes
  a comprehensive set of unit tests for the BatchMMJ2.java
  program as well as those messages that can't (apparently)
  be triggered with the software in its current configuration
  (for example, a bit of code isn't exercised when batch
  .mm files are read in but could be exercised if the
  java object's method were invoked directly.)

  See:
    C:\mmj2\test\windows\RunUnitTest.bat (which calls RunUT1.bat)
    C:\mmj2\test\windows\RunUT1.bat

    plus various new .mm files in
    C:\mmj2\data\mm\

    and the corresponding RunParmFiles in
    C:\mmj2\data\runparm\windows\

- mmj.verify.TypeConversionRule#deriveAdditionalRules(): bug!
  derivation of new type conversion rules -- when adding a type
  converison rule must check both rules for hypothesis matches
  (i.e. rule "B isa A" and rule "C isa B" requires derived rule
  "C isa A" regardless of the order of input of the 1st two
  rules, so attempt derivation both ways when 2nd rule is read.)

  In the example below, if the last two axioms were reversed,
  the error message was triggered, but as shown below, no error
  was reported!

    $( E-GR-0041 Syntax Axiom, label = ";
                 " is a Type Conversion Rule that creates a
                 " Type Conversion loop from Type = ";
                 ", to Type = "; $)
    $c c41a c41b c41c $.
    $v v41a v41b v41c $.
    vH41a $f c41a v41a $.
    vH41b $f c41b v41b $.
    vH41c $f c41c v41c $.
    conv41c $a c41b v41c $.
    conv41b $a c41a v41b $.
    conv41a $a c41c v41a $.

- mmj.verify.GrammarRule#add
  Change message text of E-GR-0044 to reflect fact that the
  duplicate grammar rule is *derived*, and to show the actual
  rules involved!

- mmj.util.BatchFramework.java
  Start counting RunParmFile lines at 1 (instead of 0. duh.)
  (The other differences in Sample002 output resulted
   from addition of symbol "F" to EarleyParserExample.mm
   after the Sample002 test was run (test file version
   mismatch -- oops! And similar version problem w/Sample003
   output.)

- mmj.mmio.MMIOConstants.java : misc typos
- mmj.mmio.Systemizer
- mmj.lang.LangConstants.java : misc typos
- mmj.util.Dump.java
    -> check grammar.getGrammarInitialized() in addition to "!= null"
- mmj.vxerify.ProofConstants.java : misc typos
- mmj.verify.GrammarConstants.java : misc.
- mmj.verify.Grammar : comment typo fixed.

==============================================================

Aug-30-2005:
- add CHGLOG.TXT to c:/mmj2 directory

- add note in mmj2.html about java 1.5 being needed,
  java.util.PriorityQueue is new to JDK1.5 as are
  Chained Exceptions (one is used in mmj\verify\EarleyParser.java).

- add note cautioning the user to avoid or minimize changes to
  the contents of c:/mmj2 because newer versions of mmj2 will be
  just mmj2.zip's of the entire directory, and one would not like
  to lose anything with an overlay update.

- typos
    * in c:\mmj2\mmj2.html
    * /mmj/lang/LangConstants.html#ERRMSG_PARSED_RPN_INCOMPLETE
    * /mmj/lang/LangConstants.html#ERRMSG_STMT_VAR_UNDEF
    * /mmj/verify/GrammarConstants.html#ERRMSG_EARLEY_HYP_PARAMS_NOTFND_1
    * note: double-check rest of C:/mmj2/doc/constant-values.html

- add md5 checksum file for mmj2.zip

- change getMandHypArray() to getMandHypArrayLength() due
  to compiler errors in earlier Java versions:
  "cannot override getMandHypArray() in mmj.lang.Stmt; attempting
  to use incompatible return type
        found   : mmj.lang.VarHyp[]
        required: mmj.lang.Hyp[]
             public VarHyp[] getMandHypArray() {"
  The "feature" allowing this assignment is described in 10.10
  of Java Language Specification, but even so appears less than
  robust. And mmj2 only needs the *count* of mandatory hypotheses.

  Reference Search of mmj2 =
    C:\mmj2\src\mmj\lang\Assrt.java(106): public Hyp[] getMandHypArray() {
    C:\mmj2\src\mmj\lang\LogHyp.java(101): public VarHyp[] getMandHypArray() {
    C:\mmj2\src\mmj\lang\ParseNode.java(341): int nbrChildNodes = stmt.getMandHypArray().length;
    C:\mmj2\src\mmj\lang\Stmt.java(191): public abstract Hyp[]    getMandHypArray();
    C:\mmj2\src\mmj\lang\VarHyp.java(188): public VarHyp[] getMandHypArray() {

- Removed javadoc-generated files left in c:/mmj2/doc as they
  increase the download size and are recreated from the source.