public class UtilConstants
extends java.lang.Object
There are two primary types of constants: parameters that are "hardcoded" which affect/control processing, and error/info messages.
Each mmj message begins with a code, such as this:
E-LA-0007
where the format of the code is X-YY-9999
X
: error level
E
= Error
I
= Information
A
= Abort (processing terminates, usually a bug).
YY
: source code
GM
= mmj.gmff package (see GMFFConstants
)
GR
= mmj.verify.Grammar and related code (see
GrammarConstants
)
IO
= mmj.mmio package (see MMIOConstants
)
LA
= mmj.lang package (see GMFFConstants
)
PA
= mmj.pa package (proof assistant) (see PaConstants
)
PR
= mmj.verify.VerifyProof and related code (see
ProofConstants
)
TL
= mmj.tl package (Theorem Loader).
TM
= mmj.tmff.AlignColumn and related code
UT
= mmj.util package. (see UtilConstants
)
TR
= mmj.transforms package (proof assistant) (see
TrConstants
)
9999
: sequential number within the source code, 0001 through
9999.
=============================================================
RunParmFile parameter Names (1st field on a RunParmFile line).
The only mandatory RunParm is RUNPARM_LOAD_FILE, and even that is not required if nothing much is desired :)
All other RunParms have defaults or invoke processing that is optional. For example proof verification is done only if RUNPARM_VERIFY_PROOF is entered.
There are "state" variables in BatchMMJ's handling of RunParms. Some situations are dealt with automatically while others result in an error.
A RunParm error, either in the parm values or the "state" (combination of RunParms) terminates processing immediately (BatchMMJ will not continue with subsequent commands after a bogosity,)
It is simplest to sequence RunParmFile lines with the non-executable commands first. These are the settings that modify subsequent processing and stay in effect until superceded.
"Executable" RunParms: 000000000011111111112 012345678901234567890... ---------------------------- Clear GarbageCollection LoadFile LoadTheoremsFromMMTFolder VerifyProof VerifyParse Parse InitializeGrammar PrintSyntaxDetails PrintStatementDetails PrintBookManagerChapters PrintBookManagerSections PrintBookManagerSectionDetails ProofAsstExportToFile ProofAsstBatchTest StepSelectorBatchTest PreprocessRequestBatchTest RunProofAsstGUI SvcCall ExtractTheoremToMMTFolder Example #1 RunParmFile to load 1 file, verify proofs, edit grammar, parse, print syntax and statement details, and print BookManager data: 000000000011111111112 012345678901234567890... MaxStatementPrintCount,9999 Caption,Example #1 MaxErrorMessages,500 MaxInfoMessages,500 LoadFile,c:\metamath\expset.mm VerifyProof,* Parse,* PrintSyntaxDetails PrintStatementDetails,* PrintBookManagerChapters PrintBookManagerSections PrintBookManagerSectionDetails,* Example #2 RunParmFile doing the exact same thing except this time: - specifying the default values AND - sending the output to files AND - specify Load Limits for the input .mm file(s) to stop loading Metamath statements after a given number of statements and/or a given statement label is reached. - loading an extra .mm file on top of the old one! AND - specify TheoremLoader stuff! - doing a belt-and-suspenders double-check of the parse RPN's! with - Set Proof Asst parms, export the input theorems' proofs, read that file back in as a test, and then - Trigger the ProofAsstGUI - generous use of blank comment lines for readability! - and THEN we clear and load a different file! 000000000011111111112 012345678901234567890... OutputVerbosity,9999 CommentLine: Example #2 - default charsets="" and new/update parameter SystemErrorFile,c:\my\mmjSyserrTest001.txt,new,"" SystemOutputFile,c:\my\mmjSysoutTest001.txt,new,"" MaxErrorMessages,500 MaxInfoMessages,500 SymbolTableInitialSize,600 StatementTableInitialSize,30000 SeqAssignerIntervalSize,100 SeqAssignerIntervalTblInitialSize,100 LoadEndpointStmtNbr,5000 LoadEndpointStmtLabel,FermatsLastTheorem LoadComments,yes LoadProofs,yes ProvableLogicStmtType,|- LogicStmtType,wff BookManagerEnabled,yes GrammarAmbiguityEdits,basic StatementAmbiguityEdits,basic MaxStatementPrintCount,9999 Caption,Example #2 LoadFile,c:\metamath\expset.mm LoadFile,c:\metamath\expset2.mm TheoremLoaderMMTFolder,c:\my\mmtFolder TheoremLoaderDjVarsOption,Replace TheoremLoaderAuditMessages,Yes TheoremLoaderStoreFormulasAsIs,Yes TheoremLoaderStoreMMIndentAmt,2 TheoremLoaderStoreMMRightCol,79 LoadTheoremsFromMMTFolder,* UnifyPlusStoreInMMTFolder,syl.mmp UnifyPlusStoreInLogSysAndMMTFolder,syl.mmp ExtractTheoremToMMTFolder,syl VerifyProof,* Parse,* VerifyParse,* ===TMFF stuff follows=== TMFFDefineScheme,AlignVarDepth1,AlignColumn,1,Var,1,Var TMFFDefineScheme,AlignVarDepth2,AlignColumn,2,Var,1,Var TMFFDefineScheme,AlignVarDepth3,AlignColumn,3,Var,1,Var TMFFDefineScheme,AlignVarDepth4,AlignColumn,4,Var,1,Var TMFFDefineScheme,AlignVarDepth5,AlignColumn,5,Var,1,Var TMFFDefineScheme,AlignVarDepth99,AlignColumn,99,Var,1,Var TMFFDefineScheme,Flat,Flat TMFFDefineScheme,PrefixDepth3,AlignColumn,3,Sym,2,Sym TMFFDefineScheme,PostfixDepth3,AlignColumn,3,Sym,1,Sym TMFFDefineScheme,TwoColumnAlignmentDepth1,TwoColumnAlignment,1 TMFFDefineScheme,TwoColumnAlignmentDepth2,TwoColumnAlignment,2 TMFFDefineScheme,TwoColumnAlignmentDepth3,TwoColumnAlignment,3 TMFFDefineScheme,TwoColumnAlignmentDepth4,TwoColumnAlignment,4 TMFFDefineScheme,TwoColumnAlignmentDepth5,TwoColumnAlignment,5 TMFFDefineScheme,TwoColumnAlignmentDepth99,TwoColumnAlignment,99 Note: "Unformatted" and Format 0 are hardcoded -- they cannot be redefined via RunParms. TMFFDefineScheme,Unformatted,Unformatted TMFFDefineFormat,1,AlignVarDepth1 TMFFDefineFormat,2,AlignVarDepth2 TMFFDefineFormat,3,AlignVarDepth3 TMFFDefineFormat,4,AlignVarDepth4 TMFFDefineFormat,5,AlignVarDepth5 TMFFDefineFormat,6,AlignVarDepth99 TMFFDefineFormat,7,Flat TMFFDefineFormat,8,PrefixDepth3 TMFFDefineFormat,9,PostfixDepth3 TMFFDefineFormat,10,TwoColumnAlignmentDepth99 TMFFDefineFormat,11,TwoColumnAlignmentDepth1 TMFFDefineFormat,12,TwoColumnAlignmentDepth2 TMFFDefineFormat,13,TwoColumnAlignmentDepth3 TMFFDefineFormat,14,TwoColumnAlignmentDepth4 TMFFDefineFormat,15,TwoColumnAlignmentDepth5 TMFFUseFormat,3 TMFFAltFormat,7 TMFFUseIndent,0 TMFFAltIndent,1 PrintSyntaxDetails PrintStatementDetails,* PrintBookManagerChapters PrintBookManagerSections PrintBookManagerSectionDetails,* ProofAsstFontSize,14 ProofAsstFontBold,yes ProofAsstFontFamily,Monospaced ProofAsstForegroundColorRGB,0,0,0 ProofAsstBackgroundColorRGB,255,255,255 ProofAsstFormulaLeftCol,20 ProofAsstFormulaRightCol,79 ProofAsstTextColumns,80 ProofAsstTextRows,21 ProofAsstErrorMessageRows,4 ProofAsstErrorMessageColumns,80 ProofAsstTextAtTop,yes ProofAsstIncompleteStepCursor,Last ProofAsstRPNProofLeftCol,6 ProofAsstRPNProofRightCol,79 ProofAsstOutputCursorInstrumentation,no ProofAsstAutoReformat,yes ProofAsstProofFolder,c:\my\proofs RecheckProofAsstUsingProofVerifier,yes ProofAsstUndoRedoEnabled,yes ProofAsstUnifySearchExclude,biigb,xxxid ProofAsstExportToFile,*,c:\my\export.mmp,new,un-unified,Randomized,Print ProofAsstBatchTest,*,c:\my\export.mmp,un-unified,NotRandomized,NoPrint StepSelectorBatchTest,c:\my\export.mmp,50,0 PreprocessRequestBatchTest,c:\my\export.mmp,EraseAndRederiveFormulas ProofAsstStartupProofWorksheet,c:\mmj2\data\mmp\PATutorial\Page101.mmp StepSelectorMaxResults,50 StepSelectorShowSubstitutions,yes StepSelectorDialogPaneWidth,720 StepSelectorDialogPaneHeight,440 ProofAsstAssrtListFreespace,5 RunProofAsstGUI Comment: now load & process another .mm file!!!! clear GarbageCollection LoadFile,c:\metamath\exppeano.mm VerifyProof,* PrintSyntaxDetails PrintStatementDetails,* Comment: now load another .mm and make SvcCallback!!!! clear GarbageCollection LoadFile,c:\metamath\set.mm VerifyProof,* Parse,* SvcFolder,c:\myProduct SvcCallbackClass,MyProductMMJ2SvcCallback SvcArg,ZipOutput,yes SvcArg,OrgFilesBy,chapter SvcArg,ExportFormat,mmjbert SvcArg,whatever,whatever SvcCall
============================================================= ----> RunParm Default Values. Some options have defaults and allowable values defined elsewhere. See: mmj.mmio.MMIOConstants.java mmj.lang.LangConstants.java mmj.verify.GrammarConstants.java mmj.verify.ProofConstants.java mmj.pa.PaConstants.java mmj.tl.TlConstants.java =============================================================
Modifier and Type | Class and Description |
---|---|
static class |
UtilConstants.RunParmContext |
Constructor and Description |
---|
UtilConstants() |
public static final java.lang.String JAVA_VERSION_PROPERTY_NAME
public static final int JAVA_VERSION_MMJ2_MAJ
public static final int JAVA_VERSION_MMJ2_MIN
public static final java.lang.String JAVA_VERSION_MMJ2_RUNTIME_ERROR_MSG
public static final java.lang.String RUN_PARM_FILE_REPORT_LINE_1
public static final java.lang.String MMJ2_PATH_REPORT_LINE_1
public static final java.lang.String METAMATH_PATH_REPORT_LINE_2
public static final java.lang.String SVC_PATH_REPORT_LINE_3
public static final java.lang.String PATH_REPORT_E_G_CAPTION_1
public static final java.lang.String PATH_REPORT_E_G_CAPTION_2
public static final java.lang.String PATH_REPORT_EXAMPLE_FILE_NAME
public static final int RUNPARM_FILE_NAME_ARGUMENT_INDEX
public static final int DISPLAY_MMJ2_FAIL_POPUP_WINDOW_ARGUMENT_INDEX
public static final int MMJ2_PATH_ARGUMENT_INDEX
public static final int METAMATH_PATH_ARGUMENT_INDEX
public static final int SVC_PATH_ARGUMENT_INDEX
public static final int TEST_OPTION_ARGUMENT_INDEX
public static final java.lang.String RUNPARM_FILE_NAME_ARGUMENT_LITERAL
public static final java.lang.String DISPLAY_MMJ2_FAIL_POPUP_WINDOW_ARGUMENT_LITERAL
public static final java.lang.String MMJ2_PATH_ARGUMENT_LITERAL
public static final java.lang.String METAMATH_PATH_ARGUMENT_LITERAL
public static final java.lang.String SVC_PATH_ARGUMENT_LITERAL
public static final boolean DISPLAY_MMJ2_FAIL_POPUP_WINDOW_DEFAULT
public static final java.lang.String YES_ARGUMENT
public static final java.lang.String NO_ARGUMENT
public static final MMJException.ErrorContext ERRMSG_COMMAND_LINE_ARGUMENTS_FORMAT
public static final java.lang.String ARGUMENTS_OPTION_REPORT_LINE_1
public static final java.lang.String ARGUMENTS_OPTION_REPORT_LINE_2
public static final java.lang.String ARGUMENTS_OPTION_REPORT_LINE_3A
public static final java.lang.String ARGUMENTS_OPTION_REPORT_LINE_3B
public static final java.lang.String ARGUMENTS_OPTION_REPORT_LINE_4
public static final java.lang.String ARGUMENTS_OPTION_REPORT_LINE_5
public static final java.lang.String MMJ2_FAIL_DIALOG_TITLE
public static final java.lang.String MMJ2_FAIL_STARTUP_DIALOG_TITLE
public static final java.lang.String MMJ2_STARTUP_MSG_LIT_1
public static final java.lang.String MMJ2_STARTUP_MSG_LIT_2
public static final java.lang.String MMJ2_STARTUP_MSG_LIT_3
public static final int LINE_BREAK_MAX_LENGTH
public static final char NEW_LINE_CHAR
public static final int MAX_STARTUP_ERROR_MESSAGES
public static final int RUNPARM_LINE_DUMP_VERBOSITY
public static final char RUNPARM_FIELD_DELIMITER_DEFAULT
public static final char RUNPARM_FIELD_QUOTER_DEFAULT
public static final char RUNPARM_COMMENT_CHAR_SPACE
public static final char RUNPARM_COMMENT_CHAR_SLASH
public static final char RUNPARM_COMMENT_CHAR_ASTERISK
public static final BatchCommand RUNPARM_PROVABLE_LOGIC_STMT_TYPE
public static final BatchCommand RUNPARM_LOGIC_STMT_TYPE
public static final BatchCommand RUNPARM_BOOK_MANAGER_ENABLED
public static final BatchCommand RUNPARM_CLEAR
public static final BatchCommand RUNPARM_JAVA_GARBAGE_COLLECTION
public static final BatchCommand RUNPARM_SYSERR_FILE
public static final BatchCommand RUNPARM_SYSOUT_FILE
public static final BatchCommand RUNPARM_OUTPUT_VERBOSITY
public static final BatchCommand RUNPARM_START_INSTRUMENTATION_TIMER
public static final BatchCommand RUNPARM_STOP_INSTRUMENTATION_TIMER
public static final BatchCommand RUNPARM_LOAD_FILE
public static final BatchCommand RUNPARM_LOAD_ENDPOINT_STMT_NBR
public static final BatchCommand RUNPARM_LOAD_ENDPOINT_STMT_LABEL
public static final BatchCommand RUNPARM_LOAD_COMMENTS
public static final BatchCommand RUNPARM_LOAD_PROOFS
public static final BatchCommand RUNPARM_MAX_ERROR_MESSAGES
public static final BatchCommand RUNPARM_MAX_INFO_MESSAGES
public static final BatchCommand RUNPARM_SYM_TBL_INITIAL_SIZE
public static final BatchCommand RUNPARM_STMT_TBL_INITIAL_SIZE
public static final BatchCommand RUNPARM_SEQ_ASSIGNER_INTERVAL_SIZE
public static final BatchCommand RUNPARM_SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE
public static final BatchCommand RUNPARM_GRAMMAR_AMBIGUITY_EDITS
public static final BatchCommand RUNPARM_STATEMENT_AMBIGUITY_EDITS
public static final BatchCommand RUNPARM_MAX_STATEMENT_PRINT_COUNT
public static final BatchCommand RUNPARM_CAPTION
public static final BatchCommand RUNPARM_PRINT_SYNTAX_DETAILS
public static final BatchCommand RUNPARM_PRINT_STATEMENT_DETAILS
public static final BatchCommand RUNPARM_PRINT_BOOK_MANAGER_CHAPTERS
public static final BatchCommand RUNPARM_PRINT_BOOK_MANAGER_SECTIONS
public static final BatchCommand RUNPARM_PRINT_BOOK_MANAGER_SECTION_DETAILS
public static final BatchCommand RUNPARM_VERIFY_PROOF
public static final BatchCommand RUNPARM_VERIFY_PARSE
public static final BatchCommand RUNPARM_SET_PARSER
public static final BatchCommand RUNPARM_PARSE
public static final BatchCommand RUNPARM_INITIALIZE_GRAMMAR
public static final BatchCommand RUNPARM_PROOF_ASST_STORE
public static final BatchCommand RUNPARM_PROOF_ASST_LOOK_AND_FEEL
public static final BatchCommand RUNPARM_PROOF_ASST_DJ_VARS_SOFT_ERRORS
public static final BatchCommand RUNPARM_PROOF_ASST_PROOF_FORMAT
public static final BatchCommand RUNPARM_PROOF_ASST_AUTOCOMPLETE_ENABLED
public static final BatchCommand RUNPARM_PROOF_ASST_DERIVE_AUTOCOMPLETE
public static final BatchCommand RUNPARM_PROOF_ASST_HIGHLIGHTING_ENABLED
public static final BatchCommand RUNPARM_PROOF_ASST_HIGHLIGHTING_STYLE
public static final BatchCommand RUNPARM_PROOF_ASST_FOREGROUND_COLOR_RGB
public static final BatchCommand RUNPARM_PROOF_ASST_BACKGROUND_COLOR_RGB
public static final BatchCommand RUNPARM_PROOF_ASST_FONT_FAMILY
public static final BatchCommand RUNPARM_PROOF_ASST_FONT_BOLD
public static final BatchCommand RUNPARM_PROOF_ASST_LINE_SPACING
public static final BatchCommand RUNPARM_PROOF_ASST_FONT_SIZE
public static final BatchCommand RUNPARM_PROOF_ASST_LINE_WRAP
public static final BatchCommand RUNPARM_PROOF_ASST_TEXT_COLUMNS
public static final BatchCommand RUNPARM_PROOF_ASST_TEXT_ROWS
public static final BatchCommand RUNPARM_PROOF_ASST_MAXIMIZED
public static final BatchCommand RUNPARM_PROOF_ASST_TEXT_AT_TOP
public static final BatchCommand RUNPARM_PROOF_ASST_INCOMPLETE_STEP_CURSOR
public static final BatchCommand RUNPARM_PROOF_ASST_ERROR_MESSAGE_ROWS
public static final BatchCommand RUNPARM_PROOF_ASST_ERROR_MESSAGE_COLUMNS
public static final BatchCommand RUNPARM_PROOF_ASST_FORMULA_LEFT_COL
public static final BatchCommand RUNPARM_PROOF_ASST_FORMULA_RIGHT_COL
public static final BatchCommand RUNPARM_PROOF_ASST_RPN_PROOF_LEFT_COL
public static final BatchCommand RUNPARM_PROOF_ASST_RPN_PROOF_RIGHT_COL
@Deprecated public static final BatchCommand RUNPARM_PROOF_ASST_MAX_UNIFY_ALTERNATES
@Deprecated public static final BatchCommand RUNPARM_PROOF_ASST_MAX_UNIFY_HINTS
@Deprecated public static final BatchCommand RUNPARM_PROOF_ASST_UNIFY_HINTS_IN_BATCH
public static final BatchCommand RUNPARM_STEP_SELECTOR_MAX_RESULTS
public static final BatchCommand RUNPARM_STEP_SELECTOR_SHOW_SUBSTITUTIONS
public static final BatchCommand RUNPARM_STEP_SELECTOR_DIALOG_PANE_WIDTH
public static final BatchCommand RUNPARM_STEP_SELECTOR_DIALOG_PANE_HEIGHT
public static final BatchCommand RUNPARM_PROOF_ASST_ASSRT_LIST_FREESPACE
public static final BatchCommand RUNPARM_PROOF_ASST_OUTPUT_CURSOR_INSTRUMENTATION
public static final BatchCommand RUNPARM_PROOF_ASST_AUTO_REFORMAT
public static final BatchCommand RUNPARM_PROOF_ASST_UNDO_REDO_ENABLED
@Deprecated public static final BatchCommand RUNPARM_PROOF_ASST_DUMMY_VAR_PREFIX
public static final BatchCommand RUNPARM_PROOF_ASST_DEFAULT_FILE_NAME_SUFFIX
public static final BatchCommand RUNPARM_PROOF_ASST_PROOF_FOLDER
public static final BatchCommand RUNPARM_PROOF_ASST_STARTUP_PROOF_WORKSHEET
public static final BatchCommand RUNPARM_RECHECK_PROOF_ASST_USING_PROOF_VERIFIER
public static final BatchCommand RUNPARM_RUN_PROOF_ASST_GUI
public static final BatchCommand RUNPARM_PROOF_ASST_EXPORT_TO_FILE
public static final BatchCommand RUNPARM_PROOF_ASST_OPTIMIZE_THEOREM_SEARCH
public static final BatchCommand RUNPARM_PROOF_ASST_USE_AUTOTRANSFORMATIONS
public static final BatchCommand RUNPARM_PROOF_ASST_BATCH_TEST
public static final BatchCommand RUNPARM_STEP_SELECTOR_BATCH_TEST
public static final BatchCommand RUNPARM_PREPROCESS_REQUEST_BATCH_TEST
@Deprecated public static final BatchCommand RUNPARM_SET_MM_DEFINITIONS_CHECK
public static final BatchCommand RUNPARM_PROOF_ASST_UNIFY_SEARCH_EXCLUDE
public static final BatchCommand RUNPARM_PROOF_ASST_EXCLUDE_DISCOURAGED
public static final BatchCommand RUNPARM_TMFF_DEFINE_SCHEME
public static final BatchCommand RUNPARM_TMFF_DEFINE_FORMAT
public static final BatchCommand RUNPARM_TMFF_USE_FORMAT
public static final BatchCommand RUNPARM_TMFF_ALT_FORMAT
public static final BatchCommand RUNPARM_TMFF_USE_INDENT
public static final BatchCommand RUNPARM_TMFF_ALT_INDENT
public static final BatchCommand RUNPARM_DEFINE_WORK_VAR_TYPE
public static final BatchCommand RUNPARM_DECLARE_WORK_VARS
public static final BatchCommand RUNPARM_SVC_FOLDER
public static final BatchCommand RUNPARM_SVC_CALLBACK_CLASS
public static final BatchCommand RUNPARM_SVC_ARG
public static final BatchCommand RUNPARM_SVC_CALL
public static final BatchCommand RUNPARM_GMFF_EXPORT_PARMS
public static final BatchCommand RUNPARM_GMFF_USER_TEXT_ESCAPES
public static final BatchCommand RUNPARM_GMFF_USER_EXPORT_CHOICE
public static final BatchCommand RUNPARM_GMFF_INITIALIZE
public static final BatchCommand RUNPARM_GMFF_PARSE_METAMATH_TYPESET_COMMENT
public static final BatchCommand RUNPARM_GMFF_EXPORT_FROM_FOLDER
public static final BatchCommand RUNPARM_GMFF_EXPORT_THEOREM
public static final boolean RUNPARM_MACRO_ENABLED_DEFAULT
public static final BatchCommand RUNPARM_MACRO_ENABLED
public static final BatchCommand RUNPARM_MACRO_FOLDER
public static final BatchCommand RUNPARM_MACRO_LANGUAGE
public static final BatchCommand RUNPARM_RUN_MACRO_INIT
public static final BatchCommand RUNPARM_RUN_MACRO
public static final BatchCommand RUNPARM_SET_SETTINGS_FILE
public static final BatchCommand RUNPARM_DISABLE_SETTINGS
public static final BatchCommand RUNPARM_LOAD_SETTINGS
public static final BatchCommand RUNPARM_SAVE_SETTINGS
public static final BatchCommand RUNPARM_THEOREM_LOADER_DJ_VARS_OPTION
public static final BatchCommand RUNPARM_THEOREM_LOADER_MMT_FOLDER
public static final BatchCommand RUNPARM_THEOREM_LOADER_AUDIT_MESSAGES
public static final BatchCommand RUNPARM_LOAD_THEOREMS_FROM_MMT_FOLDER
public static final BatchCommand RUNPARM_EXTRACT_THEOREM_TO_MMT_FOLDER
public static final BatchCommand RUNPARM_UNIFY_PLUS_STORE_IN_LOG_SYS_AND_MMT_FOLDER
public static final BatchCommand RUNPARM_UNIFY_PLUS_STORE_IN_MMT_FOLDER
public static final BatchCommand RUNPARM_THEOREM_LOADER_STORE_FORMULAS_ASIS
public static final BatchCommand RUNPARM_THEOREM_LOADER_STORE_MM_INDENT_AMT
public static final BatchCommand RUNPARM_THEOREM_LOADER_STORE_MM_RIGHT_COL
public static final int THEOREM_LOADER_BOSS_FILE_BUFFER_SIZE
public static final java.lang.String RUNPARM_OPTION_VALUE_ALL
public static final java.lang.String RUNPARM_OPTION_VALUE_BASIC
public static final java.lang.String RUNPARM_OPTION_VALUE_COMPLETE
public static final java.lang.String RUNPARM_OPTION_FILE_OUT_NEW
public static final java.lang.String RUNPARM_OPTION_FILE_OUT_UPDATE
public static final java.lang.String OPTION_FILE_OUT_USAGE_DEFAULT
public static final int MAX_STATEMENT_PRINT_COUNT_DEFAULT
public static final java.lang.String RUNPARM_OPTION_YES
public static final java.lang.String RUNPARM_OPTION_YES_ABBREVIATED
public static final java.lang.String RUNPARM_OPTION_NO
public static final java.lang.String RUNPARM_OPTION_NO_ABBREVIATED
public static final java.lang.String RUNPARM_OPTION_ON
public static final java.lang.String RUNPARM_OPTION_OFF
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_EXPORT_UNIFIED
Means that Ref (statement labels) should be included on exported derivation proof steps.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_EXPORT_UN_UNIFIED
Means that Ref (statement labels) should NOT be included on exported derivation proof steps. This is the default.
@Deprecated public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_NOT_RANDOMIZED
This option is deprecated and means the same as HypsOrder.Correct
.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_CORRECT
This option has the same meaning as notrandomized above
Means that logical hypotheses should be left in the original order.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_REVERSE
Means that logical hypotheses should be emitted in reverse order.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_HALF_REVERSE
Means that the first half of logical hypotheses should be emitted in canonical order, but the second part should be emitted in reverse order.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_AUTOCOMPLETE
Means that logical hypotheses list should be empty and autocompleted by autocomplete feature.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_SOME_ORDER
Means that the logical hypotheses should be emitted in some order, depending on current debug goals. The order is not fixed and this option should be used for preformance experements.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_PRINT
Means that an extra copy of the Proof Worksheet should be sent to the SystemOutputFile (or System.out). The print copy sent by ProofAsstBatchTest is the after-unification version, with the generated RPN proof, if available. exported proof steps.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_DERIVE_FORMULAS
Exported non-Qed derivation steps are output without formulas, leaving it up to the Proof Unifier to "Derive" the formulas.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_COMPARE_DJS
Compares generated DjVars pairs after unification with the input .mm file's for the theorem.
public static final java.lang.String RUNPARM_OPTION_PROOF_ASST_UPDATE_DJS
Updates generated DjVars pairs after unification.
public static final java.lang.String RUNPARM_OPTION_ASCII_RETEST
Re-unifies the output Proof Worksheet after unification.
public static final java.lang.String RUNPARM_OPTION_INHERIT
public static final int OUTPUT_VERBOSITY_DEFAULT
public static final java.lang.String RUNPARM_OPTION_ERASE_AND_REDERIVE_FORMULAS
public static final java.lang.String RUNPARM_OPTION_MACRO_LANGUAGE
public static final java.lang.String RUNPARM_OPTION_MACRO_EXTENSION
public static final java.lang.String RUNPARM_OPTION_INIT_MACRO
public static final java.lang.String RUNPARM_OPTION_PREP_MACRO
public static final ErrorCode ERRMSG_RUNPARM_FILE_EMPTY
public static final ErrorCode ERRMSG_RUNPARM_NEXT_AFTER_EOF
public static final ErrorCode ERRMSG_RUNPARM_FILE_NOT_FOUND
public static final ErrorCode ERRMSG_PARSER_LINE_EMPTY
public static final ErrorCode ERRMSG_PARSER_INPUT_STRING_NULL
public static final ErrorCode ERRMSG_UNMATCHED_QUOTE_CHAR
public static final ErrorCode ERRMSG_MISSING_DELIM
public static final ErrorCode ERRMSG_PARSER_LINE_ALREADY_REACHED
public static final ErrorCode ERRMSG_RUNPARM_FILE_BOGUS_1
public static final ErrorCode ERRMSG_RUNPARM_COMMENT_CAPTION
public static final ErrorCode ERRMSG_RUNPARM_EXECUTABLE_CAPTION
public static final ErrorCode ERRMSG_RUNPARM_NAME_INVALID
public static final ErrorCode ERRMSG_FILE_USAGE_ERR_EXISTS
public static final ErrorCode ERRMSG_FILE_UPDATE_NOT_ALLOWED
public static final ErrorCode ERRMSG_FILE_MISC_ERROR
public static final ErrorCode ERRMSG_FILE_NAME_BLANK
public static final ErrorCode ERRMSG_FILE_USAGE_PARM_UNRECOG
public static final ErrorCode ERRMSG_FILE_CHARSET_INVALID
public static final ErrorCode ERRMSG_FILE_CHARSET_UNSUPPORTED
public static final ErrorCode ERRMSG_RUNPARM_NOT_ENOUGH_FIELDS
public static final ErrorCode ERRMSG_RUNPARM_NBR_FORMAT_ERROR
public static final ErrorCode ERRMSG_RUNPARM_NBR_LE_ZERO
public static final ErrorCode ERRMSG_RUNPARM_STMT_NOT_THEOREM
public static final ErrorCode ERRMSG_RUNPARM_STMT_LABEL_BLANK
public static final ErrorCode ERRMSG_RUNPARM_STMT_LABEL_NOTFND
public static final ErrorCode ERRMSG_RUNPARM_FLOAT_FORMAT_ERROR
public static final ErrorCode ERRMSG_FOLDER_NAME_BLANK
public static final ErrorCode ERRMSG_NOT_A_FOLDER
public static final ErrorCode ERRMSG_FOLDER_NOTFND
public static final ErrorCode ERRMSG_FOLDER_MISC_ERROR
public static final ErrorCode ERRMSG_BAD_YES_NO_PARM
public static final ErrorCode ERRMSG_BAD_ON_OFF_PARM
public static final ErrorCode ERRMSG_FILE_NOTFND
public static final ErrorCode ERRMSG_FILE_READ_NOT_ALLOWED
public static final ErrorCode ERRMSG_RUNPARM_NONBLANK_PRINT_STR_BAD
public static final ErrorCode ERRMSG_NOT_A_FILE
public static final ErrorCode ERRMSG_BAD_FILE_NAME_SUFFIX
public static final ErrorCode ERRMSG_RUNPARM_NBR_LT_ZERO
public static final ErrorCode ERRMSG_RUNPARM_RGB_FORMAT
public static final ErrorCode ERRMSG_BOOLEAN_UNRECOG
public static final ErrorCode ERRMSG_PARSE_RPN
public static final ErrorCode ERRMSG_RUNPARM_PARSER_BAD_CLASS
public static final ErrorCode ERRMSG_MM_FILE_NOT_LOADED
public static final ErrorCode ERRMSG_LOAD_ENDPOINT_LABEL_BLANK
public static final ErrorCode ERRMSG_PROVABLE_TYP_CD_BOGUS
public static final ErrorCode ERRMSG_LOGIC_TYP_CD_BOGUS
public static final ErrorCode ERRMSG_BOOK_MANAGER_ALREADY_EXISTS
public static final ErrorCode ERRMSG_DUMP_STMT_UNRECOG_1
public static final ErrorCode ERRMSG_SYSOUT_PRINT_WRITER_IO_ERROR
public static final ErrorCode ERRMSG_SYSERR_PRINT_WRITER_IO_ERROR
public static final ErrorCode ERRMSG_BOOK_MANAGER_NOT_ENABLED
public static final ErrorCode ERRMSG_BOOK_MANAGER_SECTION_NBR_NOT_FOUND
public static final ErrorCode ERRMSG_PA_REQUIRES_GRAMMAR_INIT
public static final ErrorCode ERRMSG_SELECTOR_MISSING
public static final ErrorCode ERRMSG_SELECTOR_NOT_A_STMT
public static final ErrorCode ERRMSG_SELECTOR_NOT_A_THEOREM
public static final ErrorCode ERRMSG_EXPORT_RANDOMIZED_PARM_UNRECOG
public static final java.lang.String PROOF_ASST_FONT_FAMILY_LIST_CAPTION
public static final ErrorCode ERRMSG_PREPROCESS_OPTION_UNRECOG
public static final ErrorCode ERRMSG_MISC_IO_ERROR
public static final ErrorCode ERRMSG_RUNPARM_PA_STYLE_UNKNOWN
public static final ErrorCode ERRMSG_TMFF_REQUIRES_GRAMMAR_INIT
public static final ErrorCode ERRMSG_IGNORING_VERIFY_PROOF_RUNPARM
public static final ErrorCode ERRMSG_WV_MGR_REQUIRES_GRAMMAR_INIT
public static final ErrorCode ERRMSG_SVC_CALLBACK_CLASS_INIT_ERROR
public static final ErrorCode ERRMSG_SVC_CALLBACK_CLASS_CAST_ERROR
public static final ErrorCode ERRMSG_SVC_ARG_ERROR
public static final ErrorCode ERRMSG_SVC_CALL_PROOF_ASST_MISSING
public static final ErrorCode ERRMSG_SVC_CALL_THEOREM_LOADER_MISSING
public static final ErrorCode ERRMSG_MERGE_SORTED_LISTS_DUP_ERROR
public static final ErrorCode ERRMSG_THEOREM_LOADER_READER_ERROR
public static final ErrorCode ERRMSG_GMFF_INITIALIZATION_ERROR
public static final ErrorCode ERRMSG_GMFF_PROOF_ASST_MISSING
public static final ErrorCode ERRMSG_GMFF_RUNPARM_ERROR
public static final ErrorCode ERRMSG_FAIL_POPUP_WINDOW_ARGUMENT
public static final ErrorCode ERRMSG_TEST_OPTION_ARGUMENT
public static final ErrorCode ERRMSG_PATH_INVALID
public static final ErrorCode ERRMSG_PATH_SECURITY_ERROR
public static final ErrorCode ERRMSG_MACRO_LANGUAGE_MISSING
public static final java.lang.String ERRMSG_MACRO_LANGUAGE_MISSING_2
public static final ErrorCode ERRMSG_MACRO_LANGUAGE_DEFAULT_MISSING
public static final ErrorCode ERRMSG_PREP_MACRO_DOES_NOT_EXIST
public static final ErrorCode ERRMSG_CALLBACK_ERROR
public static final ErrorCode ERRMSG_LOAD_FAILED
public static final ErrorCode ERRMSG_SAVE_FAILED
public static final java.lang.String DUMP_LOGSYS_COUNTS
public static final java.lang.String DUMP_PROVABLE_TYP_SET
public static final java.lang.String DUMP_LOGIC_TYP_SET
public static final java.lang.String DUMP_VARHYP_TYP_SET
public static final java.lang.String DUMP_SYNTAX_AXIOM_TYP_SET
public static final java.lang.String DUMP_NULLS_PERMITTED_TYP_SET
public static final java.lang.String DUMP_LOGSYS_SYM_TBL
public static final int DUMP_GRAMMAR_RULE_MAX_PRINT
public static final java.lang.String DUMP_NULLS_PERMITTED_LIST
public static final java.lang.String DUMP_TYPE_CONVERSION_LIST
public static final java.lang.String DUMP_NOTATION_LIST
public static final java.lang.String DUMP_LOGSYS_STMT_TBL
public static final java.lang.String DUMP_LOGICAL_SYSTEM
public static final java.lang.String DUMP_START
public static final java.lang.String DUMP_END
public static final java.lang.String DUMP_SYM_TBL_SIZE
public static final java.lang.String DUMP_STMT_TBL_SIZE
public static final java.lang.String DUMP_SYM_TBL
public static final java.lang.String DUMP_SYM_TBL_UNDERSCORE
public static final java.lang.String DUMP_SYM_TBL_IS_EMPTY
public static final java.lang.String DUMP_STMT_TBL
public static final java.lang.String DUMP_STMT_TBL_UNDERSCORE
public static final java.lang.String DUMP_STMT_TBL_IS_EMPTY
public static final java.lang.String DUMP_OF_FIRST
public static final java.lang.String DUMP_THEOREM
public static final java.lang.String DUMP_OPT_FRAME_HYP_ARRAY
public static final java.lang.String DUMP_OPT_FRAME_DJ_VARS
public static final java.lang.String DUMP_START_BRACKET
public static final java.lang.String DUMP_END_BRACKET
public static final char DUMP_COMMA
public static final java.lang.String DUMP_PROOF
public static final java.lang.String DUMP_PROOF_MISSING_STEP
public static final java.lang.String DUMP_AXIOM
public static final java.lang.String DUMP_VARHYP_RESEQ
public static final java.lang.String DUMP_AXIOM_UNIQUE_CNST
public static final java.lang.String DUMP_LOGHYP
public static final java.lang.String DUMP_VARHYP
public static final java.lang.String DUMP_MAND_FRAME_HYP_ARRAY
public static final java.lang.String DUMP_MAND_FRAME_DJ_VARS
public static final java.lang.String DUMP_TYP
public static final java.lang.String DUMP_IS_ACTIVE
public static final java.lang.String DUMP_IS_ASSRT
public static final java.lang.String DUMP_IS_HYP
public static final java.lang.String DUMP_IS_CNST
public static final java.lang.String DUMP_MAND_VARHYP_ARRAY
public static final java.lang.String DUMP_FORMULA
public static final java.lang.String DUMP_EXPR_RPN
public static final java.lang.String DUMP_VAR
public static final java.lang.String DUMP_ACTIVE_VARHYP
public static final java.lang.String DUMP_CNST
public static final java.lang.String DUMP_IS_VAR_TYP
public static final java.lang.String DUMP_IS_GRAMMATICAL_TYP
public static final java.lang.String DUMP_IS_PROVABLE_TYP
public static final java.lang.String DUMP_IS_LOGIC_TYP
public static final java.lang.String DUMP_IS_SYNTAX_AXIOM_TYP
public static final java.lang.String DUMP_LEN1_CNST_RULE_NBR
public static final java.lang.String DUMP_LEN1_CNST_AXIOM
public static final java.lang.String DUMP_EARLEY_FIRST
public static final java.lang.String DUMP_RULE_COLLECTION
public static final java.lang.String DUMP_RULE_COLLECTION_UNDERSCORE
public static final java.lang.String DUMP_RULE_COLLECTION_IS_EMPTY
public static final java.lang.String DUMP_GRAMMAR_RULE
public static final java.lang.String DUMP_RULE_NBR
public static final java.lang.String DUMP_TYPE_CODE
public static final java.lang.String DUMP_MAX_SEQ_NBR
public static final java.lang.String DUMP_NBR_HYP_PARAMS_USED
public static final java.lang.String DUMP_PARAM_TREE_AS_RPN
public static final java.lang.String DUMP_PARAM_VARHYP_NODE_ARRAY
public static final java.lang.String DUMP_NOTATION_RULE
public static final int DUMP_NOTATION_LABEL_PADIT
public static final int DUMP_NOTATION_RULE_NBR_PADIT
public static final int DUMP_NOTATION_RULE_TYP_PADIT
public static final java.lang.String DUMP_GRAMMAR_RULE_REPLACEMENT_SYMBOL
public static final java.lang.String DUMP_RULE_CONTINUATION_LIT
public static final java.lang.String DUMP_RULE_COLON
public static final java.lang.String DUMP_IS_GIMME_MATCH_NBR
public static final java.lang.String DUMP_TYPE_CONVERSION_RULE
public static final java.lang.String DUMP_RIGHT_ARROW
public static final java.lang.String DUMP_NULLS_PERMITTED_RULE
public static final java.lang.String DUMP_THE_GRAMMAR
public static final java.lang.String DUMP_THE_GRAMMAR_UNDERSCORE
public static final java.lang.String DUMP_THE_GRAMMAR_IS_EMPTY
public static final java.lang.String DUMP_BM_CNST
public static final java.lang.String DUMP_BM_VAR
public static final java.lang.String DUMP_BM_VARHYP
public static final java.lang.String DUMP_BM_LOGHYP
public static final java.lang.String DUMP_BM_AXIOM
public static final java.lang.String DUMP_BM_THEOREM
public static final java.lang.String DUMP_BM_UNKNOWN
public static final java.lang.String DUMP_BM_DOT
public static final java.lang.String DUMP_BM_EQ_COL
public static final BatchCommand[] RUNPARM_LIST