diff --git a/compile/mmj/gmff/gmffClasses.txt b/compile/mmj/gmff/gmffClasses.txt index 83495ee9..cefbbeae 100644 --- a/compile/mmj/gmff/gmffClasses.txt +++ b/compile/mmj/gmff/gmffClasses.txt @@ -1,28 +1,26 @@ -src\mmj\gmff\EscapePair.java -src\mmj\gmff\GMFFConstants.java -src\mmj\gmff\GMFFException.java -src\mmj\gmff\GMFFExportFile.java -src\mmj\gmff\GMFFExportParms.java -src\mmj\gmff\GMFFExporter.java -src\mmj\gmff\GMFFExporterTypesetDefs.java -src\mmj\gmff\GMFFFileFilter.java -src\mmj\gmff\GMFFFileNotFoundException.java -src\mmj\gmff\GMFFFolder.java -src\mmj\gmff\GMFFInputFile.java -src\mmj\gmff\GMFFManager.java -src\mmj\gmff\GMFFMandatoryModelNotFoundException.java -src\mmj\gmff\GMFFUserExportChoice.java -src\mmj\gmff\GMFFUserTextEscapes.java -src\mmj\gmff\MinCommentStmt.java -src\mmj\gmff\MinDerivationStep.java -src\mmj\gmff\MinDistinctVariablesStmt.java -src\mmj\gmff\MinFooterStmt.java -src\mmj\gmff\MinGeneratedProofStmt.java -src\mmj\gmff\MinHeaderStmt.java -src\mmj\gmff\MinHypothesisStep.java -src\mmj\gmff\MinProofStepStmt.java -src\mmj\gmff\MinProofWorkStmt.java -src\mmj\gmff\MinProofWorksheet.java -src\mmj\gmff\ModelAExporter.java -src\mmj\gmff\ProofWorksheetCache.java -src\mmj\gmff\TypesetDefCommentParser.java +src\main\java\mmj\gmff\EscapePair.java +src\main\java\mmj\gmff\GMFFConstants.java +src\main\java\mmj\gmff\GMFFException.java +src\main\java\mmj\gmff\GMFFExportFile.java +src\main\java\mmj\gmff\GMFFExportParms.java +src\main\java\mmj\gmff\GMFFExporter.java +src\main\java\mmj\gmff\GMFFExporterTypesetDefs.java +src\main\java\mmj\gmff\GMFFFileFilter.java +src\main\java\mmj\gmff\GMFFFolder.java +src\main\java\mmj\gmff\GMFFInputFile.java +src\main\java\mmj\gmff\GMFFManager.java +src\main\java\mmj\gmff\GMFFUserExportChoice.java +src\main\java\mmj\gmff\GMFFUserTextEscapes.java +src\main\java\mmj\gmff\MinCommentStmt.java +src\main\java\mmj\gmff\MinDerivationStep.java +src\main\java\mmj\gmff\MinDistinctVariablesStmt.java +src\main\java\mmj\gmff\MinFooterStmt.java +src\main\java\mmj\gmff\MinGeneratedProofStmt.java +src\main\java\mmj\gmff\MinHeaderStmt.java +src\main\java\mmj\gmff\MinHypothesisStep.java +src\main\java\mmj\gmff\MinProofStepStmt.java +src\main\java\mmj\gmff\MinProofWorkStmt.java +src\main\java\mmj\gmff\MinProofWorksheet.java +src\main\java\mmj\gmff\ModelAExporter.java +src\main\java\mmj\gmff\ProofWorksheetCache.java +src\main\java\mmj\gmff\TypesetDefCommentParser.java diff --git a/compile/mmj/lang/langClasses.txt b/compile/mmj/lang/langClasses.txt index 5d74aab6..c303da55 100644 --- a/compile/mmj/lang/langClasses.txt +++ b/compile/mmj/lang/langClasses.txt @@ -1,38 +1,34 @@ -src\mmj\lang\Assrt.java -src\mmj\lang\Axiom.java -src\mmj\lang\BookManager.java -src\mmj\lang\Chapter.java -src\mmj\lang\Cnst.java -src\mmj\lang\DjVars.java -src\mmj\lang\Formula.java -src\mmj\lang\Hyp.java -src\mmj\lang\LangConstants.java -src\mmj\lang\LangException.java -src\mmj\lang\LogHyp.java -src\mmj\lang\LogicFormula.java -src\mmj\lang\LogicalSystem.java -src\mmj\lang\MObj.java -src\mmj\lang\MandFrame.java -src\mmj\lang\Messages.java -src\mmj\lang\OptFrame.java -src\mmj\lang\ParseNode.java -src\mmj\lang\ParseNodeHolder.java -src\mmj\lang\ParseTree.java -src\mmj\lang\ProofCompression.java -src\mmj\lang\ProofVerifier.java -src\mmj\lang\ScopeDef.java -src\mmj\lang\Section.java -src\mmj\lang\SeqAssigner.java -src\mmj\lang\SystemLoader.java -src\mmj\lang\Stmt.java -src\mmj\lang\Sym.java -src\mmj\lang\SyntaxVerifier.java -src\mmj\lang\Theorem.java -src\mmj\lang\TheoremLoaderException.java -src\mmj\lang\Var.java -src\mmj\lang\VarHyp.java -src\mmj\lang\VarHypFormula.java -src\mmj\lang\VerifyException.java -src\mmj\lang\WorkVar.java -src\mmj\lang\WorkVarHyp.java -src\mmj\lang\WorkVarManager.java +src\main\java\mmj\lang\Assrt.java +src\main\java\mmj\lang\Axiom.java +src\main\java\mmj\lang\BookManager.java +src\main\java\mmj\lang\Chapter.java +src\main\java\mmj\lang\Cnst.java +src\main\java\mmj\lang\DjVars.java +src\main\java\mmj\lang\Formula.java +src\main\java\mmj\lang\Hyp.java +src\main\java\mmj\lang\LangConstants.java +src\main\java\mmj\lang\LangException.java +src\main\java\mmj\lang\LogHyp.java +src\main\java\mmj\lang\LogicalSystem.java +src\main\java\mmj\lang\MObj.java +src\main\java\mmj\lang\Messages.java +src\main\java\mmj\lang\ParseNode.java +src\main\java\mmj\lang\ParseNodeHolder.java +src\main\java\mmj\lang\ParseTree.java +src\main\java\mmj\lang\ProofCompression.java +src\main\java\mmj\lang\ProofVerifier.java +src\main\java\mmj\lang\ScopeDef.java +src\main\java\mmj\lang\ScopeFrame.java +src\main\java\mmj\lang\Section.java +src\main\java\mmj\lang\SeqAssigner.java +src\main\java\mmj\lang\Stmt.java +src\main\java\mmj\lang\Sym.java +src\main\java\mmj\lang\SyntaxVerifier.java +src\main\java\mmj\lang\SystemLoader.java +src\main\java\mmj\lang\Theorem.java +src\main\java\mmj\lang\Var.java +src\main\java\mmj\lang\VarHyp.java +src\main\java\mmj\lang\VarHypSubst.java +src\main\java\mmj\lang\WorkVar.java +src\main\java\mmj\lang\WorkVarHyp.java +src\main\java\mmj\lang\WorkVarManager.java diff --git a/compile/mmj/mmio/mmioClasses.txt b/compile/mmj/mmio/mmioClasses.txt index 1042a355..85e7c119 100644 --- a/compile/mmj/mmio/mmioClasses.txt +++ b/compile/mmj/mmio/mmioClasses.txt @@ -1,14 +1,8 @@ -src\mmj\mmio\MMIOConstants.java -src\mmj\mmio\MMIOException.java -src\mmj\mmio\MMIOError.java -src\mmj\mmio\Tokenizer.java -src\mmj\mmio\SrcStmt.java -src\mmj\mmio\Statementizer.java -src\mmj\mmio\IncludeFile.java -src\mmj\mmio\Systemizer.java - - - - - - +src\main\java\mmj\mmio\BlockList.java +src\main\java\mmj\mmio\IncludeFile.java +src\main\java\mmj\mmio\MMIOConstants.java +src\main\java\mmj\mmio\MMIOException.java +src\main\java\mmj\mmio\SrcStmt.java +src\main\java\mmj\mmio\Statementizer.java +src\main\java\mmj\mmio\Systemizer.java +src\main\java\mmj\mmio\Tokenizer.java diff --git a/compile/mmj/pa/paClasses.txt b/compile/mmj/pa/paClasses.txt index 91f14a9b..cd47bb3b 100644 --- a/compile/mmj/pa/paClasses.txt +++ b/compile/mmj/pa/paClasses.txt @@ -1,35 +1,43 @@ -src\mmj\pa\PaConstants.java -src\mmj\pa\PreprocessRequest.java -src\mmj\pa\EraseWffsPreprocessRequest.java -src\mmj\pa\AuxFrameGUI.java -src\mmj\pa\HelpGeneralInfoGUI.java -src\mmj\pa\RequestMessagesGUI.java -src\mmj\pa\ProofAsstCursor.java -src\mmj\pa\ProofAsstException.java -src\mmj\pa\ProofAsstPreferences.java -src\mmj\pa\ProofWorkStmt.java -src\mmj\pa\HeaderStmt.java -src\mmj\pa\ProofStepStmt.java -src\mmj\pa\HypothesisStep.java -src\mmj\pa\DerivationStep.java -src\mmj\pa\CommentStmt.java -src\mmj\pa\DistinctVariablesStmt.java -src\mmj\pa\GeneratedProofStmt.java -src\mmj\pa\FooterStmt.java -src\mmj\pa\ProofWorksheet.java -src\mmj\pa\ProofWorksheetParser.java -src\mmj\pa\StepRequest.java -src\mmj\pa\StepSelectorItem.java -src\mmj\pa\StepSelectorResults.java -src\mmj\pa\StepSelectorStore.java -src\mmj\pa\StepSelectorSearch.java -src\mmj\pa\StepSelectorDialog.java -src\mmj\pa\ProofUnifier.java -src\mmj\pa\UnifySubst.java -src\mmj\pa\StepUnifier.java -src\mmj\pa\ProofAsstGUI.java -src\mmj\pa\ProofAsst.java - - - - +src\main\java\mmj\pa\AuxFrameGUI.java +src\main\java\mmj\pa\BaseSetting.java +src\main\java\mmj\pa\ColorThread.java +src\main\java\mmj\pa\CommentStmt.java +src\main\java\mmj\pa\CompoundUndoManager.java +src\main\java\mmj\pa\DerivationStep.java +src\main\java\mmj\pa\DistinctVariablesStmt.java +src\main\java\mmj\pa\EraseWffsPreprocessRequest.java +src\main\java\mmj\pa\ErrorCode.java +src\main\java\mmj\pa\FooterStmt.java +src\main\java\mmj\pa\GeneratedProofStmt.java +src\main\java\mmj\pa\HeaderStmt.java +src\main\java\mmj\pa\HelpGeneralInfoGUI.java +src\main\java\mmj\pa\HighlightedDocument.java +src\main\java\mmj\pa\HypothesisStep.java +src\main\java\mmj\pa\MMJException.java +src\main\java\mmj\pa\MacroManager.java +src\main\java\mmj\pa\MacroStmt.java +src\main\java\mmj\pa\PaConstants.java +src\main\java\mmj\pa\PreprocessRequest.java +src\main\java\mmj\pa\ProofAsst.java +src\main\java\mmj\pa\ProofAsstCursor.java +src\main\java\mmj\pa\ProofAsstException.java +src\main\java\mmj\pa\ProofAsstGUI.java +src\main\java\mmj\pa\ProofAsstPreferences.java +src\main\java\mmj\pa\ProofStepStmt.java +src\main\java\mmj\pa\ProofUnifier.java +src\main\java\mmj\pa\ProofWorkStmt.java +src\main\java\mmj\pa\ProofWorksheet.java +src\main\java\mmj\pa\ProofWorksheetParser.java +src\main\java\mmj\pa\RequestMessagesGUI.java +src\main\java\mmj\pa\Serializer.java +src\main\java\mmj\pa\SessionStore.java +src\main\java\mmj\pa\Setting.java +src\main\java\mmj\pa\StepRequest.java +src\main\java\mmj\pa\StepSelectorDialog.java +src\main\java\mmj\pa\StepSelectorItem.java +src\main\java\mmj\pa\StepSelectorResults.java +src\main\java\mmj\pa\StepSelectorSearch.java +src\main\java\mmj\pa\StepSelectorStore.java +src\main\java\mmj\pa\StepUnifier.java +src\main\java\mmj\pa\UnifySubst.java +src\main\java\mmj\pa\WorksheetTokenizer.java diff --git a/compile/mmj/search/searchClasses.txt b/compile/mmj/search/searchClasses.txt new file mode 100644 index 00000000..f07b9577 --- /dev/null +++ b/compile/mmj/search/searchClasses.txt @@ -0,0 +1,121 @@ +src\main\java\mmj\search\AutoSelect.java +src\main\java\mmj\search\AutoSelectScrnMap.java +src\main\java\mmj\search\Bool.java +src\main\java\mmj\search\BoolScrnMap.java +src\main\java\mmj\search\ChapSecHierarchy.java +src\main\java\mmj\search\ChapSecHierarchyScrnMap.java +src\main\java\mmj\search\CharStrSearchDataLine.java +src\main\java\mmj\search\Comments.java +src\main\java\mmj\search\CommentsScrnMap.java +src\main\java\mmj\search\CompiledSearchArgs.java +src\main\java\mmj\search\DoubleQuote.java +src\main\java\mmj\search\DoubleQuoteScrnMap.java +src\main\java\mmj\search\ExclLabels.java +src\main\java\mmj\search\ExclLabelsScrnMap.java +src\main\java\mmj\search\ForWhat.java +src\main\java\mmj\search\ForWhatScrnMap.java +src\main\java\mmj\search\Format.java +src\main\java\mmj\search\FormatScrnMap.java +src\main\java\mmj\search\FromChap.java +src\main\java\mmj\search\FromChapScrnMap.java +src\main\java\mmj\search\FromSec.java +src\main\java\mmj\search\FromSecScrnMap.java +src\main\java\mmj\search\InWhat.java +src\main\java\mmj\search\InWhatScrnMap.java +src\main\java\mmj\search\MaxExtResults.java +src\main\java\mmj\search\MaxExtResultsScrnMap.java +src\main\java\mmj\search\MaxHyps.java +src\main\java\mmj\search\MaxHypsScrnMap.java +src\main\java\mmj\search\MaxIncompHyps.java +src\main\java\mmj\search\MaxIncompHypsScrnMap.java +src\main\java\mmj\search\MaxResults.java +src\main\java\mmj\search\MaxResultsScrnMap.java +src\main\java\mmj\search\MaxTime.java +src\main\java\mmj\search\MaxTimeScrnMap.java +src\main\java\mmj\search\MetamathSearchDataLine.java +src\main\java\mmj\search\MinHyps.java +src\main\java\mmj\search\MinHypsScrnMap.java +src\main\java\mmj\search\MinProofRefs.java +src\main\java\mmj\search\MinProofRefsScrnMap.java +src\main\java\mmj\search\Oper.java +src\main\java\mmj\search\OperScrnMap.java +src\main\java\mmj\search\OrSeparator.java +src\main\java\mmj\search\OrSeparatorScrnMap.java +src\main\java\mmj\search\OutputSort.java +src\main\java\mmj\search\OutputSortScrnMap.java +src\main\java\mmj\search\ParseExprSearchDataLine.java +src\main\java\mmj\search\ParseStmtSearchDataLine.java +src\main\java\mmj\search\ParsedSearchTerm.java +src\main\java\mmj\search\Part.java +src\main\java\mmj\search\PartScrnMap.java +src\main\java\mmj\search\PrevStepsChecked.java +src\main\java\mmj\search\PrevStepsCheckedScrnMap.java +src\main\java\mmj\search\ProximityScoring.java +src\main\java\mmj\search\ProximityScoringScrnMap.java +src\main\java\mmj\search\QuotedSearchTerm.java +src\main\java\mmj\search\RegExprSearchDataLine.java +src\main\java\mmj\search\ResultsChecked.java +src\main\java\mmj\search\ResultsCheckedScrnMap.java +src\main\java\mmj\search\ReuseDerivSteps.java +src\main\java\mmj\search\ReuseDerivStepsScrnMap.java +src\main\java\mmj\search\SearchArgs.java +src\main\java\mmj\search\SearchArgsCheckBox.java +src\main\java\mmj\search\SearchArgsComboBox.java +src\main\java\mmj\search\SearchArgsField.java +src\main\java\mmj\search\SearchArgsInt.java +src\main\java\mmj\search\SearchArgsLong.java +src\main\java\mmj\search\SearchArgsTextField.java +src\main\java\mmj\search\SearchConstants.java +src\main\java\mmj\search\SearchDataGetter.java +src\main\java\mmj\search\SearchDataLine.java +src\main\java\mmj\search\SearchDataLines.java +src\main\java\mmj\search\SearchEngine.java +src\main\java\mmj\search\SearchError.java +src\main\java\mmj\search\SearchJTextFieldPopupMenu.java +src\main\java\mmj\search\SearchJTextFieldPopupMenuListener.java +src\main\java\mmj\search\SearchMgr.java +src\main\java\mmj\search\SearchOptionsButtonAttr.java +src\main\java\mmj\search\SearchOptionsButtonHandler.java +src\main\java\mmj\search\SearchOptionsConstants.java +src\main\java\mmj\search\SearchOptionsFieldAttr.java +src\main\java\mmj\search\SearchOptionsFrame.java +src\main\java\mmj\search\SearchOptionsHelp.java +src\main\java\mmj\search\SearchOptionsIntField.java +src\main\java\mmj\search\SearchOptionsJButton.java +src\main\java\mmj\search\SearchOptionsJCheckBox.java +src\main\java\mmj\search\SearchOptionsJComboBox.java +src\main\java\mmj\search\SearchOptionsJIntegerTextField.java +src\main\java\mmj\search\SearchOptionsJTextField.java +src\main\java\mmj\search\SearchOptionsPosIntField.java +src\main\java\mmj\search\SearchOptionsScrnMap.java +src\main\java\mmj\search\SearchOptionsScrnMapField.java +src\main\java\mmj\search\SearchOutput.java +src\main\java\mmj\search\SearchOutputStore.java +src\main\java\mmj\search\SearchResultsButtonAttr.java +src\main\java\mmj\search\SearchResultsButtonHandler.java +src\main\java\mmj\search\SearchResultsConstants.java +src\main\java\mmj\search\SearchResultsData.java +src\main\java\mmj\search\SearchResultsDataField.java +src\main\java\mmj\search\SearchResultsFieldAttr.java +src\main\java\mmj\search\SearchResultsFrame.java +src\main\java\mmj\search\SearchResultsHelp.java +src\main\java\mmj\search\SearchResultsJButton.java +src\main\java\mmj\search\SearchResultsPopupMenuListener.java +src\main\java\mmj\search\SearchResultsScrnMap.java +src\main\java\mmj\search\SearchResultsScrnMapField.java +src\main\java\mmj\search\SearchSelectionItem.java +src\main\java\mmj\search\SearchSelectionJList.java +src\main\java\mmj\search\SearchSelectionScrnMap.java +src\main\java\mmj\search\SearchUnifier.java +src\main\java\mmj\search\SingleQuote.java +src\main\java\mmj\search\SingleQuoteScrnMap.java +src\main\java\mmj\search\Stats.java +src\main\java\mmj\search\StatsScrnMap.java +src\main\java\mmj\search\Substitutions.java +src\main\java\mmj\search\SubstitutionsScrnMap.java +src\main\java\mmj\search\ThruChap.java +src\main\java\mmj\search\ThruChapScrnMap.java +src\main\java\mmj\search\ThruSec.java +src\main\java\mmj\search\ThruSecScrnMap.java +src\main\java\mmj\search\Unifiable.java +src\main\java\mmj\search\UnifiableScrnMap.java diff --git a/compile/mmj/setmm/setmmClasses.txt b/compile/mmj/setmm/setmmClasses.txt new file mode 100644 index 00000000..9a1c91da --- /dev/null +++ b/compile/mmj/setmm/setmmClasses.txt @@ -0,0 +1,5 @@ +src\main\java\mmj\setmm\FolTranslator.java +src\main\java\mmj\setmm\LFTerm.java +src\main\java\mmj\setmm\LFType.java +src\main\java\mmj\setmm\SetMMConstants.java +src\main\java\mmj\setmm\SetMMException.java diff --git a/compile/mmj/svc/svcClasses.txt b/compile/mmj/svc/svcClasses.txt index 6c19c53f..cf1bc641 100644 --- a/compile/mmj/svc/svcClasses.txt +++ b/compile/mmj/svc/svcClasses.txt @@ -1,5 +1 @@ -src\mmj\svc\SvcCallback.java - - - - +src\main\java\mmj\svc\SvcCallback.java diff --git a/compile/mmj/tl/tlClasses.txt b/compile/mmj/tl/tlClasses.txt index 9b0d9daa..7f525d40 100644 --- a/compile/mmj/tl/tlClasses.txt +++ b/compile/mmj/tl/tlClasses.txt @@ -1,18 +1,13 @@ - -src\mmj\tl\TheoremLoaderCommitListener.java -src\mmj\tl\TheoremStmtGroup.java -src\mmj\tl\TlConstants.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\TlPreferences.java -src\mmj\tl\TheoremLoader.java -src\mmj\tl\TLRequest.java -src\mmj\tl\StoreInLogSysAndMMTFolderTLRequest.java -src\mmj\tl\StoreInMMTFolderTLRequest.java - - - - +src\main\java\mmj\tl\MMTFileFilter.java +src\main\java\mmj\tl\MMTFolder.java +src\main\java\mmj\tl\MMTTheoremExportFormatter.java +src\main\java\mmj\tl\MMTTheoremFile.java +src\main\java\mmj\tl\MMTTheoremSet.java +src\main\java\mmj\tl\StoreInMMTFolderTLRequest.java +src\main\java\mmj\tl\TLRequest.java +src\main\java\mmj\tl\TheoremLoader.java +src\main\java\mmj\tl\TheoremLoaderCommitListener.java +src\main\java\mmj\tl\TheoremLoaderException.java +src\main\java\mmj\tl\TheoremStmtGroup.java +src\main\java\mmj\tl\TlConstants.java +src\main\java\mmj\tl\TlPreferences.java diff --git a/compile/mmj/tmff/tmffClasses.txt b/compile/mmj/tmff/tmffClasses.txt index 547fd14f..4e011c61 100644 --- a/compile/mmj/tmff/tmffClasses.txt +++ b/compile/mmj/tmff/tmffClasses.txt @@ -1,16 +1,11 @@ -src\mmj\tmff\TMFFAlignColumn.java -src\mmj\tmff\TMFFConstants.java -src\mmj\tmff\TMFFException.java -src\mmj\tmff\TMFFFlat.java -src\mmj\tmff\TMFFFormat.java -src\mmj\tmff\TMFFMethod.java -src\mmj\tmff\TMFFPreferences.java -src\mmj\tmff\TMFFScheme.java -src\mmj\tmff\TMFFStateParams.java -src\mmj\tmff\TMFFTwoColumnAlignment.java -src\mmj\tmff\TMFFUnformatted.java - - - - - +src\main\java\mmj\tmff\TMFFAlignColumn.java +src\main\java\mmj\tmff\TMFFConstants.java +src\main\java\mmj\tmff\TMFFException.java +src\main\java\mmj\tmff\TMFFFlat.java +src\main\java\mmj\tmff\TMFFFormat.java +src\main\java\mmj\tmff\TMFFMethod.java +src\main\java\mmj\tmff\TMFFPreferences.java +src\main\java\mmj\tmff\TMFFScheme.java +src\main\java\mmj\tmff\TMFFStateParams.java +src\main\java\mmj\tmff\TMFFTwoColumnAlignment.java +src\main\java\mmj\tmff\TMFFUnformatted.java diff --git a/compile/mmj/transforms/transformsClasses.txt b/compile/mmj/transforms/transformsClasses.txt new file mode 100644 index 00000000..f0475e1f --- /dev/null +++ b/compile/mmj/transforms/transformsClasses.txt @@ -0,0 +1,31 @@ +src\main\java\mmj\transforms\AssocComComplexRuleMap.java +src\main\java\mmj\transforms\AssocComTransformation.java +src\main\java\mmj\transforms\AssocTree.java +src\main\java\mmj\transforms\AssociativeInfo.java +src\main\java\mmj\transforms\AssociativeTransformation.java +src\main\java\mmj\transforms\CanonicalOperandHelper.java +src\main\java\mmj\transforms\ClosureInfo.java +src\main\java\mmj\transforms\CommutativeInfo.java +src\main\java\mmj\transforms\CommutativeTransformation.java +src\main\java\mmj\transforms\ComplexRuleMap.java +src\main\java\mmj\transforms\ConjunctionInfo.java +src\main\java\mmj\transforms\ConstSubst.java +src\main\java\mmj\transforms\DBInfo.java +src\main\java\mmj\transforms\EquivalenceInfo.java +src\main\java\mmj\transforms\GenProofStepStmt.java +src\main\java\mmj\transforms\GeneralizedStmt.java +src\main\java\mmj\transforms\IdentityTransformation.java +src\main\java\mmj\transforms\ImplicationInfo.java +src\main\java\mmj\transforms\ParseNodeHashElem.java +src\main\java\mmj\transforms\Pattern.java +src\main\java\mmj\transforms\PropertyTemplate.java +src\main\java\mmj\transforms\Prover.java +src\main\java\mmj\transforms\Provers.java +src\main\java\mmj\transforms\ReplaceInfo.java +src\main\java\mmj\transforms\ReplaceTransformation.java +src\main\java\mmj\transforms\TrConstants.java +src\main\java\mmj\transforms\TrOutput.java +src\main\java\mmj\transforms\TrUtil.java +src\main\java\mmj\transforms\Transformation.java +src\main\java\mmj\transforms\TransformationManager.java +src\main\java\mmj\transforms\WorksheetInfo.java diff --git a/compile/mmj/util/utilClasses.txt b/compile/mmj/util/utilClasses.txt index 6bac04e2..51d2f52e 100644 --- a/compile/mmj/util/utilClasses.txt +++ b/compile/mmj/util/utilClasses.txt @@ -1,22 +1,28 @@ -src\mmj\util\BatchFramework.java -src\mmj\util\BatchMMJ2.java -src\mmj\util\Boss.java -src\mmj\util\CommandLineArguments.java -src\mmj\util\DelimitedTextParser.java -src\mmj\util\Dump.java -src\mmj\util\GMFFBoss.java -src\mmj\util\GrammarBoss.java -src\mmj\util\LogicalSystemBoss.java -src\mmj\util\MMJ2FailPopupWindow.java -src\mmj\util\MergeSortedArrayLists.java -src\mmj\util\OutputBoss.java -src\mmj\util\Paths.java -src\mmj\util\ProofAsstBoss.java -src\mmj\util\RunParmArrayEntry.java -src\mmj\util\RunParmFile.java -src\mmj\util\SvcBoss.java -src\mmj\util\TMFFBoss.java -src\mmj\util\TheoremLoaderBoss.java -src\mmj\util\UtilConstants.java -src\mmj\util\VerifyProofBoss.java -src\mmj\util\WorkVarBoss.java +src\main\java\mmj\util\BatchCommand.java +src\main\java\mmj\util\BatchDocumentationGenerator.java +src\main\java\mmj\util\BatchFramework.java +src\main\java\mmj\util\BatchMMJ2.java +src\main\java\mmj\util\Boss.java +src\main\java\mmj\util\CommandLineArguments.java +src\main\java\mmj\util\DelimitedTextParser.java +src\main\java\mmj\util\Dump.java +src\main\java\mmj\util\GMFFBoss.java +src\main\java\mmj\util\GrammarBoss.java +src\main\java\mmj\util\LogicalSystemBoss.java +src\main\java\mmj\util\MMJ2FailPopupWindow.java +src\main\java\mmj\util\MacroBoss.java +src\main\java\mmj\util\MergeSortedArrayLists.java +src\main\java\mmj\util\OutputBoss.java +src\main\java\mmj\util\Paths.java +src\main\java\mmj\util\ProofAsstBoss.java +src\main\java\mmj\util\RunParmArrayEntry.java +src\main\java\mmj\util\RunParmFile.java +src\main\java\mmj\util\StopWatch.java +src\main\java\mmj\util\StoreBoss.java +src\main\java\mmj\util\SvcBoss.java +src\main\java\mmj\util\TMFFBoss.java +src\main\java\mmj\util\TheoremLoaderBoss.java +src\main\java\mmj\util\TopologicalSorter.java +src\main\java\mmj\util\UtilConstants.java +src\main\java\mmj\util\VerifyProofBoss.java +src\main\java\mmj\util\WorkVarBoss.java diff --git a/compile/mmj/verify/verifyClasses.txt b/compile/mmj/verify/verifyClasses.txt index 853b3664..7a8b99f9 100644 --- a/compile/mmj/verify/verifyClasses.txt +++ b/compile/mmj/verify/verifyClasses.txt @@ -1,17 +1,20 @@ -src\mmj\verify\BottomUpParser.java -src\mmj\verify\EarleyItem.java -src\mmj\verify\EarleyParser.java -src\mmj\verify\Grammar.java -src\mmj\verify\GrammarAmbiguity.java -src\mmj\verify\GrammarConstants.java -src\mmj\verify\GrammarRule.java -src\mmj\verify\GrammaticalParser.java -src\mmj\verify\GRForest.java -src\mmj\verify\GRNode.java -src\mmj\verify\NotationRule.java -src\mmj\verify\NullsPermittedRule.java -src\mmj\verify\ProofConstants.java -src\mmj\verify\ProofDerivationStepEntry.java -src\mmj\verify\SubstMapEntry.java -src\mmj\verify\TypeConversionRule.java -src\mmj\verify\VerifyProofs.java +src\main\java\mmj\verify\BottomUpParser.java +src\main\java\mmj\verify\EarleyItem.java +src\main\java\mmj\verify\EarleyParser.java +src\main\java\mmj\verify\GRForest.java +src\main\java\mmj\verify\GRNode.java +src\main\java\mmj\verify\Grammar.java +src\main\java\mmj\verify\GrammarAmbiguity.java +src\main\java\mmj\verify\GrammarConstants.java +src\main\java\mmj\verify\GrammarRule.java +src\main\java\mmj\verify\GrammaticalParser.java +src\main\java\mmj\verify\HypsOrder.java +src\main\java\mmj\verify\LRParser.java +src\main\java\mmj\verify\NotationRule.java +src\main\java\mmj\verify\NullsPermittedRule.java +src\main\java\mmj\verify\ProofConstants.java +src\main\java\mmj\verify\ProofDerivationStepEntry.java +src\main\java\mmj\verify\SubstMapEntry.java +src\main\java\mmj\verify\TypeConversionRule.java +src\main\java\mmj\verify\VerifyException.java +src\main\java\mmj\verify\VerifyProofs.java diff --git a/compile/windows/CompMMJ.bat b/compile/windows/CompMMJ.bat index 44074862..828bb95f 100644 --- a/compile/windows/CompMMJ.bat +++ b/compile/windows/CompMMJ.bat @@ -6,49 +6,61 @@ REM that it is simplest to just recompile everything everytime.) REM - creates a jar file for mmj2 REM =================================================================== -PUSHD c:\mmj2 +PUSHD %1 :STEP0 -CALL compile\windows\EraseMMJObjCode.bat +CALL compile\windows\EraseMMJObjCode.bat %1 :STEP1 -CALL compile\windows\CompPackage.bat c:\mmj2 mmio +CALL compile\windows\CompPackage.bat %1 mmio REM IF ERRORLEVEL 1 GOTO :OUCH :STEP2 -CALL compile\windows\CompPackage.bat c:\mmj2 lang +CALL compile\windows\CompPackage.bat %1 lang REM IF ERRORLEVEL 1 GOTO :OUCH :STEP3 -CALL compile\windows\CompPackage.bat c:\mmj2 verify +CALL compile\windows\CompPackage.bat %1 verify REM IF ERRORLEVEL 1 GOTO :OUCH :STEP4 -CALL compile\windows\CompPackage.bat c:\mmj2 util +CALL compile\windows\CompPackage.bat %1 util REM IF ERRORLEVEL 1 GOTO :OUCH :STEP5 -CALL compile\windows\CompPackage.bat c:\mmj2 pa +CALL compile\windows\CompPackage.bat %1 pa REM IF ERRORLEVEL 1 GOTO :OUCH :STEP6 -CALL compile\windows\CompPackage.bat c:\mmj2 tmff +CALL compile\windows\CompPackage.bat %1 tmff +REM IF ERRORLEVEL 1 GOTO :OUCH + +:STEP6.1 +CALL compile\windows\CompPackage.bat %1 search +REM IF ERRORLEVEL 1 GOTO :OUCH + +:STEP6.2 +CALL compile\windows\CompPackage.bat %1 setmm REM IF ERRORLEVEL 1 GOTO :OUCH :STEP7 -CALL compile\windows\CompPackage.bat c:\mmj2 svc +CALL compile\windows\CompPackage.bat %1 svc REM IF ERRORLEVEL 1 GOTO :OUCH :STEP8 -CALL compile\windows\CompPackage.bat c:\mmj2 tl +CALL compile\windows\CompPackage.bat %1 tl +REM IF ERRORLEVEL 1 GOTO :OUCH + +:STEP8.1 +CALL compile\windows\CompPackage.bat %1 transforms REM IF ERRORLEVEL 1 GOTO :OUCH :STEP9 -CALL compile\windows\CompPackage.bat c:\mmj2 gmff +CALL compile\windows\CompPackage.bat %1 gmff REM IF ERRORLEVEL 1 GOTO :OUCH :STEP99 -CALL compile\windows\mkjar.bat c:\mmj2 +CALL compile\windows\mkjar.bat %1 REM IF ERRORLEVEL 1 GOTO :OUCH diff --git a/compile/windows/EraseMMJObjCode.bat b/compile/windows/EraseMMJObjCode.bat index 801d09b8..9e76694e 100644 --- a/compile/windows/EraseMMJObjCode.bat +++ b/compile/windows/EraseMMJObjCode.bat @@ -3,15 +3,18 @@ REM EraseMMJObjCode does: REM - erases old compiled classes in all MMJ packages REM =================================================================== -PUSHD c:\mmj2 +PUSHD %1 :STEP1 erase /Q classes\mmj\gmff\*.class erase /Q classes\mmj\lang\*.class erase /Q classes\mmj\mmio\*.class erase /Q classes\mmj\pa\*.class +erase /Q classes\mmj\search\*.class +erase /Q classes\mmj\setmm\*.class erase /Q classes\mmj\svc\*.class erase /Q classes\mmj\tl\*.class +erase /Q classes\mmj\transforms\*.class erase /Q classes\mmj\tmff\*.class erase /Q classes\mmj\util\*.class erase /Q classes\mmj\verify\*.class diff --git a/compile/windows/javacCompilePaths.txt b/compile/windows/javacCompilePaths.txt index 4d044dfe..b4eef1a8 100644 --- a/compile/windows/javacCompilePaths.txt +++ b/compile/windows/javacCompilePaths.txt @@ -1 +1 @@ --classpath .;c:\mmj2\classes; -d c:\mmj2\classes -sourcepath c:\mmj2\src +-classpath .;c:\mmj2\classes; -d c:\mmj2\classes -sourcepath c:\mmj2\src\main\java diff --git a/compile/windows/mkjarargs.txt b/compile/windows/mkjarargs.txt index 2b01c4ef..c9c2f542 100644 --- a/compile/windows/mkjarargs.txt +++ b/compile/windows/mkjarargs.txt @@ -1,9 +1,12 @@ -C classes mmj\gmff --C classes mmj\lang --C classes mmj\mmio --C classes mmj\pa +-C classes mmj\lang +-C classes mmj\mmio +-C classes mmj\pa +-C classes mmj\search +-C classes mmj\setmm -C classes mmj\svc -C classes mmj\tl +-C classes mmj\transforms -C classes mmj\tmff --C classes mmj\util +-C classes mmj\util -C classes mmj\verify