Modifier and Type | Constant Field | Value |
---|---|---|
public static final char |
APPEND_FILE_NAME_ERR_CHAR_1 |
47 |
public static final char |
APPEND_FILE_NAME_ERR_CHAR_2 |
92 |
public static final char |
APPEND_FILE_NAME_ERR_CHAR_3 |
58 |
public static final java.lang.String |
CHARSET_ENCODING_ISO_8859 |
"ISO-8859-1" |
public static final int |
DEFAULT_MODEL_FILE_BUFFER_SIZE |
512 |
public static final java.lang.String |
DEFAULT_OUTPUT_FILE_NAME |
"general" |
public static final java.lang.String |
ERRMSG_TYPESET_DEFS_AUDIT_2 |
" Sym: %s Repl: %s\n" |
public static final int |
ESCAPE_PAIR_NUM_MAX |
255 |
public static final int |
ESCAPE_PAIR_NUM_MIN |
0 |
public static final int |
EXPORT_BUFFER_DEFAULT_SIZE |
4096 |
public static final java.lang.String |
EXPORT_PARM_OFF |
"OFF" |
public static final java.lang.String |
EXPORT_PARM_ON |
"ON" |
public static final java.lang.String |
EXPORT_TYPE_ALTHTML |
"althtml" |
public static final java.lang.String |
EXPORT_TYPE_HTML |
"html" |
public static final java.lang.String |
EXPORTER_AUDIT_REPORT |
"Typesetting Definitions: .mm $t keyword = %s, Number Of Defined Symbols = %d" |
public static final int |
EXPORTER_MODEL_CACHE_INIT_SIZE |
40 |
public static final char |
FILE_TYPE_DOT |
46 |
public static final java.lang.String |
INITIALIZATION_AUDIT_REPORT_2 |
" %s\n\n" |
public static final java.lang.String |
INITIALIZATION_AUDIT_REPORT_3 |
" SelectedExporter[%s]\n\n %s\n\n %s\n\n %s\n\n" |
public static final int |
METAMATH_DOLLAR_T_BUFFER_SIZE |
8192 |
public static final int |
METAMATH_DOLLAR_T_MAP_SIZE |
1500 |
public static final java.lang.String |
METAMATH_DOLLAR_T_MESSAGE_DESCRIPTOR |
"Metamath $t Comment" |
public static final java.lang.String |
MODEL_A |
"A" |
public static final java.lang.String |
MODEL_A_COMMENT0_NAME |
"AO-comment0.txt" |
public static final java.lang.String |
MODEL_A_COMMENT1X_NAME |
"AO-comment1X.txt" |
public static final java.lang.String |
MODEL_A_COMMENT2_NAME |
"AO-comment2.txt" |
public static final java.lang.String |
MODEL_A_DISTINCTVAR0_NAME |
"AO-distinctvar0.txt" |
public static final java.lang.String |
MODEL_A_DISTINCTVAR1X_NAME |
"AO-distinctvar1X.txt" |
public static final java.lang.String |
MODEL_A_DISTINCTVAR2_NAME |
"AO-distinctvar2.txt" |
public static final java.lang.String |
MODEL_A_DISTINCTVAR3X_NAME |
"AO-distinctvar3X.txt" |
public static final java.lang.String |
MODEL_A_DISTINCTVAR4_NAME |
"AO-distinctvar4.txt" |
public static final java.lang.String |
MODEL_A_FILE0_NAME |
"AM-file0.txt" |
public static final java.lang.String |
MODEL_A_FILE2_NAME |
"AM-file2.txt" |
public static final java.lang.String |
MODEL_A_FOOTER0_NAME |
"AO-footer0.txt" |
public static final java.lang.String |
MODEL_A_GENPROOF0_NAME |
"AO-genproof0.txt" |
public static final java.lang.String |
MODEL_A_GENPROOF1X_NAME |
"AO-genproof1X.txt" |
public static final java.lang.String |
MODEL_A_GENPROOF2_NAME |
"AO-genproof2.txt" |
public static final java.lang.String |
MODEL_A_HEADER0_NAME |
"AO-header0.txt" |
public static final java.lang.String |
MODEL_A_HEADER1X_NAME |
"AO-header1X.txt" |
public static final java.lang.String |
MODEL_A_HEADER2_NAME |
"AO-header2.txt" |
public static final java.lang.String |
MODEL_A_HEADER3X_NAME |
"AO-header3X.txt" |
public static final java.lang.String |
MODEL_A_HEADER4_NAME |
"AO-header4.txt" |
public static final java.lang.String |
MODEL_A_HEADER5X_NAME |
"AO-header5X.txt" |
public static final java.lang.String |
MODEL_A_HEADER6_NAME |
"AO-header6.txt" |
public static final java.lang.String |
MODEL_A_HEADER7_NAME |
"AO-header7.txt" |
public static final java.lang.String |
MODEL_A_STEP0_NAME |
"AM-step0.txt" |
public static final java.lang.String |
MODEL_A_STEP1X_NAME |
"AM-step1X.txt" |
public static final java.lang.String |
MODEL_A_STEP2_NAME |
"AM-step2.txt" |
public static final java.lang.String |
MODEL_A_STEP3X_NAME |
"AM-step3X.txt" |
public static final java.lang.String |
MODEL_A_STEP4_NAME |
"AM-step4.txt" |
public static final java.lang.String |
MODEL_ERROR_MESSAGE_DESCRIPTOR |
"Model" |
public static final java.lang.String |
OPTION_VALUE_ALL |
"*" |
public static final char |
OUTPUT_FILE_NAME_ERR_CHAR_1 |
47 |
public static final char |
OUTPUT_FILE_NAME_ERR_CHAR_2 |
92 |
public static final char |
OUTPUT_FILE_NAME_ERR_CHAR_3 |
58 |
public static final java.lang.String |
PRINT_TYPESETTING_DEFINITIONS |
"PrintTypesettingDefinitions" |
public static final int |
PROOF_WORKSHEET_BUFFER_SIZE |
8192 |
public static final java.lang.String |
PROOF_WORKSHEET_MESSAGE_DESCRIPTOR |
"Proof Worksheet" |
public static final java.lang.String |
RUNPARM_PRINT_OPTION |
"PRINT" |
public static final java.lang.String |
USER_EXPORT_CHOICE_ALL |
"ALL" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
NS |
"GM" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final int |
ALLOC_NBR_BOOK_CHAPTERS_INITIAL |
50 |
public static final int |
ALLOC_NBR_BOOK_SECTIONS_INITIAL |
1500 |
public static final boolean |
BOOK_MANAGER_ENABLED_DEFAULT |
true |
public static final java.lang.String |
CHAPTER_TOSTRING_LITERAL |
"Chapter %d -- %s -- Sections %d thru %d" |
public static final java.lang.String |
CNST_SET_TYPE |
"set" |
public static final byte |
COMPRESS_ERROR_CHAR_VALUE |
-1 |
public static final int |
COMPRESS_HIGH_BASE |
5 |
public static final int |
COMPRESS_LOW_BASE |
20 |
public static final int |
COMPRESS_OTHER_STMT_INIT_LEN |
500 |
public static final byte |
COMPRESS_REPEAT_CHAR |
90 |
public static final byte |
COMPRESS_REPEAT_CHAR_VALUE |
-2 |
public static final int |
COMPRESS_REPEATED_SUBPROOF_INIT_LEN |
500 |
public static final int |
COMPRESS_STEP_INIT_LEN |
20000 |
public static final byte |
COMPRESS_UNKNOWN_CHAR |
63 |
public static final byte |
COMPRESS_UNKNOWN_CHAR_VALUE |
-3 |
public static final java.lang.String |
DJVARS_LEFT_BRACKET |
"<" |
public static final java.lang.String |
DJVARS_RIGHT_BRACKET |
">" |
public static final java.lang.String |
DJVARS_SEPARATOR |
"," |
public static final java.lang.String |
ERRMSG_APPENDED_CAPTION |
"Appended" |
public static final java.lang.String |
ERRMSG_INSERTED_CAPTION |
"Inserted" |
public static final java.lang.String |
ERRMSG_LOGHYP_CAPTION |
"LogHyp" |
public static final java.lang.String |
ERRMSG_THEOREM_CAPTION |
"Theorem" |
public static final int |
MAX_ERROR_MESSAGES_DEFAULT |
15000 |
public static final int |
MAX_INFO_MESSAGES_DEFAULT |
15000 |
public static final java.lang.String |
MISSING_PROOF_STEP |
"?" |
public static final int |
NBR_WORK_VARS_FOR_TYPE_MAX |
999 |
public static final int |
NBR_WORK_VARS_FOR_TYPE_MIN |
10 |
public static final int |
SECTION_LOGIC_CD |
4 |
public static final int |
SECTION_NBR_CATEGORIES |
4 |
public static final int |
SECTION_SYM_CD |
1 |
public static final int |
SECTION_SYNTAX_CD |
3 |
public static final java.lang.String |
SECTION_TOSTRING_LITERAL |
"Chapter %d, Section %d %s -- %s -- Last MObj Nbr = %d" |
public static final int |
SECTION_VAR_HYP_CD |
2 |
public static final int |
SEQ_ASSIGNER_INTERVAL_SIZE_DEFAULT |
1000 |
public static final int |
SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_DEFAULT |
100 |
public static final int |
SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_MAX |
10000 |
public static final int |
SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_MIN |
10 |
public static final int |
SEQ_ASSIGNER_MAX_INTERVAL_SIZE |
10000 |
public static final int |
SEQ_ASSIGNER_MIN_INTERVAL_SIZE |
1 |
public static final int |
STARTING_WORK_VAR_SEQ_NBR_FOR_MOBJ |
-2147483648 |
public static final int |
STMT_TBL_INITIAL_SIZE_DEFAULT |
45000 |
public static final int |
STMT_TBL_INITIAL_SIZE_MINIMUM |
100 |
public static final int |
SYM_TBL_INITIAL_SIZE_DEFAULT |
1500 |
public static final int |
SYM_TBL_INITIAL_SIZE_MINIMUM |
10 |
public static final int |
WORK_VAR_DEFAULT_NBR_FOR_TYP_CD |
200 |
public static final java.lang.String |
WORK_VAR_DEFAULT_PREFIX |
"&" |
public static final int |
WV_OCCURS_IN_ERROR |
1 |
public static final int |
WV_OCCURS_IN_NOT_AT_ALL |
0 |
public static final int |
WV_OCCURS_IN_RENAME_LOOP |
-1 |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
NS |
"LA" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
CHAPTER_ID_STRING |
"#*#*" |
public static final java.lang.String |
DEFAULT_TITLE |
"Default Title" |
public static final java.lang.String |
ERRMSG_TXT_KEYWORD |
" Keyword = " |
public static final java.lang.String |
ERRMSG_TXT_LABEL |
" Label = " |
public static final byte |
FILE_NAME |
16 |
public static final byte |
LABEL |
4 |
public static final boolean |
LOAD_COMMENTS_DEFAULT |
true |
public static final boolean |
LOAD_PROOFS_DEFAULT |
true |
public static final byte |
MATH_SYMBOL |
8 |
public static final java.lang.String |
MISSING_PROOF_STEP |
"?" |
public static final java.lang.String |
MM_AXIOMATIC_ASSRT_KEYWORD |
"$a" |
public static final java.lang.String |
MM_BEGIN_COMMENT_KEYWORD |
"$(" |
public static final char |
MM_BEGIN_COMPRESSED_PROOF_LIST_CHAR |
40 |
public static final java.lang.String |
MM_BEGIN_FILE_KEYWORD |
"$[" |
public static final java.lang.String |
MM_BEGIN_SCOPE_KEYWORD |
"${" |
public static final java.lang.String |
MM_CNST_KEYWORD |
"$c" |
public static final java.lang.String |
MM_DJ_VAR_KEYWORD |
"$d" |
public static final java.lang.String |
MM_END_COMMENT_KEYWORD |
"$)" |
public static final char |
MM_END_COMPRESSED_PROOF_LIST_CHAR |
41 |
public static final java.lang.String |
MM_END_FILE_KEYWORD |
"$]" |
public static final java.lang.String |
MM_END_SCOPE_KEYWORD |
"$}" |
public static final java.lang.String |
MM_END_STMT_KEYWORD |
"$." |
public static final char |
MM_END_STMT_KEYWORD_CHAR |
46 |
public static final char |
MM_KEYWORD_1ST_CHAR |
36 |
public static final java.lang.String |
MM_LABEL_IN_COMMENT_ESCAPE_STRING |
"~" |
public static final java.lang.String |
MM_LOG_HYP_KEYWORD |
"$e" |
public static final java.lang.String |
MM_PROVABLE_ASSRT_KEYWORD |
"$p" |
public static final java.lang.String |
MM_START_PROOF_KEYWORD |
"$=" |
public static final java.lang.String |
MM_VAR_HYP_KEYWORD |
"$f" |
public static final java.lang.String |
MM_VAR_KEYWORD |
"$v" |
public static final byte |
PRINTABLE |
1 |
public static final int |
READER_BUFFER_SIZE |
32768 |
public static final java.lang.String |
SECTION_ID_STRING |
"=-=-" |
public static final java.lang.String |
TYPESETTING_AS_LITERAL |
"as" |
public static final char |
TYPESETTING_ASTERISK_CHAR |
42 |
public static final java.lang.String |
TYPESETTING_C_COMMENT_END |
"*/" |
public static final java.lang.String |
TYPESETTING_C_COMMENT_START |
"/*" |
public static final java.lang.String |
TYPESETTING_COMMENT_ID_STRING |
"$t" |
public static final char |
TYPESETTING_DOUBLE_QUOTE_CHAR |
34 |
public static final char |
TYPESETTING_PLUS_CHAR |
43 |
public static final char |
TYPESETTING_SEMICOLON_CHAR |
59 |
public static final char |
TYPESETTING_SINGLE_QUOTE_CHAR |
39 |
public static final char |
TYPESETTING_SLASH_CHAR |
47 |
public static final byte |
WHITE_SPACE |
2 |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
NS |
"IO" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final int |
ASSRT_LIST_FREESPACE_DEFAULT |
5 |
public static final int |
ASSRT_LIST_FREESPACE_MAX |
1000 |
public static final boolean |
AUTO_REFORMAT_DEFAULT |
true |
public static final java.lang.String |
AUTO_STEP_PREFIX |
"!" |
public static final boolean |
AUTOCOMPLETE_ENABLED_DEFAULT |
true |
public static final java.lang.String |
AUTOCOMPLETE_SAMPLE_PROOF_TEXT |
"$( <MM> <PROOF_ASST> THEOREM=syllogism LOC_AFTER=\n\nh |- ( ph -> ps ) \nh |- ( ps -> ch ) \n! |- ( ph -> ( ps -> ch ) ) \n! |- ( ( ph -> ps ) -> ( ph -> ch ) ) \n!qed |- ( ph -> ch ) \n\n$)\n" |
public static final java.lang.String |
AUX_FRAME_FONT_FAMILY |
"Monospaced" |
public static final int |
AUX_FRAME_NBR_COLUMNS_DEFAULT |
80 |
public static final int |
AUX_FRAME_NBR_ROWS_DEFAULT |
25 |
public static final java.lang.String |
AUX_FRAME_TEXT_DEFAULT |
"AuxFrameGUI default text" |
public static final java.lang.String |
AUX_FRAME_TITLE_DEFAULT |
"AuxFrameGUI default title" |
public static final java.lang.String |
BACKUP_SUFFIX |
".bak" |
public static final java.lang.String |
COLOR_CHOOSE_TITLE_2 |
" -- presently = " |
public static final java.lang.String |
COLOR_CHOOSE_TITLE_SEPARATOR |
"," |
public static final java.lang.String |
COMMENT_STMT_TOKEN_PREFIX |
"*" |
public static final java.lang.String |
DEFAULT_STMT_LABEL |
"?" |
public static final boolean |
DERIVE_AUTOCOMPLETE_DEFAULT |
true |
public static final java.lang.String |
DERIVE_STEP_PREFIX |
"d" |
public static final java.lang.String |
DISTINCT_VARIABLES_STMT_TOKEN |
"$d" |
public static final java.lang.String |
DOT_STEP_CAPTION |
".Step " |
public static final java.lang.String |
DUMMY_VAR_PREFIX |
"$" |
public static final java.lang.String |
END_PROOF_STMT_TOKEN |
"$." |
public static final java.lang.String |
ERRMSG_INVALID_OPTION |
"Not a valid option; try again" |
public static final java.lang.String |
ERRMSG_TXT_COLUMN |
" Column: " |
public static final java.lang.String |
ERRMSG_TXT_LINE |
" Line: " |
public static final java.lang.String |
ERROR_TEXT_SPACER_LINE |
" --------------------------------------------------------- " |
public static final char |
FIELD_DELIMITER_COLON |
58 |
public static final char |
FIELD_DELIMITER_COMMA |
44 |
public static final int |
FIELD_ID_NONE |
-1 |
public static final int |
FIELD_ID_REF |
1 |
public static final int |
FONT_LIST_MAX_LINES |
18 |
public static final int |
FONT_LIST_STARTING_LINE_LENGTH |
70 |
public static final java.lang.String |
FOOTER_STMT_TOKEN |
"$)" |
public static final java.lang.String |
GENERAL_HELP_FRAME_TITLE |
"Proof Assistant Help: General Information, Version 2.5.3 as of 23-Sep-2019" |
public static final java.lang.String |
GENERAL_HELP_INFO_TEXT |
"The mmj2 Proof Assistant provides an easy-to-use system for creating\nMetamath proofs, but it does not provide all of the features of the\nMetamath.exe Proof Assistant. Specifically:\n\n* mmj2 does not update Metamath .mm databases.\n\n* mmj2 cannot import incomplete or invalid proofs from a Metamath database. \n\nAlso, please do not be disappointed. In spite of the point-and-click user-\nfriendliness, the fact that the mmj2 Proof Assistant uses a GUI interface\ndoes not eliminate the requirement that the user learn logic and math. Nor\ndoes it eliminate the need for deep thought, hard work or perseverance. It\nmay be that you will need to work out your proofs by hand before entering\nthem into the system.\n\n----------------------------------------------------------------------------\n\nHere are a few important facts and concepts about the mmj2 Proof Assistant\nGUI program:\n\n* A \'proof\' on the Proof Assistant GUI screen is just a big text area.\n\n* The GUI program itself is just a rudimentary text editor that knows\nnothing and retains no memory of previous interactions, except for the\ncurrent location in the database, which is used for browsing purposes.\n\n* The text on the screen is divided into two window \'panes\'. By default, the\nupper pane is the Proof Text Area, which is called a \'Proof Worksheet\' when\nproperly formatted according to the mmj2 rules. The lower window pane shows\nerror and informational messages, and its contents are duplicated in a\nseparate \'Request Messages\' window (use Alt-Tab to switch back and forth.)\n\n* The contents of the Proof Text Area can be saved to, or retrieved from an\nASCII text file.\n\n* The Theorem Loader feature (menu item \'TL\') can be used to update the\nMetamath data presently loaded in the mmj2 Logical System, and to convert a\nProof Worksheet to a Metamath formatted file, which it stores in your\ndesignated \'MMT Folder\' with file type \'.mmt\'. A theorem in the MMT Folder\nin a \'.mmt\' type file can be loaded into the Logical System even if its\nproof is incomplete (contains a \'?\') or invalid, but the Proof Asst GUI\nrequires successful proof unification for exports to the MMT Folder (you\nmay manually edit \'.mmt\' theorems in the MMT Folder.)\n\n* The Proof Worksheet format is also used by the Metamath \'eimm.exe\' program\nfor import and export of proofs to and from a Metamath database. eimm.exe\nprovides the Export command to export proofs from a Metamath .mm database to\na Proof Worksheet file -- even incomplete or invalid proofs -- and the\nImport command to read a Proof Worksheet file and store its proof into a\nMetamath .mm database.\n\n* At any point you can freely use Edit Cut, Copy and Paste to replace all or\npart of a Proof Worksheet.\n\n* The format of a Proof Worksheet satisfies the Metamath validation\nrequirements for a Metamath Comment statement, which begins with \'$(\' and\nends with \'$)\'. In fact, an mmj2 Proof Worksheet can be copied manually as a\nlarge Metamath comment directly into the text of a Metamath .mm database\n(which is ALSO an ASCII text file.)\n\n* A Proof Worksheet begins with a \'Header\' statement line, containing a \'$(\'\ntoken starting in column 1, and ends with a \'Trailer\' statement line\ncontaining a \'$)\' token starting in column 1.\n\n* \'Statements\' in a Proof Worksheet always begin in column 1 of a line on\nthe screen and continue up to the next Statement\'s start. In other words, a\nline containing a blank character in column 1 is, by definition, a\ncontinuation of the previous Proof Worksheet Statement.\n\n* A Comment Statement is denoted by an \'*\' (asterisk) in column 1.\n\n* A Proof Worksheet must contain at least one proof step Statement, the step\nlabelled \'qed\', which must be the last proof step in the Proof Worksheet.\n\n* Hypothesis proof step Statements are identified by an \'h\' in column 1,\nwith the \'h\' prefixing the Step Number.\n\n* Every proof step Statment that is not an Hypothesis step is, by\ndefinition, a Derivation proof step Statement.\n\n* Proof step numbers, except for the \'qed\' step \'number\' are positive\nintegers, but the numbers need not be in ascending order. There cannot be\nduplicate step numbers, however.\n\nThe rest of the mmj2 Proof Worksheet format requirements you can learn by\ninspection, or by reviewing the additional documentation about mmj2 and its\nProof Assistant, which can be found on the mmj2.html page within the\nmmj2.zip download file. Also, be sure to check out the interactive Proof\nAssistant Tutorial!\n\n----------------------------------------------------------------------------\n\nHere is a brief summary of the mmj2 Proof Assistant Menu Options.\n\n\n========= File Menu =========\n\n* Save Proof File -- Saves the current Proof Text Area to a text file.\n\n* New Proof -- Creates a \'skeleton\' Proof Worksheet for a new or existing\nTheorem.\n\n* New-Next Proof -- Creates a \'skeleton\' Proof Worksheet for the next\ntheorem in the input Metamath database after the current theorem\'s location.\n\n* Open Proof File -- Reads and displays a Proof Worksheet (text) file.\n\n* Get Proof -- Creates and displays a Proof Worksheet for an existing\ntheorem\'s proof in the input Metamath .mm database.\n\n* Forward-Get Proof -- Creates and displays the Proof Worksheet for the\nproof of the next theorem after the current location within the input\nMetamath .mm database. Wraps around to the start of the database after the\nend is reached.\n\n* Backward-Get Proof -- Creates and displays the Proof Worksheet for the\nproof of the theorem prior to the current location within the input Metamath\n.mm database. Wraps around to the end of the database after the start is\nreached.\n\n* Close Proof File -- Closes the current Proof Worksheet after providing an\nopportunity to save any unsaved changes.\n\n* Save As -- Saves the current Proof Worksheet to a text file after\nproviding an opportunity to change the file name.\n\n* Export Via GMFF -- GMFF (Graphics Mode Formula Formatting) exports the\nProof Worksheet as html file(s) in the \\mmj2jar\\gmff directory.\nSee \\mmj2\\doc\\GMFFDoc\\* \n\n* Exit/Quit -- Exits the Proof Assistant GUI program after providing an\nopportunity to save any unsaved changes.\n\n\n========= Edit Menu =========\n\n* Undo -- Undoes the last \'undoable edit\' made to the Proof Worksheet. Note\nthat you must Undo twice in succession following Reformat, Unification and\nperhaps other Menu functions to restore the Proof Worksheet to its previous\nstate. The first Undo in this scenario results in a blank text area, and the\nsecond Undo restores the text. We at MMJ2 Laboratories, Inc. sincerely\napologize for this sadly deficient behavior. Be assured that we will be\ncomplaining on your behalf to someone, somewhere, sometime about this shoddy\nworkmanship.\n\n* Redo -- \'Undoes\' an Undo.\n\n* Cut -- Standard text \'cut\' operation on selected text. The \'cut\' text is\ncopied to the clipboard.\n\n* Copy -- Standard text \'copy\' operation which copies the selected text to\nthe clipboard.\n\n* Paste -- Standard text \'paste\' operation which \'pastes\' the contents of the\ntext clipboard to the screen at the position of the text caret (cursor).\n\n* Set Incomplete Step Cursor -- Controls cursor positioning after Unification\nif there are no errors. \'First\' and \'Last\' mean position the cursor to the\nfirst/last incomplete step, respectively, while \'AsIs\' means do not move the\nto a different proof step. If unification is successful, or if there are no\nerrors and no incomplete proof steps, the cursor is positioned to the \'qed\'\nstep.\n\n* Set Soft Dj Vars Error Handling -- Controls program responses to missing\n$d statements on the theorem being proved. GenerateReplacements produces a\nset of $d statements to replace the existing $d statements if there are any\nsoft Dj Vars errors. GenerateDifferences produces $d statements for just\nthe missing $d statements. GenerateNew is the similar as GenerateReplacements\nexcept that new $d statements are produced even if there are no missing $d\nstatements on the theorem being proved. Also, GenerateNew does not use any of\nthe existing $d statements in the input .mm file (i.e. extraneous $d\nstatements are eliminated by GenerateNew -- a very handy feature!). Option\n\'Report\' produces detailed error messages at the proof step level for any\nsoft Dj Vars errors. Option \'Ignore\' turns off soft Dj Vars Error processing.\n\n* Set Font Family -- Dialog Box for choosing a Font. Note that only fixed\nwidth fonts display formulas with proper alignment on the screen. Also, the\nDialog box is rather primitive and requires the user to type in the name\nof the desired Font Family. \n\n* Set Font Style Bold -- Changes the Proof Worksheet text to Bold.\n\n* Set Font Style Plain -- Changes the Proof Worksheet text to not-Bold.\n\n* Larger Font Size -- Increases the Font Size.\n\n* Smaller Font Size -- Decreases the Font Size.\n\n* Set Foreground Color -- Dialog Box for selecting the foreground color of\nproof text. Note that the Title in the Dialog Box displays the RGB color\nnumbers of the current color (e.g. black = \'0,0,0\'). RGB numbers are used in\nthe mmj2 RunParms file for setting color.\n\n* Set Background Color -- Dialog Box for selecting the background color of\nproof text. Note that the Title in the Dialog Box displays the RGB color\nnumbers of the current color (e.g. white = \'0,0,0\'). RGB numbers are used in\nthe mmj2 RunParms file for setting color.\n\n* Set Format Number -- Dialog Box for choosing the TMFF Format Number to\nuse in formatting formulas. \'3\' is a good choice for use with set.mm. Note\nthat the proof is reformatted if you change the Format Number. \n\n* Set Indent -- Dialog Box for choosing the number of columns to indent each\nformula for each proof level. Note: indentation occurs only when the program\nformats or reformats a proof step -- at present, reformatting occurs when a\nWork Variable is resolved during Unification.\n\n* Reformat Proof -- Reformats the proof using the TMFF Format Number \npresently in use. This is handy for tidying up.\n\n* Reformat Proof: Swap Alt -- Toggles back and forth between the current\nFormat Number and Indent and the Alternate Format Number and Indent (set\nby RunParms TMFFAltFormat and TMFFAltIndent).\n\n\n=========== Cancel Menu ===========\n\n* Cancel (Looping? Kill it!!!) -- Cancels an ongoing Menu function, such as\nUnification. Note: most functions, inluding Unification, are so fast that\nthere is no time to \'Cancel\' before they finish. However, if something\nappears to be taking a long time, hit \'Alt+Tab\' to switch to the Command\nWindow used to start mmj2 and the Proof Assistant. In the event that a\nprogram bug is encountered, a serious-looking error message is regurgitated\non the Command Window; thus, the program may not be looping, but halted! In\nthis case, \'Cancel\' will unlock the Proof Assistant and you may be able to\ncontinue working -- but please File/Save the Proof Worksheet and include it\nwith a problem report (MMJ2 Laboratories, Inc. apologizes in advance for\nany inconveniences: We\'re sorry, our bad!)\n\n\n===== Unify Menu =====\n\n* Unify (check proof) -- Validates the Proof Worksheet and ensures that the\n\'qed\' step is correctly derived via \'unifications\' with existing assertions\nin the input Metamath .mm database. FYI, the term \'unification\' refers to\nthe process of making sure that a derivation step\'s formula and hypotheses\nmatch the pattern of a given assertion and its hypotheses. By \'match\' we\nmean that there exists a consistent set of substitutions that, when\nsimultaneously substituted for the corresponding variables of the referenced\nassertion, the derivation step\'s formulas and hypotheses are exactly\nreproduced. The term \'consistent\' means if variable \'x\' occurs in more than\none place in the referenced assertion and its hypotheses, that the same\nsubstitution is made to every occurrence of \'x\'. If the \'qed\' step is\nsuccessfully unified and no other errors are encountered, the Proof\nAssistant generates a Metamath RPN-format proof which can be copied into the\ninput Metamath .mm database text file. Note: extraneous derivation steps are\nallowed but are not included in the generated RPN proof.\n\n* Unify+Renumber -- Same as \'Unify (check proof)\', but in addition, the step\nnumbers are renumbered from 1, by 1.\n\n* Unify+Erase and Rederive Formulas -- Same as \'Unify (check proof)\', but\nbefore the unification process begins the formula is erased on every\nnon-qed Derivation Step which has a Ref label; if there are no errors\nthe \'Derive\' feature will rederive the formulas.\n\n* Step Selector Search -- Displays Step Selector Dialog screen for the proof\nstep on which the input cursor is located. For maximum speed double-click\nany Derivation proof step to invoke Step Selector Search. Provides list of\nassertions which can be unified with the indicated step and its hypotheses.\nAdd a \'?\' to the step\'s hypotheses to indicate that zero or more additional\nhypotheses are acceptable. When an assertion is selected on the dialog screen\nthe label of the assertion is text-edited by the program into the proof\nstep\'s Ref field, and then the standard Unification process is performed.\n\n* Reshow Step Selector Dialog -- redisplays the dialog, just as it was. This\nfeature enables the user to Undo the last unification (Ctrl-Z twice), then\npress Ctrl-9 to Reshow the Step Selector Dialog and make another selection.\n\n* Set Step Selector Max Results -- limits the number of assertions returned\nby the Step Selector Search.\n\n* Set Step Selector Show Substitutions -- true/false option to display, or\nnot, substitutions from the proof into unifiable assertions (default = true).\nIf false, assertions are displayed as they appear in the input .mm\nfile.\n\n\n===== TL Menu (Theorem Loader) =====\n\n* Unify + Store In LogSys and MMT Folder -- Validates the Proof Worksheet,\nand if proof unification is successful, writes the theorem to the MMT Folder\nand stores it in the Logical System in memory.\n\n* Unify + Store In MMT Folder -- Validates the Proof Worksheet, and if proof\nunification is successful, writes the theorem to the MMT Folder.\n\n* Load Theorems From MMT Folder -- Loads every theorem file suffixed with\n\'.mmt\' in the MMT Folder into the Logical System in memory.\n\n* Extract Theorem To MMT Folder -- Exports a theorem in the Logical System\nto the MMT Folder. The output file name is the theorem label suffixed with\n\'.mmt\'.\n\n* Verify All Proofs -- Runs the Metamath Proof Verification algorithm against\nevery theorem in the Logical System in memory. This is particularly useful if\nthe Theorem Loader has been used to update $d restrictions for an existing\ntheorem.\n\n* Set Theorem Loader MMT Folder -- Designates the folder used by the Theorem\nLoader for input/output of \'.mmt\' theorem files.\n\n* Set Theorem Loader Dj Vars Option -- Specifies whether the Theorem Loader\nshould \'Merge\', \'Replace\' or \'NoUpdate\' $d restrictions in the Logical System\nwhen loading theorems from the MMT Folder. \'NoUpdate\' is the default but if\nthe Proof Asst GUI Edit menu \'Set Soft Dj Vars Error Handling\' is set to\n\'GenerateNew\', then the \'Theorem Loader Dj Vars\' option \'Replace\' is good!\n\n* Set Theorem Loader Audit Messages -- Specifies whether or not the Theorem\nLoader should generate \'audit messages\'. The default is \'Yes\'. The audit\nmessages are displayed in the message area on the Proof Asst GUI and are very\nhelpful.\n\n* Set Store MM Indent Amt -- indentation amount used when writing theorems\nto the MMT folder. Default is 2.\n\n* Set Store MM Right Col -- right margin used when writing theorems to the\nMMT folder. Default is 79.\n\n* Set Store MM Formulas AsIs -- If \'yes\', writes formulas to the MMT Folder\nas they are in the Proof Worksheet. This parameter has no effect when\nstoring theorems which already exist in the Logical System (only proofs and\n$d restrictions are updated for these theorems.)\n\n\n==== 2nd/Right Mouse Button Pop-Up Menu ====\n\n* Cut, Copy, Paste -- Same as Edit Menu functions describe above.\n\n* Reformat Step -- Reformat the proof step where the cursor is located using\nthe current TMFF Format Number and Indent Amount.\n\n* Reformat Step:Swap Alt -- Swap/toggle current TMFF Format Number and\nAmount to or from the Alternate Format Number and Indent Amount, and then\nreformat just the proof step where the cursor is located. Note that this\nfunction toggles the current settings (the \'mode\') for the entire proof,\nand that the program retains no memory about the formatting of individual\nproof steps.\n\n* Step Selector Search -- Same as Unify Menu item above.\n\n* Reshow Step Selector Dialog -- Same as Unify Menu item above.\n\n\n========= GMFF Menu =========\n\n* Export Via GMFF -- GMFF (Graphics Mode Formula Formatting) exports the\nProof Worksheet as html file(s) in the \\mmj2jar\\gmff directory.\nSee \\mmj2\\doc\\GMFFDoc\\* \n\n\n==== Help Menu ====\n\n* General Help Info -- This page.\n\n* About mmj2 -- Some copyright information *plus* very interesting data\nabout your computer\'s memory: \'Max\' = the maximum amount of memory that the\nJava Virtual Machine will attempt to hog; \'Free\' = memory available for use,\nwhich may increase after the JVM does its \'garbage collection\' duties; and\n\'Total\' = the total amount of memory in the JVM at the time (will be <=\nMax.) Note: if your machine is memory constrained, or if you wish to\neconomize, there are mmj2 RunParms which may be altered to reduce the memory\nrequirements of mmj2 and the Proof Assistant -- and these may also shorten\nthe mmj2 start-up time!\n" |
public static final java.lang.String |
GENERAL_SEARCH_ITEM_TEXT |
"General Search" |
public static final java.lang.String |
GENERATED_PROOF_STMT_TOKEN |
"$=" |
public static final int |
GREATEST_STEP_NBR_INCREMENT_AMT |
1 |
public static final java.lang.String |
HEADER_LOC_AFTER_EQUAL_PREFIX |
"LOC_AFTER=" |
public static final int |
HEADER_LOC_AFTER_EQUAL_PREFIX_CHUNK_INDEX |
8 |
public static final java.lang.String |
HEADER_MM_TOKEN |
"<MM>" |
public static final int |
HEADER_MM_TOKEN_CHUNK_INDEX |
2 |
public static final java.lang.String |
HEADER_PROOF_ASST_TOKEN |
"<PROOF_ASST>" |
public static final int |
HEADER_PROOF_ASST_TOKEN_CHUNK_INDEX |
4 |
public static final java.lang.String |
HEADER_STMT_TOKEN |
"$(" |
public static final java.lang.String |
HEADER_THEOREM_EQUAL_PREFIX |
"THEOREM=" |
public static final int |
HEADER_THEOREM_EQUAL_PREFIX_CHUNK_INDEX |
6 |
public static final java.lang.String |
HELP_ABOUT_TEXT |
"mmj2 Version 2.5.3 as of 23-Sep-2019.\n\nCopyright (C) 2005 thru 2011 MEL O\'CAT via X178G243 (at) yahoo (dot) com \nLicense terms: GNU General Public License Version 2 or any later version.\n\nNote: The following copyright is included because ProofAsstGUI.java\nhas several snippets of code that are very similar, if not identical\nto snippets of code in the Java Tutorial.\n\nCopyright\u00a9 1995-2004 Sun Microsystems, Inc. All Rights Reserved.\nRedistribution and use in source and binary forms, with or without\nmodification, are permitted provided that the following conditions are\nmet\n* Redistribution of source code must retain the above copyright\n notice, this list of conditions and the following disclaimer.\n* Redistribution in binary form must reproduce the above copyright\n notice, this list of conditions and the following disclaimer in the\n documentation and/or other materials provided with the distribution.\n(See SunJavaTutorialLicense.html in the mmj2 distribution for the\nfor the disclaimer.)\n\nGarbage Collection Run (just now) Memory Totals follow:\n Max Memory = %s\n Free Memory = %s\n Total Memory = %s\n" |
public static final java.lang.String |
HELP_ABOUT_TITLE |
"About mmj2" |
public static final boolean |
HIGHLIGHTING_ENABLED_DEFAULT |
true |
public static final java.lang.String |
HYP_STEP_PREFIX |
"h" |
public static final char |
LOCAL_REF_ESCAPE_CHAR |
35 |
public static final java.lang.String |
MACRO_STMT_TOKEN |
"$m" |
public static final int |
MAX_FIELD_DELIMITER_COLONS |
2 |
public static final int |
MAX_UNIFY_ALTERNATES |
10 |
public static final boolean |
OUTPUT_CURSOR_INSTRUMENTATION_DEFAULT |
false |
public static final java.lang.String |
PA_GUI_ACTION_BEFORE_SAVE_CLOSE |
"Close" |
public static final java.lang.String |
PA_GUI_ACTION_BEFORE_SAVE_EXIT |
"Exit" |
public static final java.lang.String |
PA_GUI_ACTION_BEFORE_SAVE_NEW |
"New" |
public static final java.lang.String |
PA_GUI_ACTION_BEFORE_SAVE_OPEN |
"Open" |
public static final java.lang.String |
PA_GUI_CANCEL_MENU_KILL_ITEM_TEXT |
"Cancel (Looping? Kill it!!!)" |
public static final java.lang.String |
PA_GUI_CANCEL_MENU_TITLE |
"Cancel" |
public static final java.lang.String |
PA_GUI_DEFAULT_FILE_NAME_SUFFIX |
".mmp" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_COPY_ITEM_TEXT |
"Copy" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_CUT_ITEM_TEXT |
"Cut" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_DEC_FONT_ITEM_TEXT |
"Smaller Font Size" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_FONT_STYLE_BOLD_ITEM_TEXT |
"Set Font Style BOLD" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_FONT_STYLE_PLAIN_ITEM_TEXT |
"Set Font Style PLAIN" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_INC_FONT_ITEM_TEXT |
"Larger Font Size" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_PASTE_ITEM_TEXT |
"Paste" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_REDO_ITEM_TEXT |
"Redo" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_REFORMAT_ITEM_TEXT |
"Reformat Proof" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_REFORMAT_SWAP_ALT_ITEM_TEXT |
"Reformat Proof: Swap Alt" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_SET_BACKGROUND_ITEM_TEXT |
"Set Background Color" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_SET_FONT_FAMILY_ITEM_TEXT |
"Set Font Family" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_SET_FOREGROUND_ITEM_TEXT |
"Set Foreground Color" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_SET_FORMAT_NBR_ITEM_TEXT |
"Set Format Number" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_SET_INCOMPLETE_STEP_CURSOR_ITEM_TEXT |
"Set Incomplete Step Cursor" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_SET_INDENT_ITEM_TEXT |
"Set Indent" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_SET_SOFT_DJ_ERROR_ITEM_TEXT |
"Set Soft Dj Vars Error Handling" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_TITLE |
"Edit" |
public static final java.lang.String |
PA_GUI_EDIT_MENU_UNDO_ITEM_TEXT |
"Undo" |
public static final java.lang.String |
PA_GUI_FILE_CHOOSER_DESCRIPTION |
"Text and mmj2 Proof Asst files" |
public static final java.lang.String |
PA_GUI_FILE_CHOOSER_FILE_SUFFIX_MMP |
".mmp" |
public static final java.lang.String |
PA_GUI_FILE_CHOOSER_FILE_SUFFIX_TXT |
".txt" |
public static final java.lang.String |
PA_GUI_FILE_MENU_CLOSE_ITEM_TEXT |
"Close Proof File" |
public static final java.lang.String |
PA_GUI_FILE_MENU_EXIT_ITEM_TEXT |
"Exit/Quit" |
public static final java.lang.String |
PA_GUI_FILE_MENU_EXPORT_VIA_GMFF_ITEM_TEXT |
"Export Via GMFF" |
public static final java.lang.String |
PA_GUI_FILE_MENU_GET_BWD_PROOF_ITEM_TEXT |
"Backward-Get Proof" |
public static final java.lang.String |
PA_GUI_FILE_MENU_GET_FWD_PROOF_ITEM_TEXT |
"Forward-Get Proof" |
public static final java.lang.String |
PA_GUI_FILE_MENU_GET_PROOF_ITEM_TEXT |
"Get Proof" |
public static final java.lang.String |
PA_GUI_FILE_MENU_LOAD_SETTINGS |
"Load Settings" |
public static final java.lang.String |
PA_GUI_FILE_MENU_NEW_ITEM_TEXT |
"New Proof" |
public static final java.lang.String |
PA_GUI_FILE_MENU_NEW_NEXT_ITEM_TEXT |
"New-Next Proof" |
public static final java.lang.String |
PA_GUI_FILE_MENU_OPEN_ITEM_TEXT |
"Open Proof File" |
public static final java.lang.String |
PA_GUI_FILE_MENU_SAVE_AS_ITEM_TEXT |
"Save As..." |
public static final java.lang.String |
PA_GUI_FILE_MENU_SAVE_ITEM_TEXT |
"Save Proof File" |
public static final java.lang.String |
PA_GUI_FILE_MENU_SAVE_SETTINGS |
"Save Settings" |
public static final java.lang.String |
PA_GUI_FILE_MENU_TITLE |
"File" |
public static final java.lang.String |
PA_GUI_GET_THEOREM_LABEL_PROMPT |
"Theorem label?" |
public static final java.lang.String |
PA_GUI_GET_THEOREM_LABEL_PROMPT_2 |
"Label %s invalid: not found or not a Theorem. Theorem label?" |
public static final java.lang.String |
PA_GUI_GMFF_MENU_TITLE |
"GMFF" |
public static final java.lang.String |
PA_GUI_HELP_ABOUT |
"About mmj2" |
public static final java.lang.String |
PA_GUI_HELP_BATCH_COMMAND_DOCUMENTATION_TITLE |
"Documentation viewer" |
public static final java.lang.String |
PA_GUI_HELP_MENU_BATCH_COMMAND_DOCUMENTATION |
"Batch command documentation" |
public static final java.lang.String |
PA_GUI_HELP_MENU_GENERAL |
"General Help Info" |
public static final java.lang.String |
PA_GUI_HELP_MENU_TITLE |
"Help" |
public static final java.lang.String |
PA_GUI_NEW_THEOREM_LABEL_PROMPT |
"Theorem label?" |
public static final java.lang.String |
PA_GUI_POPUP_MENU_REFORMAT_STEP_TEXT |
"Reformat Step" |
public static final java.lang.String |
PA_GUI_POPUP_MENU_REFORMAT_SWAP_ALT_STEP_TEXT |
"Reformat Step: Swap Alt" |
public static final java.lang.String |
PA_GUI_SAVE_BEFORE_CLOSE_QUESTION |
"Save changes before Window Closes?" |
public static final java.lang.String |
PA_GUI_SAVE_PROOF_TEXT_TITLE |
"SaveProofTextFile()" |
public static final java.lang.String |
PA_GUI_SEARCH_MENU_TITLE |
"Search" |
public static final java.lang.String |
PA_GUI_SET_FONT_FAMILY_PROMPT |
"Enter Font Family Name" |
public static final java.lang.String |
PA_GUI_SET_FORMAT_NBR_PROMPT |
"Enter Format Number" |
public static final java.lang.String |
PA_GUI_SET_INCOMPLETE_STEP_CURSOR_OPTION_PROMPT |
"Enter Incomplete Step Cursor Option Number" |
public static final java.lang.String |
PA_GUI_SET_INDENT_PROMPT |
"Enter Indent amount, 0 through " |
public static final java.lang.String |
PA_GUI_SET_MAX_RESULTS_OPTION_PROMPT |
"Enter Step Selector Max Results Number (1 thru 9999)" |
public static final java.lang.String |
PA_GUI_SET_SHOW_SUBST_OPTION_PROMPT |
"Enter Step Select Show Substitutions option (true or false)" |
public static final java.lang.String |
PA_GUI_SET_SOFT_DJ_ERROR_OPTION_PROMPT |
"Enter Soft Dj Vars Error Option Number" |
public static final java.lang.String |
PA_GUI_SET_TL_AUDIT_MESSAGES_OPTION_PROMPT |
"Enter Theorem Loader Audit Messages option (True or False)" |
public static final java.lang.String |
PA_GUI_SET_TL_DJ_VARS_OPTION_PROMPT |
"Enter Theorem Loader DjVars Option:" |
public static final java.lang.String |
PA_GUI_SET_TL_MMT_FOLDER_OPTION_PROMPT |
"Select MMT Folder" |
public static final java.lang.String |
PA_GUI_SET_TL_MMT_FOLDER_OPTION_PROMPT_2 |
"\nTry another?" |
public static final java.lang.String |
PA_GUI_SET_TL_STORE_FORMULAS_AS_IS_OPTION_PROMPT |
"Enter Theorem Loader Store Formulas AsIs option (True or False)" |
public static final java.lang.String |
PA_GUI_SET_TL_STORE_MM_INDENT_AMT_OPTION_PROMPT |
"Enter Theorem Loader Store MM Indent Amt (0 thru 9)" |
public static final java.lang.String |
PA_GUI_SET_TL_STORE_MM_RIGHT_COL_OPTION_PROMPT |
"Enter Theorem Loader Store MM Right (margin) Col (70 thru 9999)" |
public static final java.lang.String |
PA_GUI_TL_MENU_AUDIT_MESSAGES |
"Set Theorem Loader Audit Messages" |
public static final java.lang.String |
PA_GUI_TL_MENU_COMPRESSION |
"Set Proof Compression" |
public static final java.lang.String |
PA_GUI_TL_MENU_DJ_VARS_OPTION |
"Set Theorem Loader Dj Vars Option" |
public static final java.lang.String |
PA_GUI_TL_MENU_EXTRACT_THEOREM |
"Extract Theorem To MMT Folder" |
public static final java.lang.String |
PA_GUI_TL_MENU_LOAD_THEOREMS |
"Load Theorems From MMT Folder" |
public static final java.lang.String |
PA_GUI_TL_MENU_MMT_FOLDER |
"Set Theorem Loader MMT Folder" |
public static final java.lang.String |
PA_GUI_TL_MENU_STORE_FORMULAS_AS_IS |
"Set Store MM Formulas AsIs" |
public static final java.lang.String |
PA_GUI_TL_MENU_STORE_MM_INDENT_AMT |
"Set Store MM Indent Amt" |
public static final java.lang.String |
PA_GUI_TL_MENU_STORE_MM_RIGHT_COL |
"Set Store MM Right Col" |
public static final java.lang.String |
PA_GUI_TL_MENU_TITLE |
"TL" |
public static final java.lang.String |
PA_GUI_TL_MENU_UNIFY_PLUS_STORE |
"Unify + Store In MMT Folder" |
public static final java.lang.String |
PA_GUI_TL_MENU_UNIFY_PLUS_STORE_IN_LOG_SYS |
"Unify + Store In LogSys and MMT Folder" |
public static final java.lang.String |
PA_GUI_TL_MENU_VERIFY_ALL_PROOFS |
"Verify All Proofs" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_ERASE_NO_WV_ITEM_TEXT |
"Unify+Erase+Don\'t Convert" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_NO_WV_ITEM_TEXT |
"Unify+Don\'t Convert WorkVars" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_REDERIVE_ITEM_TEXT |
"Unify+Erase and Rederive Formulas" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_RESHOW_STEP_SELECTOR_DIALOG_ITEM_TEXT |
"Reshow Step Selector Dialog" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_SET_MAX_RESULTS_ITEM_TEXT |
"Set Step Selector Max Results" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_SET_SHOW_SUBST_ITEM_TEXT |
"Set Step Selector Show Substitutions" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_START_ITEM_TEXT |
"Unify (check proof)" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_START_UR_ITEM_TEXT |
"Unify+Renumber" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_STEP_SELECTOR_SEARCH_ITEM_TEXT |
"Step Selector Search" |
public static final java.lang.String |
PA_GUI_UNIFY_MENU_TITLE |
"Unify" |
public static final java.lang.String |
PA_GUI_YES_NO_CANCEL_TITLE |
"getYesNoCancelAnswer()" |
public static final java.lang.String |
PA_GUI_YES_NO_TITLE |
"getYesNoAnswer()" |
public static final int |
PA_TESTMSG_THEOREM_NUMBER_THRESHOLD |
20 |
public static final int |
PA_TESTMSG_THEOREM_TIME_TOP_NUMBER |
10 |
public static final java.lang.String |
PA_UNKNOWN_THEOREM_LABEL |
"?" |
public static final boolean |
PROOF_ASST_ASCII_RETEST_DEFAULT |
false |
public static final java.lang.String |
PROOF_ASST_COMPRESSION_LIST |
"Valid Proof Compression Options: " |
public static final java.lang.String |
PROOF_ASST_COMPRESSION_PROMPT |
"Enter Proof Compression Number" |
public static final int |
PROOF_ASST_ERROR_MESSAGE_COLUMNS_DEFAULT |
80 |
public static final int |
PROOF_ASST_ERROR_MESSAGE_COLUMNS_MAX |
999 |
public static final int |
PROOF_ASST_ERROR_MESSAGE_COLUMNS_MIN |
40 |
public static final int |
PROOF_ASST_ERROR_MESSAGE_ROWS_DEFAULT |
4 |
public static final int |
PROOF_ASST_ERROR_MESSAGE_ROWS_MAX |
99 |
public static final int |
PROOF_ASST_ERROR_MESSAGE_ROWS_MIN |
2 |
public static final boolean |
PROOF_ASST_EXCLUDE_DISCOURAGED_DEFAULT |
true |
public static final boolean |
PROOF_ASST_EXPORT_DERIVE_FORMULAS_DEFAULT |
false |
public static final boolean |
PROOF_ASST_EXPORT_FORMAT_UNIFIED_DEFAULT |
false |
public static final boolean |
PROOF_ASST_FONT_BOLD_DEFAULT |
false |
public static final java.lang.String |
PROOF_ASST_FONT_FAMILY_DEFAULT |
"Monospaced" |
public static final java.lang.String |
PROOF_ASST_FONT_FAMILY_LIST |
"Valid font family names defined in your system: " |
public static final int |
PROOF_ASST_FONT_SIZE_CHG_AMT |
2 |
public static final int |
PROOF_ASST_FONT_SIZE_DEFAULT |
14 |
public static final int |
PROOF_ASST_FONT_SIZE_MAX |
72 |
public static final int |
PROOF_ASST_FONT_SIZE_MIN |
8 |
public static final int |
PROOF_ASST_FORMULA_LEFT_COL_DEFAULT |
20 |
public static final int |
PROOF_ASST_FORMULA_LEFT_COL_MIN |
2 |
public static final int |
PROOF_ASST_FORMULA_RIGHT_COL_DEFAULT |
79 |
public static final int |
PROOF_ASST_FORMULA_RIGHT_COL_MAX |
2147483647 |
public static final java.lang.String |
PROOF_ASST_FRAME_TITLE |
"ProofAsstGUI" |
public static final java.lang.String |
PROOF_ASST_GUI_STARTUP_MSG |
"Hi! I am mmj2 v2.5.3 as of 23-Sep-2019.\nVisit https://github.com/digama0/mmj2/ or\nhttp://code.google.com/p/metamath-mmj2/\nfor support or bug reports." |
public static final boolean |
PROOF_ASST_IMPORT_COMPARE_DJS_DEFAULT |
false |
public static final boolean |
PROOF_ASST_IMPORT_UPDATE_DJS_DEFAULT |
false |
public static final java.lang.String |
PROOF_ASST_INCOMPLETE_STEP_CURSOR_OPTION_LIST |
"Valid Incomplete Step Cursor Options: " |
public static final float |
PROOF_ASST_LINE_SPACING_DEFAULT |
0.0f |
public static final boolean |
PROOF_ASST_LINE_WRAP_DEFAULT |
false |
public static final boolean |
PROOF_ASST_MAXIMIZED_DEFAULT |
false |
public static final boolean |
PROOF_ASST_PRINT_DEFAULT |
false |
public static final int |
PROOF_ASST_RPN_PROOF_LEFT_COL_AUTO |
0 |
public static final int |
PROOF_ASST_RPN_PROOF_LEFT_COL_DEFAULT |
5 |
public static final int |
PROOF_ASST_RPN_PROOF_LEFT_COL_MIN |
4 |
public static final int |
PROOF_ASST_RPN_PROOF_RIGHT_COL_DEFAULT |
70 |
public static final int |
PROOF_ASST_RPN_PROOF_RIGHT_COL_MAX |
2147483647 |
public static final java.lang.String |
PROOF_ASST_SETTINGS_FILE_DEFAULT |
"store.json" |
public static final java.lang.String |
PROOF_ASST_SOFT_DJ_ERROR_OPTION_LIST |
"Valid Soft Dj Vars Error Options: " |
public static final java.lang.String |
PROOF_ASST_STYLE_CLASS |
"class" |
public static final java.lang.String |
PROOF_ASST_STYLE_COMMENT |
"comment" |
public static final java.lang.String |
PROOF_ASST_STYLE_DEFAULT |
"default" |
public static final java.lang.String |
PROOF_ASST_STYLE_ERROR |
"error" |
public static final java.lang.String |
PROOF_ASST_STYLE_HYP |
"hyp" |
public static final java.lang.String |
PROOF_ASST_STYLE_KEYWORD |
"keyword" |
public static final java.lang.String |
PROOF_ASST_STYLE_LOCREF |
"localref" |
public static final java.lang.String |
PROOF_ASST_STYLE_PROOF |
"proof" |
public static final java.lang.String |
PROOF_ASST_STYLE_REF |
"ref" |
public static final java.lang.String |
PROOF_ASST_STYLE_SET |
"set" |
public static final java.lang.String |
PROOF_ASST_STYLE_SPECIAL_STEP |
"specialstep" |
public static final java.lang.String |
PROOF_ASST_STYLE_STEP |
"step" |
public static final java.lang.String |
PROOF_ASST_STYLE_WFF |
"wff" |
public static final java.lang.String |
PROOF_ASST_STYLE_WORKVAR |
"workvar" |
public static final boolean |
PROOF_ASST_TEXT_AT_TOP_DEFAULT |
true |
public static final int |
PROOF_ASST_TEXT_COLUMNS_DEFAULT |
80 |
public static final int |
PROOF_ASST_TEXT_COLUMNS_MAX |
999 |
public static final int |
PROOF_ASST_TEXT_COLUMNS_MIN |
40 |
public static final int |
PROOF_ASST_TEXT_ROWS_DEFAULT |
21 |
public static final int |
PROOF_ASST_TEXT_ROWS_MAX |
99 |
public static final int |
PROOF_ASST_TEXT_ROWS_MIN |
2 |
public static final int |
PROOF_STEP_RENUMBER_INTERVAL |
1 |
public static final int |
PROOF_STEP_RENUMBER_START |
50 |
public static final java.lang.String |
PROOF_TEXT_FONT_FAMILY |
"Monospaced" |
public static final java.lang.String |
PROOF_TEXT_FOOTER |
"$)" |
public static final java.lang.String |
PROOF_TEXT_HEADER_1 |
"$( <MM> <PROOF_ASST> THEOREM=" |
public static final java.lang.String |
PROOF_TEXT_HEADER_2 |
" LOC_AFTER=" |
public static final java.lang.String |
PROOF_TEXT_READER_CAPTION |
"Proof Text Reader" |
public static final int |
PROOF_TEXT_TAB_LENGTH |
1 |
public static final java.lang.String |
PROOF_WORKSHEET_COMMENT_STMT_IO_ERROR |
"IO error reading comment!" |
public static final java.lang.String |
QED_STEP_NBR |
"qed" |
public static final java.lang.String |
QED_STEP_NBR_CAPS |
"QED" |
public static final boolean |
RECHECK_PROOF_ASST_USING_PROOF_VERIFIER_DEFAULT |
false |
public static final boolean |
REQUEST_MESSAGES_GUI_ENABLED |
false |
public static final java.lang.String |
REQUEST_MESSAGES_GUI_TEXT_DEFAULT |
"No errors!" |
public static final java.lang.String |
REQUEST_MESSAGES_GUI_TITLE_DEFAULT |
"Request Messages" |
public static final java.lang.String |
RESHOW_SEARCH_RESULTS_ITEM_TEXT |
"Reshow Search Results" |
public static final java.lang.String |
SAMPLE_PROOF_LABEL |
"syllogism" |
public static final java.lang.String |
SAMPLE_PROOF_TEXT |
"$( <MM> <PROOF_ASST> THEOREM=syllogism LOC_AFTER=\n\nh1:: |- ( ph -> ps ) \nh2:: |- ( ps -> ch ) \n3:2: |- ( ph -> ( ps -> ch ) ) \n4:3: |- ( ( ph -> ps ) -> ( ph -> ch ) ) \nqed:1,4: |- ( ph -> ch ) \n\n$)\n" |
public static final java.lang.String |
SEARCH_OPTIONS_ITEM_TEXT |
"Search Options" |
public static final java.lang.String |
STEP_SEARCH_ITEM_TEXT |
"Step Search" |
public static final java.lang.String |
STEP_SELECTOR_DIALOG_HIDE_BUTTON_CAPTION |
"Hide Dialog" |
public static final java.lang.String |
STEP_SELECTOR_DIALOG_LIST_CAPTION_PREFIX |
"Step " |
public static final java.lang.String |
STEP_SELECTOR_DIALOG_LIST_CAPTION_SUFFIX |
" Unifiable Assertions" |
public static final int |
STEP_SELECTOR_DIALOG_PANE_HEIGHT_DEFAULT |
440 |
public static final int |
STEP_SELECTOR_DIALOG_PANE_HEIGHT_MAX |
9999 |
public static final int |
STEP_SELECTOR_DIALOG_PANE_HEIGHT_MIN |
100 |
public static final int |
STEP_SELECTOR_DIALOG_PANE_WIDTH_DEFAULT |
720 |
public static final int |
STEP_SELECTOR_DIALOG_PANE_WIDTH_MAX |
9999 |
public static final int |
STEP_SELECTOR_DIALOG_PANE_WIDTH_MIN |
100 |
public static final java.lang.String |
STEP_SELECTOR_DIALOG_POPUP_SET_BUTTON_CAPTION |
"Apply Selection To Step And Unify Proof?" |
public static final java.lang.String |
STEP_SELECTOR_DIALOG_SET_BUTTON_CAPTION |
"Apply Selection To Step And Unify Proof" |
public static final java.lang.String |
STEP_SELECTOR_DIALOG_TITLE |
"StepSelectorDialog" |
public static final java.lang.String |
STEP_SELECTOR_FORMULA_LABEL_SEPARATOR |
" ::= " |
public static final java.lang.String |
STEP_SELECTOR_FORMULA_LOG_HYP_SEPARATOR |
" && " |
public static final java.lang.String |
STEP_SELECTOR_FORMULA_YIELDS_SEPARATOR |
" ==> " |
public static final java.lang.String |
STEP_SELECTOR_LIST_END_LITERAL |
"***END***" |
public static final java.lang.String |
STEP_SELECTOR_LIST_MORE_LITERAL |
"***MORE***" |
public static final int |
STEP_SELECTOR_MAX_RESULTS_DEFAULT |
50 |
public static final int |
STEP_SELECTOR_MAX_RESULTS_MAXIMUM |
9999 |
public static final java.lang.String |
STEP_SELECTOR_SEARCH_FORMULA_INDENT |
" " |
public static final int |
STEP_SELECTOR_SEARCH_HYP_LOOKUP_MAX |
3 |
public static final boolean |
STEP_SELECTOR_SHOW_SUBSTITUTIONS_DEFAULT |
true |
public static final int |
STEP_UNIFIER_APPLIED_ARRAY_LEN_INIT |
1000 |
public static final int |
STEP_UNIFIER_APPLIED_ARRAY_LEN_MAX |
8000 |
public static final java.lang.String |
SYNONYM_FALSE_1 |
"false" |
public static final java.lang.String |
SYNONYM_FALSE_2 |
"off" |
public static final java.lang.String |
SYNONYM_FALSE_3 |
"no" |
public static final java.lang.String |
SYNONYM_TRUE_1 |
"true" |
public static final java.lang.String |
SYNONYM_TRUE_2 |
"on" |
public static final java.lang.String |
SYNONYM_TRUE_3 |
"yes" |
public static final boolean |
UNDO_REDO_ENABLED_DEFAULT |
true |
public static final int |
UNIFIER_MAX_LOG_HYPS |
100 |
public static final int |
UNIFIER_MAX_VAR_HYPS |
500 |
public static final java.lang.String |
VERSION |
"2.5.3" |
public static final java.lang.String |
VERSION_DATE |
"23-Sep-2019" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
NS |
"PA" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
KEY_OVERRIDE |
"manual" |
public static final java.lang.String |
KEY_REMOVE |
"remove" |
public static final java.lang.String |
KEY_STORE |
"store" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
COMPLETED_ITEM_OUTPUT_LITERAL |
"(*) " |
public static final java.lang.String |
DOT_STEP_CAPTION |
".Step " |
public static final java.lang.String |
ERRMSG_ARG_ERROR_1 |
"A-SE-0301 Validation error for field " |
public static final java.lang.String |
ERRMSG_ARG_ERROR_2 |
" value = " |
public static final java.lang.String |
ERRMSG_ARG_ERROR_3 |
". " |
public static final java.lang.String |
ERRMSG_BAD_INT_ERROR |
" Is not an integer or is greater than " |
public static final java.lang.String |
ERRMSG_CANT_APPLY_OLD_SEARCH_RESULTS |
"A-SE-0105 Cannot \'Apply\': must be in Step Search mode, or the results are \'out of date\'." |
public static final java.lang.String |
ERRMSG_CHOICE_ERROR |
" Not a valid choice." |
public static final java.lang.String |
ERRMSG_EXCL_LABELS_SPECIFIER_BAD_ERROR |
" Is invalid. Must not contain \'$$\' or invalid regular expression specifiers. Valid example: *OLD,EE*,4??5*" |
public static final java.lang.String |
ERRMSG_EXCL_LABELS_SPECIFIER_BAD_ERROR2 |
" Failed compilation as a \'Regular Expression\'. Valid example: *OLD,EE*,4??5*" |
public static final java.lang.String |
ERRMSG_EXCL_LABELS_SPECIFIER_BAD_ERROR2_2 |
" System message = " |
public static final java.lang.String |
ERRMSG_FUNCTION_INOPERABLE_IN_TEST_MODE |
"A-SE-0104 Requested function inoperable in test mode." |
public static final java.lang.String |
ERRMSG_MAX_HYPS_LT_STEP_HYPS_ERROR |
" Is less than number of Proof Step Hyps = " |
public static final java.lang.String |
ERRMSG_MIN_HYPS_GT_MAX_HYPS_ERROR |
" Is greater than number of MaxHyps = " |
public static final java.lang.String |
ERRMSG_MIN_HYPS_GT_STEP_HYPS_ERROR |
" Is greater than number of Proof Step Hyps = " |
public static final java.lang.String |
ERRMSG_NEGATIVE_ERROR |
" Is less than zero." |
public static final java.lang.String |
ERRMSG_NO_TASK_TO_CANCEL |
"A-SE-0102 Oops! Did not find Proof Asst/Search task already running. Try your original request again?" |
public static final java.lang.String |
ERRMSG_OR_SEPARATOR_EQ_QUOTE_ERROR |
" Must not equal or match the leading portion of SingleQuote or DoubleQuote, or vice-versa." |
public static final java.lang.String |
ERRMSG_PA_GUI_TASK_ALREADY_RUNNING |
"A-SE-0101 Proof Asst/Search task already running. Please try again momentarily, or click the \'Cancel\' button?" |
public static final java.lang.String |
ERRMSG_REQUIRED_INPUT_ERROR |
" Is required. " |
public static final java.lang.String |
ERRMSG_SEARCH_ASSRT_LIST_EMPTY_1 |
"A-SE-0201 Input list of assertions for search is empty!" |
public static final java.lang.String |
ERRMSG_SEARCH_NULL_PARSE_TREE_1 |
"A-SE-0202 Null parse tree for Hyp\'s formula, this should have been caught!" |
public static final java.lang.String |
ERRMSG_SEARCH_TASK_EXECUTION_1 |
"E-SE-0205 Search task execution exception! System Message = " |
public static final java.lang.String |
ERRMSG_SEARCH_TASK_INTERRUPTED_1 |
"E-SE-0204 Search task interrupted. Increase MaxTime option, or modify other SearchOptions? System Message = " |
public static final java.lang.String |
ERRMSG_SEARCH_TASK_TIMEOUT_1 |
"E-SE-0203 Search task timed out. Increase MaxTime option, or modify other SearchOptions? System Message = " |
public static final java.lang.String |
ERRMSG_SINGLE_EQ_DOUBLE_QUOTE_ERROR |
" Must not equal or match the leading portion of DoubleQuote, or vice-versa." |
public static final java.lang.String |
ERRMSG_TASK_CANCEL_REQUESTED |
"A-SE-0103 Requested cancel of running Proof Asst/Search task. In a moment, please retry your original request?" |
public static final java.lang.String |
ERRMSG_UNSUPPORTED_FEATURE_ERROR |
" Feature not yet supported (not coded...)" |
public static final java.lang.String |
ERROR_EMPTY_SEARCH_TERM_1 |
"E-SE-0408 Empty string search term is invalid." |
public static final java.lang.String |
ERROR_MISSING_END_QUOTE_1 |
"E-SE-0407 Search term end quote missing." |
public static final java.lang.String |
ERROR_MISSING_STARTING_QUOTE_1 |
"E-SE-0406 Next search term missing starting quote." |
public static final java.lang.String |
ERROR_NO_SEARCH_TERMS_1 |
"A-SE-0405 Severe program error: expected search terms are missing in ForWhat field." |
public static final java.lang.String |
ERROR_OR_AFTER_LAST_SEARCH_TERM_1 |
"E-SE-0411 An \'or\' after the last search term is invalid." |
public static final java.lang.String |
ERROR_OR_BEFORE_FIRST_SEARCH_TERM_1 |
"E-SE-0409 An \'or\' before the first search term is invalid." |
public static final java.lang.String |
ERROR_PARSE_EXPR_TERM_COMPILE_1 |
"E-SE-0413 Failed expression parse. Text = " |
public static final java.lang.String |
ERROR_PARSE_EXPR_TERM_COMPILE_1_2 |
". Detailed message = " |
public static final java.lang.String |
ERROR_PARSE_STMT_TERM_COMPILE_1 |
"E-SE-0414 Failed statement parse. Text = " |
public static final java.lang.String |
ERROR_PARSE_STMT_TERM_COMPILE_1_2 |
". Detailed message = " |
public static final java.lang.String |
ERROR_PARSE_STMT_TERM_EVAL_1 |
"E-SE-0415 ParseStmt search term evaluation error. Text = " |
public static final java.lang.String |
ERROR_PARSE_STMT_TERM_EVAL_1_2 |
". Detailed message = " |
public static final java.lang.String |
ERROR_SEARCH_DATA_LINE_FORMAT_1 |
"A-SE-0401 Program bug! Bad Format choice found while creating SearchDataLine. Value = " |
public static final java.lang.String |
ERROR_SEARCH_DATA_LINE_IN_WHAT_1 |
"A-SE-0403 Program bug! Bad InWhat choice found while creating SearchDataLine. Value = " |
public static final java.lang.String |
ERROR_SEARCH_DATA_LINE_PART_1 |
"A-SE-0402 Program bug! Bad Part choice found while creating SearchDataLine. Value = " |
public static final java.lang.String |
ERROR_SEARCH_DATA_LINE_PART2_1 |
"A-SE-0404 Program bug! Bad Part choice found while creating SearchDataLine. Value = " |
public static final java.lang.String |
ERROR_SEARCH_TERM_REGEX_COMPILE_1 |
"E-SE-0412 Failed compilation as a Regular Expression. Text = " |
public static final java.lang.String |
ERROR_SEARCH_TERM_REGEX_COMPILE_1_2 |
". System message = " |
public static final java.lang.String |
ERROR_SEARCH_UNIFIER_OPER_CHOICE_1 |
"A-SE-0501 Program bug! Bad Oper value for ParseStmt in SearchUnifier! Value = " |
public static final java.lang.String |
ERROR_SEARCH_UNIFIER_OPER_CHOICE_2 |
"A-SE-0502 Program bug! Bad Oper value for ParseExpr in SearchUnifier! Value = " |
public static final java.lang.String |
ERROR_TWO_ORS_1 |
"E-SE-0410 Only one \'or\' is permitted between each pair of search terms." |
public static final java.lang.String |
SEARCH_FONT_FAMILY |
"Monospaced" |
public static final java.lang.String |
SEARCH_OPTIONS_NEW_STMT_LABEL_PROMPT |
"Statement label, or a blank?" |
public static final java.lang.String |
SEARCH_OPTIONS_NEW_STMT_LABEL_PROMPT_2 |
"Label %s invalid: not found or not a Statement. Statement label, or a blank?" |
public static final java.lang.String |
SEARCH_OUTPUT_FORMULA_LABEL_SEPARATOR |
" ::= " |
public static final java.lang.String |
SEARCH_OUTPUT_FORMULA_LOG_HYP_SEPARATOR |
" && " |
public static final java.lang.String |
SEARCH_OUTPUT_FORMULA_YIELDS_SEPARATOR |
" ==> " |
public static final java.lang.String |
SEARCH_OUTPUT_LIST_END_LITERAL |
"***END***" |
public static final java.lang.String |
SEARCH_OUTPUT_LIST_MORE_LITERAL |
"***MORE***" |
public static final java.lang.String |
SEARCH_OUTPUT_SEARCH_FORMULA_INDENT |
" " |
public static final int |
SEARCH_RETURN_CODE_0 |
0 |
public static final int |
SEARCH_RETURN_CODE_ARG_ERROR |
1 |
public static final int |
SEARCH_RETURN_CODE_EXECUTION_ERROR |
4 |
public static final int |
SEARCH_RETURN_CODE_FATAL_ERROR |
16 |
public static final int |
SEARCH_RETURN_CODE_INTERRUPTED_ERROR |
3 |
public static final int |
SEARCH_RETURN_CODE_TIMEOUT_ERROR |
2 |
public static final int |
SEARCH_SCORE_COMPLETED_ITEM |
100 |
public static final int |
SEARCH_SCORE_NOT_SELECTED_ITEM |
0 |
public static final int |
SEARCH_SCORE_SELECTED_ITEM |
50 |
public static final int |
SEARCH_SCORE_TRAILER_ITEM |
-1 |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final int |
AUTO_SELECT_FIELD_ID |
39 |
public static final int |
BOOL_0_FIELD_ID |
8 |
public static final int |
BOOL_1_FIELD_ID |
14 |
public static final int |
BOOL_2_FIELD_ID |
20 |
public static final int |
BOOL_3_FIELD_ID |
26 |
public static final java.lang.String |
BOOL_VALUE_AND |
"AND" |
public static final int |
BOOL_VALUE_AND_ID |
0 |
public static final java.lang.String |
BOOL_VALUE_OR |
"OR" |
public static final int |
BOOL_VALUE_OR_ID |
1 |
public static final int |
CANCEL_BUTTON_ID |
1 |
public static final int |
CHAP_SEC_HIERARCHY_CHAP_DIRECT_ID |
1 |
public static final int |
CHAP_SEC_HIERARCHY_CHAP_INDIR_ID |
2 |
public static final int |
CHAP_SEC_HIERARCHY_EMPTY_STRING_ID |
0 |
public static final int |
CHAP_SEC_HIERARCHY_FIELD_ID |
40 |
public static final int |
CHAP_SEC_HIERARCHY_SEC_DIRECT_ID |
3 |
public static final int |
CHAP_SEC_HIERARCHY_SEC_INDIR_ID |
4 |
public static final java.lang.String |
CHAP_SEC_HIERARCHY_VALUE_CHAP_DIRECT |
"Chap/Direct" |
public static final java.lang.String |
CHAP_SEC_HIERARCHY_VALUE_CHAP_INDIR |
"Chap/Indir." |
public static final java.lang.String |
CHAP_SEC_HIERARCHY_VALUE_EMPTY_STRING |
"" |
public static final java.lang.String |
CHAP_SEC_HIERARCHY_VALUE_SEC_DIRECT |
"Sec/Direct" |
public static final java.lang.String |
CHAP_SEC_HIERARCHY_VALUE_SEC_INDIR |
"Sec/Indir." |
public static final int |
COMMENTS_FIELD_ID |
36 |
public static final java.lang.String |
DEFAULT_TITLE |
"Search Options, General Search R20121225 @ 20-Sep-2012 20:54" |
public static final int |
DOUBLE_QUOTE_FIELD_ID |
2 |
public static final java.lang.String |
ERRMSG_ARG_INTEGER_TEXT_INVALID |
"A-SO-0501 Severe program bug found: SearchArgsInt text value not numeric. Value = %s. fieldId = %d field label = %s" |
public static final java.lang.String |
ERRMSG_BUTTON_ATTR_TABLE_LOAD_ERROR |
"A-SO-0103 SearchOptionsConstants.BUTTON_ATTR[i].buttonId not equal to " |
public static final java.lang.String |
ERRMSG_FIELD_ATTR_TABLE_LOAD_ERROR |
"A-SO-0101 SearchOptionsConstants.FIELD_ATTR[i].fieldId not equal to " |
public static final java.lang.String |
ERRMSG_FORMAT_SEL_INVALID |
"A-SO-0801 Severe program bug found: FormatScrnMap selected item invalid. Item value = %s" |
public static final java.lang.String |
ERRMSG_FROM_CHAP_SEL_INVALID |
"A-SO-1001 Severe program bug found: FromChapScrnMap selected item invalid. Item value = %s" |
public static final java.lang.String |
ERRMSG_IN_WHAT_SEL_INVALID |
"A-SO-0601 Severe program bug found: InWhatScrnMap selected item invalid. Item value = %s" |
public static final java.lang.String |
ERRMSG_OPER_SEL_INVALID |
"A-SO-0901 Severe program bug found: OperScrnMap selected item invalid. Item value = %s" |
public static final java.lang.String |
ERRMSG_PART_SEL_INVALID |
"A-SO-0701 Severe program bug found: PartScrnMap selected item invalid. Item value = %s" |
public static final java.lang.String |
ERRMSG_SEARCH_ARGS_TABLE_LOAD_ERROR |
"A-SO-0102 SearchArgs.arg[i].getFieldId() not equal to " |
public static final java.lang.String |
ERRMSG_THRU_CHAP_SEL_INVALID |
"A-SO-1101 Severe program bug found: ThruChapScrnMap selected item invalid. Item value = %s" |
public static final java.lang.String |
ERRMSG_UNRECOGNIZED_BUTTON_ID |
"A-SO-1202 Unrecognized Button pressed. buttonId = %d" |
public static final int |
EXCL_LABELS_FIELD_ID |
27 |
public static final java.lang.String |
EXCLUSION_LABEL_TEXT |
"------Exclusion Criteria------" |
public static final java.lang.String |
EXCLUSION_LABEL_TOOL_TIP |
" Criteria for exclusion from the Search Results." |
public static final java.lang.String |
EXT_SEARCH_LABEL_TEXT |
" -------Extended Search--------" |
public static final java.lang.String |
EXT_SEARCH_LABEL_TOOL_TIP |
"Controls for Extended Search for Completed Search Results using the Search Results List and prior proof steps." |
public static final int |
FOR_WHAT_0_FIELD_ID |
7 |
public static final int |
FOR_WHAT_1_FIELD_ID |
13 |
public static final int |
FOR_WHAT_2_FIELD_ID |
19 |
public static final int |
FOR_WHAT_3_FIELD_ID |
25 |
public static final int |
FOR_WHAT_BORDER_THICKNESS |
3 |
public static final java.lang.String |
FOR_WHAT_VALUE_EMPTY_STRING |
"" |
public static final int |
FORMAT_0_FIELD_ID |
5 |
public static final int |
FORMAT_1_FIELD_ID |
11 |
public static final int |
FORMAT_2_FIELD_ID |
17 |
public static final int |
FORMAT_3_FIELD_ID |
23 |
public static final int |
FORMAT_CHAR_STR_ID |
2 |
public static final int |
FORMAT_METAMATH_ID |
0 |
public static final int |
FORMAT_PARSE_EXPR_ID |
3 |
public static final int |
FORMAT_PARSE_STMT_ID |
4 |
public static final int |
FORMAT_REG_EXPR_ID |
1 |
public static final int |
FORMAT_TYPE_NOT_TREE |
2 |
public static final int |
FORMAT_TYPE_SUB_TREE |
1 |
public static final int |
FORMAT_TYPE_TREE |
0 |
public static final java.lang.String |
FORMAT_VALUE_CHAR_STR |
"CharStr" |
public static final java.lang.String |
FORMAT_VALUE_METAMATH |
"Metamath" |
public static final java.lang.String |
FORMAT_VALUE_PARSE_EXPR |
"ParseExpr" |
public static final java.lang.String |
FORMAT_VALUE_PARSE_STMT |
"ParseStmt" |
public static final java.lang.String |
FORMAT_VALUE_REG_EXPR |
"RegExpr" |
public static final int |
FROM_CHAP_FIELD_ID |
43 |
public static final int |
FROM_SEC_FIELD_ID |
44 |
public static final java.lang.String |
GENERAL_HELP_FRAME_TITLE |
"SearchOptions Help: General Information, R20121225 @ 20-Sep-2012 20:54" |
public static final java.lang.String |
GENERAL_HELP_INFO_TEXT |
"************\n* Contents *\n************\n\n* Summary Information About The Search Options Window\n\n* Main Window Areas Explanation\n\n* Input Fields And Buttons, In Alphabetical Order\n\n------------------------------------------------------------------------------\n\n***********************\n* Summary Information *\n***********************\n\nThe main purpose of the Search Options window is to help you find assertions\n-- either axioms or theorems -- that can be used to justify a proof step. Or,\nto say it another way, to find assertions that are \'unifiable\'; where the\nproof step, including its Hyp entry, is an instance of each assertion.\n\nThis is called \'Step Search mode\'. In Step Search mode the requirement that\nevery search result is unifiable is implicit and applied automatically in\naddition to any other search criteria you specify.\n\nNuances of Step Search are explained in mmj2/doc/StepSearch.html (previously\nnamed StepSelectorSearch.html.)\n\nTo enter Step Search mode simply double-click a derivation proof step on the\nProof Asst GUI window, or position the cursor to a step and select \'Step\nSearch\' from the Search menu or the right-mouse button popup window. Step\nSearch goes directly to the Search Results window, initially bypassing Search\nOptions (though you can jump back to Search Options and refine your search.)\nAlternatively, you can select Search Options on the Proof Asst GUI window and\nif the cursor is positioned on a derivation proof step, the Search Options\nwindow is displayed in \'Step Search\' mode.\n\n\'General Search mode\' is the other modus operandi of Search Options. It is not\ntied to a particular proof step, or even to a particular theorem if you prefer\na \'global\' search of the Metamath database loaded into mmj2. General Search\nallows you to search for assertions, and to snoop around, in cases where you\nare, perhaps, still trying to develop a proof strategy.\n\nTo access General Search mode, select it from the Proof Asst GUI search menu\nor the right-mouse button popup menu, or position the cursor anywhere other\nthan a derivation proof step and select the \'Search Options\' menu item. You\ncan also initiate a new search on the Search Options window -- which will be,\nby definition, a General Search.\n\nCertain search options are disabled in General Search mode: the Extended\nSearch Options, Substitutions, and Auto-Select.\n\n\n------------------------------------------------------------------------------\n\n*********************\n* Main Window Areas *\n*********************\n\n-------------\n| Title Bar |\n-------------\n\nDisplays either \'Step Search\' or \'General Search\', plus Theorem or Stmt, and\nLOC_AFTER which contain statement labels defining the upper bound of the\nsearch. LOC_AFTER applies only to new theorems and is an inclusive upper\nbound.\n\n\n---------------\n| Search Data |\n---------------\n\nConsists of the Text Separators fields plus four lines of search criteria. At\nstart-up the ForWhat Search Data fields are blank, but afterwards the contents\nof the Search Data fields are never changed by the program.\n\n* Text Separators are intended for use when you are searching for text that\ncontains \'OR\', single quotes or double quotes. Use \'$(\' or \'$)\' as single or\ndouble quote symbols to guarantee conflict-free searching (due to the\nspecifications in the Metamath.pdf.)\n\n* The four Search Data lines are optional, and a line with a blank ForWhat\nfield is ignored completely. Evaluation of the Search Data against assertions\nis performed line by line from top to bottom, and is halted as soon as truth\nor falsity can be determined. (This eliminates the need for parentheses but\nmay require some getting used to...)\n\n* Multiple search terms can be entered in a ForWhat field. They should be\nquote-enclosed. If \'OR\' is not specified between two search terms in a ForWhat\nfield the default operation \'AND\' is assumed. Evaluation is from left to right\nwithin ForWhat. Evaluation halts as soon as truth or falsity can be determined\n(again, eliminating the need for parentheses...)\n\n\n-------------------\n| Search Controls |\n-------------------\n\nConsists of Search Options that can be categorized (loosely) as Exclusion\nCriteria, Extended Search controls and Output Controls.\n\n* Exclusion Controls are search parameters (or arguments if you prefer) that\ncan be used to narrow the search range.\n\n* Extended Search is a somewhat quixotic algorithm to find your proofs for\nyou. It uses a depth 1.5 search and does two things: it examines the sorted,\noutput Search Results looking for assertions whose hypotheses are completely\nsatisfied by the given proof step hypotheses, and if necessary -- to fulfill\nits quota -- it automatically checks prior proof steps and assertions with no\nhypotheses to supply missing hypotheses.\n\n* Output Controls specify how the Search Results should be presented and how\nlong you are willing to wait for the search to complete :-) The \'Auto-Select\'\noption works (optimistically) in conjunction with Extended Search: the first\njustifying assertion with no missing hypotheses is used to automatically\nupdate the proof step on the Proof Worksheet (just another reason to be glad\nthat the proof asst. Gui has undo :-)\n\n------------------------------------------------------------------------------\n\n****************************\n* Input Fields And Buttons *\n****************************\n\n----------------\n| Auto-Select: |\n----------------\n\nIn Step Search mode, when Auto-Select is \'On\' the first completed search\nresult in the sorted Search Results is automatically selected to update the\nuser-designated proof step in the Proof Worksheet.\n\n\'Completed Search Result\' items have unifiable assertions whose hypotheses are\nfully satisfied by the Hyp field of the designated proof step -- I.E. no\nmissing hyps. For example, assume the assertion is ax-mp and it is unifiable\nwith proof step 3 of theorem xyz, for which the user specified Hyp field \'1,2\'\n(or \'2,1\', or \'1,2,?\', etc.) ...or... The Extended Search feature discovered\nsteps 1 and/or 2 as suitable hypotheses for ax-mp (in which case the user\ncould have specified the Hyp field as simply \'?\' -- or \'1,?\', or \'2,?\', or\n\'?,1\', or \'?,2\').\n\n\n---------\n| Bool: |\n---------\n\nBoolean operator connecting a Search Data line to the following line.\n\n* AND = assertion rejected unless both Search Data lines are satisfied.\n\n* OR = assertion rejected if neither Search Data line is satisfied.\n\n\n---------------------\n| ChapSecHierarchy: |\n---------------------\n\nThe purpose of the ChapSecHierarchy option is to preemptively eliminate\nirrelevant assertions from the Search Results:\n\n* If \'On\' the ChapSecHierarchy option restricts the search domain to\nassertions belonging to the defined hierarchy of Chapters or Sections.\n\n* Hierarchies are based on the proof relationships of theorems in a Chapter\nor Section to theorems and axioms defined in other Chapters or Sections --\nplus, by definition, for the convenience of Search Options users, a\nChapter or Section is always related to itself.\n\n\nThe options are are follows:\n\n* blank = turn off ChapSecHierarchy feature\n\n* Chap/Direct = Granularity of hierarchies is at the Metamath Chapter level;\n and hierarchies are restricted to direct proof relationships between\n Chapters.\n\n* Chap/Indir. = Granularity of hierarchies is at the Metamath Chapter level;\n and hierarchies include both direct and indirect proof relationships\n between Chapters.\n\n* Sec/Direct = Granularity of hierarchies is at the Metamath Section level;\n and hierarchies are restricted to direct proof relationships between\n Sections.\n\n* Sec/Indir. = Granularity of hierarchies is at the Metamath Section level;\n and hierarchies include both direct and indirect proof relationships\n between Sections.\n\n\nEither one or two hierarchies can be specified; if two are specified then\ntheir set union is used -- that is, a composite hierarchy is used.\n\n* Hierarchy 1 has as root (or apex) the Chapter or Section of the Theorem/\n Stmt/LOC_AFTER of the search;\n\n* Hierarchy 2 has as root the ThruChap or ThruSec Chapter or Section.\n\n\nThe FromChap, FromSec, ThruChap and ThruSec fields are used to \'clip\' the\nlower and upper endpoints hierarchy ranges:\n\n* The lower endpoint of the hierarcies\' range of Chapters or Sections is given\n by FromChap or FromSec, respectively; if both are blank then the low end of\n the hiararchies is the start of the database.\n\n* The upper endpoint of the hierarchies is given by the Chapter or Section of\n the Theorem/Stmt/LOC_AFTER and the ThruChap or ThruSec, whichever is lower.\n\n\nA global search, with blank Theorem/Stmt/LOC_AFTER, and blank ThruChap and\nThruSec effectively disables the ChapSecHierarchy option.\n\n\n-------------\n| Comments: |\n-------------\n\nIf \'On\', each assertion\'s Comment statement is displayed in the Search Results\neven if Comments were not part of the search criteria -- if they were,\nComments are displayed even if this option is \'Off\'.\n\nThe Comment displayed is the Metamath $( $) statement immediately preceding\nthe $a or $p statement of the assertion. $e Comments are never displayed (and\nin fact, cannot be searched.)\n\n\n----------------\n| DoubleQuote: |\n----------------\n\nDoubleQuote (and SingleQuote) let you change the character(s) you will use to\nquote-enclose search terms in the ForWhat fields.\n\nQuotes are necessary only if more than one search term is used in a single\nForWhat field.\n\nHint: \'$\' is guaranteed by the Metamath.pdf spec to never occur in a label of\nformula, while \'$(\' and \'$)\' cannot occur inside Comment statements.\n\n\n---------------\n| ExclLabels: |\n---------------\n\nThe purpose of ExclLabels: is to exclude assertions with labels matching\nthe given label specifications.\n\nThis option uses a superset of Metamath \'search\' command label format\nspecification:\n\n* Wildcard \'$*\' or \'*\' accepted, signifies 0 or more of any label character.\n\n* Wildcard \'$?\' or \'?\' ok, signifies 0 or 1 of any label character\n\n* mmj2 converts the ExclLabels search terms into Java Regular Expression\n(\'regex\') terms and \'compiles\' them -- taking due care to handle Metamath\nlabel symbol \'.\' as a quoted character in the compiled regex expression.\n\nSearch terms are delimited by either whitespace or commas (\',\') and are\nimplicitly OR\'ed. Examples: *OLD,ee* and *OLD EE* are valid.\n\nNote: two consecutive \'$\' characters are invalid by definition to outlaw\nproblems with recursive specifiers such as \'$$*?\' and \'$$*\' -- the program\nmakes one pass through the label specifier, left to right, and therefore\n\'$$*\' does not tranlate to \'*\', and is an error.\n\n\n-----------\n| Format: |\n-----------\n\nThere are five different search term formats.\n\nIMPORTANT TO KNOW: Formats \'Metamath\', \'RegExpr\' and \'CharStr\' operate\non \'normalized\' string versions of the underlying Metamath objects -- formulas,\ncomments, labels and RPN proof label lists. The \'normalized\' string\nconsists of the non-whitespace math, label and (lower-cased) Comment tokens\nseparated by single, individual space characters, \' \'.\n\nNOTE: Comment tokens are converted internally to lower-case for searching\npurposes, as are the Metamath and CharStr ForWhat search strings -- RegExpr\nForWhat search strings should be written to target lower-case Comment tokens.)\n\nThe other two Formats, \'ParseExpr\' and \'ParseStmt\' operate on syntactic\nparse trees (and so are restricted to formula objects...) When using these\nFormats the contents of the ForWhat field are parsed into syntax trees for\nuse in the searching process.\n\n* Metamath : very similar to the RegExpr format except that the Metamath\n Format uses the \'$?\' and \'$*\' wildcards instead of \'.?\' and \'.*\' --\n signifying 1 character of anything, and 0 or more characters or tokens of any\n value, respectively. When searching labels, \'$?\' and \'$*\' can be abbreviated\n to just \'?\' and \'*\'. (Note: Metamath Format ForWhat values are converted\n internally by mmj2 into RegExpr values, so you might see an error message\n talking about Regular Expression errors...) Also, Comment searches are not\n case sensitive.\n\n* RegExpr : uses the Java-defined version of regular expressions as defined at\n http://docs.oracle.com/javase/tutorial/essential/regex/index.html. The\n ForWhat value is \'compiled\' into Java Regular Expression object(s), and\n so must be valid according to the aforementioned Java specs.\n\n* CharStr : a character string search for at least one occurrence of the\n search term within the normalized character string version of the Metamath\n object. Comment searches are not case sensitive.\n\n* ParseExpr : a ParseExpr search term is parsed to construct a parse tree for\n the expression (may be any Metamath type, not just wff). The expression\'s\n parse tree is then used in a unification-like process to search for any\n occurrence of the ParseExpr in a formula parse tree. The precise match\n requirement is given by the Oper field -- please refer to the Oper help text\n for details. Note: ParseExpr search terms may not contain Work Variables.\n\n* ParseStmt : a ParseStmt search term is parsed to construct a parse tree for\n the statement (in set.mm it must be a wff). The statement\'s parse tree is\n then used in a unification-like process to search for a match with a formula\n parse tree. The precise match requirement is given by the Oper field --\n please refer to the Oper help text for details. Note: ParseExpr search terms\n may not contain Work Variables.\n\n\n------------\n| ForWhat: |\n------------\n\nThe ForWhat field is used to input one or more search terms on a search data\nlines.\n\nIMPORTANT TO KNOW: ForWhat is optional! Pressing \'Search\' with all ForWhat\nfields blank still produces a Search Result -- the contents of the input\nassertion list minus those rejected because of the Exclusion Criteria, or\nif in Step Search mode beccause unification failed.\n\n* If left blank that Search Data line is ignored.\n\n* Quotes are required if more than one search term is input in ForWhat.\n\n* If the ForWhat field begins with a SingleQuote or a DoubleQuote then the\ncontents of ForWhat must be a space-delimited list of quoted search terms,\noptionally interspersed with occurrences of the Or: field string (likely\nto be \'OR\').\n\n* Note: an empty-string search term is invalid.\n\n* If ForWhat does not begin with either a SingleQuote or a DoubleQuote then\nthe contents of ForWhat are taken to be a single, unquoted search term (which\nis still subject to further validation.)\n\n* \'OR\' or the value specified in the or field can be specified between any two\nForWhat search terms. \'AND\' is assumed if two search terms are not separated\nby an \'OR\'.\n\n* Evaluation of multiple search terms in ForWhat is performed from left to\nright with evaluation halting as soon as truth or falsity can be determined.\nParentheses are not used to change the evaluation order.\n\n* Search terms are validated according to the Format field specification at\nthe start of the search (i.e. not when you tab or cursor out of ForWhat after\ninput.) Errors, such as an invalid RegExpr, or a parse error in a ParseExpr or\nParseStmt produce an error message displayed in a popup message window.\n\n* Each ForWhat field has a pull-down list that provides the nine most recently\nsearched for values.\n\n* The precise meaning and format of search terms depends on the Format field\non the same line. Please refer to the Format help text for additional\ninformation.\n\n\n-------------\n| FromChap: |\n-------------\n\nFromChap specifies the (inclusive) low end of the range of Chapters input to\nthe search. Only assertions defined in the specified Chapter or later are\ninput.\n\nIf FromChap is blank then the low end of the range is the start of the\nMetamath database -- and FromSec is automatically set to blank.\n\nNote: FromChap and FromSec are also used to \'clip\' or restrict the range of\nthe hierarchy(s) used by the ChapSecHierarchy feature.\n\n\n------------\n| FromSec: |\n------------\n\nFromSec specifies the (inclusive) low end of the range of Sections within the\ncurrent FromChap Chapter input to the search. Only assertions defined in the\nspecified Chapter/Section or later are input.\n\nIf FromSec is blank then the low end of the range is the start of current\nFromChap Chapter, or the start of the Metamath database if FromChap is blank.\n\nNote: FromChap and FromSec are also used to \'clip\' or restrict the range of\nthe hierarchy(s) used by the ChapSecHierarchy feature.\n\n\n----------\n| Cancel |\n----------\n\nThe Cancel button terminates a long-running search, if possible.\n\n\n--------\n| Help |\n--------\n\nThe Help button displays the help window.\n\n\n-----------\n| InWhat: |\n-----------\n\nInWhat is a pulldown list field on each Search Data line that lets you specify\nwhich assertion types and associated Metamath statements will be searched\nusing the criteria given on the Search Data line:\n\n* $aep = axioms, theorems and associated (logical) hypotheses (not varHyps).\n* $ae = axioms and associated (logical) hypotheses (not varHyps).\n* $ap = axioms and theorems but not hypotheses.\n* $ep = theorems and associated (logical) hypotheses (not varHyps).\n* $a = axioms but not the associated hypotheses.\n* $e = just the logical hypotheses of axioms and theorems.\n* $p = theorems but not the associated hypotheses.\n* $= RPN proof label list on theorems.\n\nNote: the Comment statement immediately preceding each axiom and theorem is\nautomatically included and can be searched, but hypothesis Comments are not\navailable.\n\n\n------------------\n| MaxExtResults: |\n------------------\n\nThe number of completed Search Results to find.\n\n\'Completed Search Result\' items have unifiable assertions whose hypotheses are\nfully satisfied by the Hyp field of the designated proof step -- i.e. no\nmissing hyps.\n\nThe Extended Search feature is not run when MaxExtResults is zero -- or when\nthe regular search process finds at least MaxExtResults number of Completed\nSearch Results.\n\n\n------------\n| MaxHyps: |\n------------\n\nExcludes any assertion with more than \'MaxHyps\' number of logical hypotheses.\n\nNote: the input sorted assertion list is sorted by number of hyps and MObjSeq\nnumber. Skip-sequential processing is used in the search to access the list\nvery efficiently. Also, the Extended Search process first looks for assertions\nwith one missing hyp, then two missing hyps, etc. So, it is possible to reduce\nthe search elapsed time significantly by specifying MinHyps and MaxHyps,\nespecially if you are using Extended Search. If your searches are taking too\nlong or are timing out because of the MaxTime setting you can efficiently\nbreak up a search into ranges of hyps: e.g. 0 thru 2, 3 thru 3, 4 thru 4, etc.\nSomething like 95% of assertions in set.mm use 2 or fewer hyps, and the\nassertions with larger numbers of hyps are the ones most likely to cause the\ndreaded problem of Combinatorial Explosion of Possibilities leading to a\ntimeout.\n\n\n------------------\n| MaxIncompHyps: |\n------------------\n\nSpecifies the maximum number of incomplete hypotheses to be checked during\nExtended Search for a single assertion in the Search Results list.\n\nNote: setting this value greater than two risks the dreaded problem of\nCombinatorial Explosion of Possibilities :-)\n\n\n---------------\n| MaxResults: |\n---------------\n\nLimits the size of the Search Results list.\n\nNote: MaxResults is applied prior to sorting the output. This degrades the\nquality of the results but speeds up the search. For maximum quality set to\n999999.\n\n\n------------\n| MaxTime: |\n------------\n\nSpecifies the maximum number of seconds a search is allowed to run.\n\nA helpful \'timeout\' message provides the progress of the search at the time it\nwas terminated.\n\n\n------------\n| MinHyps: |\n------------\n\nExcludes any assertion with fewer than \'MaxHyps\' number of logical hypotheses.\n\n\n-----------------\n| MinProofRefs: |\n-----------------\n\nExcludes any assertion referenced in proofs fewer than MinProofRefs times.\n\nThe idea behind this option is that, for whatever reason, some theorems in a\nMetamath database are not useful or not intended to be used by other theorems.\nAnd, lemmas are typically used just once.\n\n\n--------\n| New: |\n--------\n\nThe New button lets you start a new search in General Search mode.\n\nYou will be prompted for a statement label. This is optional and will be used\nto set an exclusive upper range for the search, and to optionally designate\nthe root (apex) of a ChapSecHierarchy (to further narrow the search.)\n\n\n---------\n| Oper: |\n---------\n\nThe Search Data line Oper field lets you specify relational operators for the\nformat types ParseExpr and ParseStmt, and a boolean operator (blank or \'NOT\' )\nfor the other format types: Metamath, RegExpr and charstr.\n\nThe boolean operator \'NOT\' is the simplest to explain. If Oper = \'NOT\' then\nthe logical value of the ForWhat search evaluation is reversed. True becomes\nfalse, and vice-versa. For example, Oper = \'NOT\' and ForWhat = \'<->\' will be\nfalse if the formula (or Comment) actually does contain \'<->\'.\n\nThe ParseExpr and ParseStmt relational operators are more complicated.\n\nIn the descriptions below, \'x\' refers to the assertion\'s formula.\n\nParseStmt relational operator meanings:\n\n* \'<=\' means ForWhat is an instance of x.\n\n* \'=\' means ForWhat and x are equal except for variable names.\n\n* \'<\' means ForWhat is an instance of x but is not equal to it.\n\n* \'==\' means ForWhat and x are identical (equal including variable names).\n\n* \'>=\' means x is an instance of ForWhat.\n\n* \'>\' means x is an instance of ForWhat but is not equal to it.\n\n* \'<>\' means ForWhat is an instance of x, or x is an instance of ForWhat, but\n they are not equal ( \'=\' ) to each other.\n\nParseExpr relational operator meanings:\n\nNOTE: Variable Hypothesis sub-expressions are excluded from the searches\nbelow for Format type ParseExpr unless the ForWhat search term is a\nsimple variable. So instead of saying \'sub-expression\' below we could say\n\'syntactically matching sub-expression\' ...but for brevity, let\'s not...\n\n* \'<=\' means ForWhat is an instance of a sub-expression of x\n\n* \'=\' means ForWhat is equal to a sub-expression of x, except for variable\n names.\n\n* \'<\' means ForWhat is an instance of a sub-expression of x but is not\n equal to that sub-expression.\n\n* \'==\' means ForWhat is identical to a sub-expression of x (equal including\n variable names).\n\n* \'>=\' means a sub-expression of x is an instance of ForWhat.\n\n\n* \'>\' means a sub-expression of x is an instance of ForWhat but is not\n equal to ForWhat.\n\n* \'<>\' means ForWhat is an instance of a sub-expression of x but is not\n equal to that sub-expression...OR...a sub-expression of x is an\n instance of ForWhat but is not equal to ForWhat.\n\n-------\n| OR: |\n-------\n\nOR enables you to specify an alternative to the logical \'OR\' operator in the\nForWhat fields when multiple search terms are used.\n\nBy default, if no logical operator separates two search terms the \'AND\'\noperator is assumed (only \'OR\' and \'AND\' are valid, though the Oper field\ncontains a \'NOT\' option that applies to the entire ForWhat field.)\n\nNote: evaluation within a ForWhat field is left-to-right, with evaluation\nstopping as soon as truth or falsity is determined -- e.g. evaluation of the\nterms to the right of an OR is not performed if evaluation of the terms to the\nleft of the OR yields true.\n\n---------------\n| OutputSort: |\n---------------\n\nThis is a pulldown list that allows the user to select the sort sequence of\nthe output Search Results list.\n\nThe sort key field choices are listed in major to minor order. Minor sort keys\nonly come into play when two items are being compared if all of the more major\nsort keys are equal.\n\nIf not otherwise mentioned, field sort sequence is ascending order. Descending\norder is indicated with \'(d)\' suffixing the field name.\n\nThe sort key fields are:\n\n* Complexity = combination of two fields: ParseDepth and FormulaLength.\n Combined here to simplify usage and documentation. \'Complexity(d)\' means\n ParseDepth(d) followed by FormulaLength(d). ParseDepth = assertion\'s\n conclusion\'s formula\'s parse tree depth. Corresponds roughly to formula\n complexity and hence, specificity. Because in standard practice the\n designated proof step has already been unified with each assertion in the\n Search Results list, a greater parse depth corresponds to a higher degree of\n similarity -- and hence, increased likelihood of usefulness in the\n designated proof step. FormulaLength = assertion\'s conclusion\'s formula\n length (in tokens, not characters). Corresponds roughly to formula\n complexity.\n\n* Label = Assertion statement label.\n\n* MObjSeq = Metamath object sequence number: corresponds to position within\n the input Metamath file. A higher number indicates a more advanced assertion\n which may be more desirable in a proof step.\n\n* Nbr Hyps = number of logical hypotheses in assertion. Fewer hypotheses tends\n to result in shorter proofs. Approximately 95% of set.mm assertions have two\n or fewer hypotheses.\n\n* Popularity = number of times assertion used in proofs of other assertions.\n\n* Score = this is a ranking number based on the Search Results and search\n controls/criteria:\n\n000 = Assertion not selected (initial score value)\n\n050 = Assertion satisfies search criteria, if any, but is not a Completed\n Search Result.\n\n100 = Assertion is a Completed Search Result: it unifies with the designated\n proof step and there are no missing hypotheses.\n\n\n------\n| PA |\n------\n\nThe PA button \'jumps\' you to the Proof Asst GUI window.\n\n\n---------\n| Part: |\n---------\n\nThe Search Data line field Part lets you specify which part of the Metamath\nstatement is to be searched: Formulas, Comments, Labels and LabelsRPN.\n\n---------------------\n| PrevStepsChecked: |\n---------------------\n\nPrevStepsChecked specifies the maximum number of previous proof steps to be\nchecked in the Extended Search. In other words, this lets you control how far\nback in the proof you want the Extended Search to look for hypotheses for the\ncurrent step.\n\nThis number does not include previous steps that are bypassed because\nReuseDerivSteps is \'Off\'.\n\nThe motivation for this option is that in a long proof with, say, 100 steps,\nif the current proof step has two missing hypotheses then up to 10,000 trial\nunifications might be needed...for each assertion in the Search Results!\n\n\n----------\n| Refine |\n----------\n\nRefine the prior search by using the prior Search Results as input to a search\nusing the current search option settings.\n\nThis is a very powerful feature!\n\n\n-----------------\n| ResetControls |\n-----------------\n\nThe ResetControls button resets the Search Control fields to the default\nsettings.\n\nSee also: SetDef button.\n\n\n-------------\n| ResetData |\n-------------\n\nThe ResetData button resets the Search Data fields to the default settings.\n\nSee also: SetDef button.\n\n\n-------------------\n| ResultsChecked: |\n-------------------\n\nRestricts the Extended Search input to the first ResultsChecked number of\n(sorted) Search Results.\n\nAlthough setting ResultsChecked to a large number might improve the chances\nthat Extended Search will be successful, the amount of work performed by the\nExtended Search is significant and potentially very time-consuming, so you may\nneed to adjust the MaxTime control to prevent timeouts.\n\n\n--------------------\n| ReuseDerivSteps: |\n--------------------\n\nIf \'Off\', previous proof derivation steps (this excludes the theorem\'s\nhypotheses,) which have already been referenced in a prior derivation step\nwill not be checked in the Extended Search.\n\nThe idea of this is that many proofs do not reuse derivations, so steps that\nhave already been referenced need not be checked in the Extended Search.\n\nFor long proofs the problem of Combinatorial Explosion of Possibilities may be\ndramatically reduced when ReuseDerivSteps is \'Off\'. For example, in a long\nproof with, say, 100 steps, if the current proof step has two missing\nhypotheses then up to 10,000 trial unifications might be needed...for each\nassertion in the Search Results!\n\nBecause some proofs do require reuse of derivations, the user can input a\nspecial mmj2 Proof Worksheet Comment statement immediately prior to a\nderivation step, specifying \'<so:reuse>\' as the first non-blank token after\nthe \'*\' in column 1. This special Comment designates the following derivation\nstep as a candidate for reuse even though ReuseDerivSteps is \'Off\'.\n\n\n----------\n| Search |\n----------\n\nThe Search button initiates the search. Unless there are errors the Search\nResults window will be displayed.\n\n\n----------\n| SetDef |\n----------\n\nThe SetDef button stores the current values of the SearchData and\nSearchControls fields as the defaults. You can then use the ResetData and\nResetControls buttons to reset the window data.\n\nNote: the follow-on project to Release 20121225 will provide Persistent\nStorage Of User Preferences, which will include your chosen Search Options\ndefaults. Until then, the customized defaults are only retained until mmj2 is\nexited.\n\n\n----------------\n| SingleQuote: |\n----------------\n\nSingleQuote (and DoubleQuote) let you change the character(s) you will use to\nquote-enclose search terms in the ForWhat fields.\n\nQuotes are necessary only if more than one search term is used in a single\nForWhat field.\n\nHint: \'$\' is guaranteed by the Metamath.pdf spec to never occur in a label of\nformula, while \'$(\' and \'$)\' cannot occur inside Comment statements.\n\n\n------\n| SR |\n------\n\nThe SR button \'jumps\' you to the Search Results window without executing a\nsearch.\n\n\n----------\n| Stats: |\n----------\n\nStats controls output of various statistics to the request messages window\nabout each search :\n\n* Stats = 0 means no Stats output\n* Stats = 1 means print Summary Statistics\n* Stats = 2 print prior levels plus Detailed Statistics\n* Stats = 3 print prior levels plus Search Arguments\n* Stats = 4 print prior levels plus Search Results\n* Stats >=5 print prior levels plus Chap/Sec Hierarchy used\n\n\n------------------\n| Substitutions: |\n------------------\n\nIn Step Search mode, if Substitutions is \'On\', formulas are shown in the\nSearch Results window with unification substitutions (from the Proof Worksheet\ninto the assertion and its hypotheses).\n\nIf \'Off\', assertion formulas are shown without substitutions, just as they\nexist in the input Metamath database.\n\n\n-------------\n| ThruChap: |\n-------------\n\nThruChap specifies the (inclusive) high end of the range of Chapters input to\nthe search. Only assertions defined in the specified Chapter or before are\ninput.\n\nIf ThruChap is blank then the high end of the range is the end of the Metamath\ndatabase -- or the Theorem/Stmt/LOC_AFTER position, whichever is lower. Also,\nif ThruChap is blank then ThruSec is automatically set to blank.\n\nNote: ThruChap and ThruSec, if not both blank, specify the root (apex) of one\nof the hierarchies used by the ChapSecHierarchy feature.\n\n\n------------\n| ThruSec: |\n------------\n\nThruSec specifies the (inclusive) high end of the range of Sections within the\ncurrent ThruChap Chapter input to the search. Only assertions defined in the\nspecified Chapter/Section or before are input.\n\nIf ThruSec is blank then the high end of the range is the end of the current\nThruChap Chapter -- or the Theorem/Stmt/LOC_AFTER position, whichever is\nlower.\n\nNote: ThruChap and ThruSec, if not both blank, specify the root (apex) of one\nof the hierarchies used by the ChapSecHierarchy feature.\n\n------------------------------------------------------------------------------\n\n****The End!****\n" |
public static final java.lang.String |
GENERAL_SEARCH_TITLE_LITERAL_1 |
"General Search: Options - " |
public static final java.lang.String |
GUI_EDIT_MENU_COPY_ITEM_TEXT |
"Copy" |
public static final java.lang.String |
GUI_EDIT_MENU_CUT_ITEM_TEXT |
"Cut" |
public static final java.lang.String |
GUI_EDIT_MENU_PASTE_ITEM_TEXT |
"Paste" |
public static final int |
HELP_BUTTON_ID |
7 |
public static final int |
IN_WHAT_0_FIELD_ID |
3 |
public static final int |
IN_WHAT_1_FIELD_ID |
9 |
public static final int |
IN_WHAT_2_FIELD_ID |
15 |
public static final int |
IN_WHAT_3_FIELD_ID |
21 |
public static final int |
IN_WHAT_A_ID |
4 |
public static final int |
IN_WHAT_AE_ID |
1 |
public static final int |
IN_WHAT_AEP_ID |
0 |
public static final int |
IN_WHAT_AP_ID |
2 |
public static final int |
IN_WHAT_E_ID |
5 |
public static final int |
IN_WHAT_EP_ID |
3 |
public static final int |
IN_WHAT_EQ_ID |
7 |
public static final int |
IN_WHAT_P_ID |
6 |
public static final int |
IN_WHAT_TYPE_HYP |
1 |
public static final int |
IN_WHAT_TYPE_STATEMENT |
0 |
public static final int |
IN_WHAT_TYPE_SUB_STATEMENT |
2 |
public static final java.lang.String |
IN_WHAT_VALUE_A |
"$a" |
public static final java.lang.String |
IN_WHAT_VALUE_AE |
"$ae" |
public static final java.lang.String |
IN_WHAT_VALUE_AEP |
"$aep" |
public static final java.lang.String |
IN_WHAT_VALUE_AP |
"$ap" |
public static final java.lang.String |
IN_WHAT_VALUE_E |
"$e" |
public static final java.lang.String |
IN_WHAT_VALUE_EP |
"$ep" |
public static final java.lang.String |
IN_WHAT_VALUE_EQ |
"$=" |
public static final java.lang.String |
IN_WHAT_VALUE_P |
"$p" |
public static final int |
MAX_EXT_RESULTS_FIELD_ID |
32 |
public static final int |
MAX_FOR_WHAT_PRIOR_VALUES |
9 |
public static final int |
MAX_HYPS_FIELD_ID |
34 |
public static final int |
MAX_INCOMP_HYPS_FIELD_ID |
35 |
public static final int |
MAX_RESULTS_FIELD_ID |
37 |
public static final int |
MAX_TIME_FIELD_ID |
30 |
public static final int |
MIN_HYPS_FIELD_ID |
31 |
public static final int |
MIN_PROOF_REFS_FIELD_ID |
28 |
public static final int |
MINUS_BUTTON_ID |
9 |
public static final int |
NBR_BUTTONS |
12 |
public static final int |
NBR_SEARCH_DATA_ROWS |
4 |
public static final int |
NEW_BUTTON_ID |
2 |
public static final int |
OPER_0_FIELD_ID |
6 |
public static final int |
OPER_1_FIELD_ID |
12 |
public static final int |
OPER_2_FIELD_ID |
18 |
public static final int |
OPER_3_FIELD_ID |
24 |
public static final int |
OPER_TYPE_NOT_TREE |
2 |
public static final int |
OPER_TYPE_SUB_TREE |
1 |
public static final int |
OPER_TYPE_TREE |
0 |
public static final java.lang.String |
OPER_VALUE_EMPTY_STRING |
"" |
public static final int |
OPER_VALUE_EMPTY_STRING_ID |
0 |
public static final java.lang.String |
OPER_VALUE_EQ |
"=" |
public static final java.lang.String |
OPER_VALUE_EQ_EQ |
"==" |
public static final int |
OPER_VALUE_EQ_EQ_ID |
5 |
public static final int |
OPER_VALUE_EQ_ID |
4 |
public static final java.lang.String |
OPER_VALUE_GE |
">=" |
public static final int |
OPER_VALUE_GE_ID |
6 |
public static final java.lang.String |
OPER_VALUE_GT |
">" |
public static final int |
OPER_VALUE_GT_ID |
7 |
public static final java.lang.String |
OPER_VALUE_LE |
"<=" |
public static final int |
OPER_VALUE_LE_ID |
2 |
public static final java.lang.String |
OPER_VALUE_LT |
"<" |
public static final java.lang.String |
OPER_VALUE_LT_GT |
"<>" |
public static final int |
OPER_VALUE_LT_GT_ID |
8 |
public static final int |
OPER_VALUE_LT_ID |
3 |
public static final java.lang.String |
OPER_VALUE_NOT |
"NOT" |
public static final int |
OPER_VALUE_NOT_ID |
1 |
public static final int |
OR_SEPARATOR_FIELD_ID |
0 |
public static final java.lang.String |
OUTPUT_LABEL_TEXT |
" -------Output Controls-------" |
public static final java.lang.String |
OUTPUT_LABEL_TOOL_TIP |
"Controls search output processing." |
public static final int |
OUTPUT_SORT_FIELD_ID |
47 |
public static final int |
PA_BUTTON_ID |
5 |
public static final int |
PART_0_FIELD_ID |
4 |
public static final int |
PART_1_FIELD_ID |
10 |
public static final int |
PART_2_FIELD_ID |
16 |
public static final int |
PART_3_FIELD_ID |
22 |
public static final int |
PART_COMMENTS_ID |
1 |
public static final int |
PART_FORMULAS_ID |
0 |
public static final int |
PART_LABELS_ID |
2 |
public static final int |
PART_LABELS_RPN_ID |
3 |
public static final int |
PART_TYPE_FORMULA |
0 |
public static final int |
PART_TYPE_NOT_FORMULA |
1 |
public static final java.lang.String |
PART_VALUE_COMMENTS |
"Comments" |
public static final java.lang.String |
PART_VALUE_FORMULAS |
"Formulas" |
public static final java.lang.String |
PART_VALUE_LABELS |
"Labels" |
public static final java.lang.String |
PART_VALUE_LABELS_RPN |
"LabelsRPN" |
public static final int |
PLUS_BUTTON_ID |
8 |
public static final java.lang.String |
POPUP_ERROR_MESSAGE_TITLE |
"Search Error" |
public static final int |
PREV_STEPS_CHECKED_FIELD_ID |
38 |
public static final int |
REFINE_BUTTON_ID |
3 |
public static final int |
RESET_CONTROLS_BUTTON_ID |
11 |
public static final int |
RESET_DATA_BUTTON_ID |
10 |
public static final int |
RESULTS_CHECKED_FIELD_ID |
29 |
public static final int |
REUSE_DERIV_STEPS_FIELD_ID |
41 |
public static final int |
SEARCH_BUTTON_ID |
0 |
public static final java.lang.String |
SEARCH_CONTROLS_LABEL_TEXT |
"SEARCH_CONTROLS " |
public static final java.lang.String |
SEARCH_DATA_LABEL_TEXT |
"SEARCH_DATA " |
public static final java.lang.String |
SEARCH_OPTIONS_ERROR_TITLE |
"Search Options Error" |
public static final int |
SET_DEF_BUTTON_ID |
4 |
public static final int |
SINGLE_QUOTE_FIELD_ID |
1 |
public static final int |
SR_BUTTON_ID |
6 |
public static final int |
STATS_0_ID |
0 |
public static final int |
STATS_1_ID_SUMMARY_STATS |
1 |
public static final int |
STATS_2_ID_DETAILED_STATS |
2 |
public static final int |
STATS_3_ID_SEARCH_ARGS |
3 |
public static final int |
STATS_4_ID_SEARCH_RESULTS |
4 |
public static final int |
STATS_5_ID_CHAP_SEC_HIERARCHY |
5 |
public static final int |
STATS_FIELD_ID |
42 |
public static final java.lang.String |
STEP_SEARCH_TITLE_LITERAL_1 |
"Step Search: Options - " |
public static final java.lang.String |
STEP_SEARCH_TITLE_STEP_LITERAL |
"Step " |
public static final int |
SUBSTITUTIONS_FIELD_ID |
33 |
public static final java.lang.String |
TEXT_SEPARATORS_LABEL_TEXT |
" Text-Separators:" |
public static final int |
THRU_CHAP_FIELD_ID |
45 |
public static final int |
THRU_SEC_FIELD_ID |
46 |
public static final java.lang.String |
TITLE_LOC_AFTER_LITERAL |
" LOC_AFTER=" |
public static final java.lang.String |
TITLE_STMT_LITERAL |
" Stmt " |
public static final java.lang.String |
TITLE_THEOREM_LITERAL |
" THEOREM=" |
public static final java.lang.String |
TOOL_TIP_AUTO_SELECT |
"AutoSelect: Automatically updates proof step using the first Completed Search Result in the Search Results List." |
public static final java.lang.String |
TOOL_TIP_BOOL |
"Bool: Logical operator (AND, OR, XOR, NAND) connecting Search Data lines (evaluation order = top to bottom.)" |
public static final java.lang.String |
TOOL_TIP_CANCEL |
"Cancel the search." |
public static final java.lang.String |
TOOL_TIP_CHAP_SEC_HIERARCHY |
"ChapSecHierarchy: restricts search domain to hierarchies of related Chapters or Sections of the FromChap/FromSec and the Theorem or Stmt/LOC_AFTER being searched." |
public static final java.lang.String |
TOOL_TIP_COMMENTS |
"Comments: causes assertion comments to be displayed in the Step Selector Dialog even if comments are not being searched." |
public static final java.lang.String |
TOOL_TIP_DOUBLE_QUOTE |
"DoubleQuote: Character string used to quote-enclose search arguments" |
public static final java.lang.String |
TOOL_TIP_EXCL_LABELS |
"ExclLabels: Comma-delimited, Metamath search expression(s) to specify assertion labels to exclude from the Search Results (e.g. \'*OLD,ee*\')" |
public static final java.lang.String |
TOOL_TIP_FOR_WHAT |
"ForWhat: search terms, optionally quote-enclosed. ANDed together by default unless OR specified. Pulldown list has 9 prior search values for the given Format. See Help." |
public static final java.lang.String |
TOOL_TIP_FORMAT |
"Format: object format used in search matching process." |
public static final java.lang.String |
TOOL_TIP_FROM_CHAP |
"FromChap: Optional. Specifies a lower bound Chapter of the search domain on the input assertion list." |
public static final java.lang.String |
TOOL_TIP_FROM_SEC |
"FromSec: Optional. Specifies a lower bound Section of the search domain on the input assertion list." |
public static final java.lang.String |
TOOL_TIP_HELP |
"Display Help for Search Options." |
public static final java.lang.String |
TOOL_TIP_IN_WHAT |
"InWhat: the Metamath statements to be searched for each input Assertion." |
public static final java.lang.String |
TOOL_TIP_MAX_EXT_RESULTS |
"MaxExtResults: number of Completed Search Results to find. You may be lucky to get one! Zero = disable Ext. Search." |
public static final java.lang.String |
TOOL_TIP_MAX_HYPS |
"MaxHyps: Maximum number of logical hypotheses in assertions included in the search domain." |
public static final java.lang.String |
TOOL_TIP_MAX_INCOMP_HYPS |
"MaxIncompHyps: Specifies the maximum number of incomplete hypotheses in Search Result items input to the Extended Search." |
public static final java.lang.String |
TOOL_TIP_MAX_RESULTS |
"MaxResults: Limits the size of the Search Results List." |
public static final java.lang.String |
TOOL_TIP_MAX_TIME |
"MaxTime: Maximum elapsed time (seconds) of the search." |
public static final java.lang.String |
TOOL_TIP_MIN_HYPS |
"MinHyps: Minimum number of logical hypotheses in assertions included in the search domain." |
public static final java.lang.String |
TOOL_TIP_MIN_PROOF_REFS |
"MinProofRefs: Minimum number of times assertion referenced in other proofs in order to be included in the search domain." |
public static final java.lang.String |
TOOL_TIP_MINUS |
"Decrease Font Size For Search Options." |
public static final java.lang.String |
TOOL_TIP_NEW |
"Begin a new search." |
public static final java.lang.String |
TOOL_TIP_OPER |
"Oper: Lets you specify relational operators for the Format types ParseExpr and ParseStmt, and boolean operators (blank or \'NOT\' ) for all other Format types. See Help." |
public static final java.lang.String |
TOOL_TIP_OR |
"Or: Character string used to specify logical OR between two ForWhat search terms. AND is the default operator for consecutive search terms if OR not specified." |
public static final java.lang.String |
TOOL_TIP_OUTPUT_SORT |
"OutputSort: Sort order of the Search Results List. (D) signifies descending order, otherwise ascending is used." |
public static final java.lang.String |
TOOL_TIP_PA |
"Jump to the Proof Assistant window (without searching.)" |
public static final java.lang.String |
TOOL_TIP_PART |
"Part: the part of the Metamath statements to be searched." |
public static final java.lang.String |
TOOL_TIP_PLUS |
"Increase Font Size For Search Options." |
public static final java.lang.String |
TOOL_TIP_PREV_STEPS_CHECKED |
"PrevStepsChecked: Specifies the maximum number of previous proof steps to be checked in the Extended Search not including steps bypassed if ReuseDerivSteps: = False." |
public static final java.lang.String |
TOOL_TIP_REFINE |
"Refine the prior search using its Search Results as input." |
public static final java.lang.String |
TOOL_TIP_RESET_CONTROLS |
"Reset the Search Control fields to the default settings." |
public static final java.lang.String |
TOOL_TIP_RESET_DATA |
"Reset the Search Data fields to the default settings." |
public static final java.lang.String |
TOOL_TIP_RESULTS_CHECKED |
"ResultsChecked: number of (sorted) Search Results input to the Extended Search. Zero = disable Ext. Search." |
public static final java.lang.String |
TOOL_TIP_REUSE_DERIV_STEPS |
"ReuseDerivSteps: Previous proof steps already referenced in the proof (as Hyps) will not be reused in the current step by the Extended Search -- unless first Comment token = <SO:REUSE>. See Help." |
public static final java.lang.String |
TOOL_TIP_SEARCH |
"Run the search!" |
public static final java.lang.String |
TOOL_TIP_SET_DEF |
"Set defaults to current Search Data/Control values (except ForWhat:)" |
public static final java.lang.String |
TOOL_TIP_SINGLE_QUOTE |
"SingleQuote: Character string used to quote-enclose search arguments" |
public static final java.lang.String |
TOOL_TIP_SR |
"Jump to the Search Results window (without searching.)" |
public static final java.lang.String |
TOOL_TIP_STATS |
"Stats: Causes statistics about each search to be produced and output to the Request Message window." |
public static final java.lang.String |
TOOL_TIP_SUBSTITUTIONS |
"Substitutions: Causes unifiable assertions to be displayed in the Step Selector Search Dialog with unification substitutions from the Proof Worksheet (instead of as-is.)" |
public static final java.lang.String |
TOOL_TIP_THRU_CHAP |
"ThruChap: Optional. Specifies an upper bound Chapter of the search domain on the input assertion list." |
public static final java.lang.String |
TOOL_TIP_THRU_SEC |
"ThruSec: Optional. Specifies a upper bound Section of the search domain on the input assertion list." |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final int |
APPLY_BUTTON_ID |
0 |
public static final int |
CANCEL_BUTTON_ID |
1 |
public static final java.lang.String |
DEFAULT_TITLE |
"Search Results, General Search R20121225 @ 20-Sep-2012 20:54" |
public static final java.lang.String |
ERRMSG_BUTTON_ATTR_TABLE_LOAD_ERROR |
"A-SR-0103 SearchResultsConstants.BUTTON_ATTR[i].buttonId not equal to " |
public static final java.lang.String |
ERRMSG_FIELD_ATTR_TABLE_LOAD_ERROR |
"A-SR-0101 SearchResultsConstants.FIELD_ATTR[i].fieldId not equal to " |
public static final java.lang.String |
ERRMSG_UNRECOGNIZED_BUTTON_ID_1 |
"A-SR-0201 Unrecognized Button pressed. buttonId = " |
public static final java.lang.String |
GENERAL_HELP_FRAME_TITLE |
"SearchResults Help: General Information, R20121225 @ 20-Sep-2012 20:54" |
public static final java.lang.String |
GENERAL_HELP_INFO_TEXT |
"************\n* Contents *\n************\n\n* Summary Information About The Search Results Window\n\n* Main Window Areas Explanation\n\n* Input Fields And Buttons, In Alphabetical Order\n\n------------------------------------------------------------------------------\n\n***********************\n* Summary Information *\n***********************\n\nThe Search Results window displays the sorted list of assertions selected by\nthe most recent Search.\n\nThe list is \'selectable\'. You can \'Apply\' a selected list item to a derivation\nproof step, or you can \'right-mouse\' popup a formatted display of the selected\nitem for easier viewing. You must be in \'Step Search mode\' to use the \'Apply\'\nfeature -- the \'Apply\' button is disabled in \'General Search mode\'.)\n\nTo re-sort the Search Results, click the \'SO\' button to return to the Search\nOptions window, then choose a new Output Sort and click the \'Refine\' button.\nThis is very fast because \'Refine\' reads just the assertions in the Search\nResults!\n\nIt is similarly convenient to change any of the other arguments on the Search\nOptions window, and then either Refine the previous search or Search again.\n\n\nNOTE: For convenience, due to an issue with code settings for the Search\nResults selection \'pane\', please use the following RunParms with any desired\ncustomizations to effect your preferred size settings (as opposed to attempting\nmanual adjustments by \'dragging\' the window edges):\n\nStepSelectorDialogPaneWidth,720\nStepSelectorDialogPaneHeight,440\n\n\n------------------------------------------------------------------------------\n\n*********************\n* Main Window Areas *\n*********************\n\n-------------\n| Title Bar |\n-------------\n\nDisplays either \'Step Search\' or \'General Search\', plus Theorem or Stmt, and\nLOC_AFTER which contain statement labels defining the upper bound of the\nsearch. LOC_AFTER applies only to new theorems and is an inclusive upper\nbound.\n\n\n---------------------------------\n| Search Results Selection List |\n---------------------------------\n\nThe Search Results Selection List is a sorted list of assertions selected by\nthe most recent Search. For each assertion one line of output is displayed\nfor each of:\n\n* The assertion\'s descriptive Metamath Comment statement, if the \'Comments\'\nSearch Option is checked (On).\n\n* The assertion\'s logical hypotheses, if any.\n\n* The assertion\'s conclusion formula.\n\n\nOf special note about each assertion\'s group selection lines:\n\n* \'(*)\' prefixes the first line if the assertion is a \'Completed Search\nResult\', which means that the assertion unifies with the derivation proof\nstep on the Proof Asst GUI window and that there are no incomplete hypotheses\n-- and thus, the step is \'complete\' (though it may still contain Work\nVariables.)\n\n* If the \'Substitutions\' Search Option is checked (On), then in Step\nSearch mode the assertion formulas are displayed with the unification\nsubstitutions obtained from the originally designated derivation proof step.\nOtherwise, if \'Substitutions\' is un-checked, the assertion formulas are\nshown as-is, the way they appear in the Metamath database.\n\n* If Work Variables were assigned during unification, the specific\nWork Variables shown may be changed when the selection is \'Apply\'ed\nto the derivation proof step.\n\n\nNote: for all Search Option \'OutputSort\' choices except the first, #0,\nCompleted Search Result lines appear first in the Search Results Selection\nList (because they are assigned a Score = 100, the highest defined value.)\n\n\n------------------------------------------------------------------------------\n\n****************************\n* Input Fields And Buttons *\n****************************\n\n---------\n| Apply |\n---------\n\nThe Apply button updates the originally designated derivation proof\nstep for Step Search mode. The selected assertion\'s label updates\nthe \'Ref\' field on the proof step and then unification of the\nProof Worksheet is performed.\n\n----------\n| Cancel |\n----------\n\nThe Cancel button terminates a long-running search, if possible.\n\n\n--------\n| Help |\n--------\n\nThe Help button displays the help window.\n\n\n------\n| PA |\n------\n\nThe PA button \'jumps\' you to the Proof Asst GUI window.\n\n\n------\n| SO |\n------\n\nThe SO button \'jumps\' you to the Search Options window without affecting\nthe contents of the Search Results window.\n\n------------------------------------------------------------------------------\n\n" |
public static final java.lang.String |
GENERAL_SEARCH_TITLE_LITERAL_1 |
"General Search: Results - " |
public static final java.lang.String |
GUI_EDIT_MENU_COPY_ITEM_TEXT |
"Copy" |
public static final java.lang.String |
GUI_EDIT_MENU_CUT_ITEM_TEXT |
"Cut" |
public static final java.lang.String |
GUI_EDIT_MENU_PASTE_ITEM_TEXT |
"Paste" |
public static final int |
HELP_BUTTON_ID |
4 |
public static final int |
MINUS_BUTTON_ID |
6 |
public static final int |
NBR_BUTTONS |
7 |
public static final int |
PA_BUTTON_ID |
2 |
public static final int |
PLUS_BUTTON_ID |
5 |
public static final java.lang.String |
POPUP_ERROR_MESSAGE_TITLE |
"Search Error" |
public static final java.lang.String |
SEARCH_RESULTS_ERROR_TITLE |
"Search Results Error" |
public static final java.lang.String |
SEARCH_RESULTS_POPUP_APPLY_BUTTON_CAPTION |
"Apply Selection To Step And Unify Proof?" |
public static final java.lang.String |
SEARCH_RESULTS_POPUP_SELECTION_CAPTION |
"Selected Line" |
public static final int |
SEARCH_SELECTION_FIELD_ID |
0 |
public static final java.lang.String |
SELECTION_NO_SEARCH_RUN_YET_LITERAL |
"I-SR-0301 Search not yet run." |
public static final int |
SO_BUTTON_ID |
3 |
public static final java.lang.String |
STEP_SEARCH_TITLE_LITERAL_1 |
"Step Search: Results - " |
public static final java.lang.String |
STEP_SEARCH_TITLE_STEP_LITERAL |
"Step " |
public static final java.lang.String |
TITLE_LOC_AFTER_LITERAL |
" LOC_AFTER " |
public static final java.lang.String |
TITLE_STMT_LITERAL |
" Stmt " |
public static final java.lang.String |
TITLE_THEOREM_LITERAL |
" Theorem " |
public static final java.lang.String |
TOOL_TIP_APPLY |
"Apply selection to derivation proof step." |
public static final java.lang.String |
TOOL_TIP_CANCEL |
"Cancel the running process." |
public static final java.lang.String |
TOOL_TIP_HELP |
"Display Help for Search Results." |
public static final java.lang.String |
TOOL_TIP_MINUS |
"Decrease Font Size For Search Results." |
public static final java.lang.String |
TOOL_TIP_PA |
"Jump to the Proof Assistant window (without searching.)" |
public static final java.lang.String |
TOOL_TIP_PLUS |
"Increase Font Size For Search Results." |
public static final java.lang.String |
TOOL_TIP_SEARCH_SELECTION |
"Select assertion to Apply to derivation step." |
public static final java.lang.String |
TOOL_TIP_SO |
"Jump to the Search Options window." |
Modifier and Type | Constant Field | Value |
---|---|---|
protected final int |
fieldId |
0 |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
NS |
"SM" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
NS |
"TL" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final int |
DEFAULT_DV_SRC_STMT_LIST_SIZE |
3 |
public static final int |
DEFAULT_LOG_HYP_SRC_STMT_LIST_SIZE |
3 |
public static final java.lang.String |
FILE_SUFFIX_MMT |
".mmt" |
public static final int |
FILE_WRITER_BUFFER_SIZE |
4096 |
public static final java.lang.String |
SYNONYM_FALSE_1 |
"false" |
public static final java.lang.String |
SYNONYM_FALSE_2 |
"off" |
public static final java.lang.String |
SYNONYM_FALSE_3 |
"no" |
public static final java.lang.String |
SYNONYM_TRUE_1 |
"true" |
public static final java.lang.String |
SYNONYM_TRUE_2 |
"on" |
public static final java.lang.String |
SYNONYM_TRUE_3 |
"yes" |
public static final boolean |
THEOREM_LOADER_AUDIT_MESSAGES_DEFAULT |
true |
public static final boolean |
THEOREM_LOADER_STORE_FORMULAS_ASIS_DEFAULT |
true |
public static final int |
THEOREM_LOADER_STORE_MM_INDENT_AMT_DEFAULT |
2 |
public static final int |
THEOREM_LOADER_STORE_MM_INDENT_AMT_MAX |
9 |
public static final int |
THEOREM_LOADER_STORE_MM_INDENT_AMT_MIN |
0 |
public static final int |
THEOREM_LOADER_STORE_MM_RIGHT_COL_DEFAULT |
79 |
public static final int |
THEOREM_LOADER_STORE_MM_RIGHT_COL_MAX |
9999 |
public static final int |
THEOREM_LOADER_STORE_MM_RIGHT_COL_MIN |
70 |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
ERRMSG_ALT_FORMAT_NBR_MISSING2_1 |
"A-TM-0306 TMFFAltFormat Format Number not input!" |
public static final java.lang.String |
ERRMSG_ALT_INDENT_MISSING2_1 |
"A-TM-0310 TMFFAltIndent Alt Indent amount not input!" |
public static final java.lang.String |
ERRMSG_BAD_ALT_FORMAT_NBR_1 |
"A-TM-0307 Input alt format number = " |
public static final java.lang.String |
ERRMSG_BAD_ALT_FORMAT_NBR_2 |
" is invalid. Must be within the range of 0 and " |
public static final java.lang.String |
ERRMSG_BAD_ALT_INDENT_1 |
"A-TM-0311 Input Alt Indent amount = " |
public static final java.lang.String |
ERRMSG_BAD_ALT_INDENT_2 |
" is invalid. Must be within the range of 0 and " |
public static final java.lang.String |
ERRMSG_BAD_AT_NBR_1 |
"A-TM-0003 Invalid \'atNbr\' = " |
public static final java.lang.String |
ERRMSG_BAD_AT_NBR_2 |
" input! Should be 1, 2, or 3." |
public static final java.lang.String |
ERRMSG_BAD_AT_VALUE |
"A-TM-0004 Invalid \'%s\' String = %s input! Should be \'Cnst\', \'Var\' or \'Sym\'." |
public static final java.lang.String |
ERRMSG_BAD_BY_VALUE |
"A-TM-0001 Invalid \'%s\' String = %s input! Should be \'Cnst\', \'Var\' or \'Sym\'." |
public static final java.lang.String |
ERRMSG_BAD_MAX_DEPTH_1 |
"A-TM-0201 Invalid maxDepth parameter, must be a positive integer. Input = " |
public static final java.lang.String |
ERRMSG_BAD_NEW_FORMAT_NBR_1 |
"A-TM-0104 Input format number = " |
public static final java.lang.String |
ERRMSG_BAD_NEW_FORMAT_NBR_2 |
" is invalid. Must be within the range of 0 and " |
public static final java.lang.String |
ERRMSG_BAD_PREF_FORMAT_NBR |
"A-TM-0302 Input format number %d is invalid. Must be within the range of 0 and %d." |
public static final java.lang.String |
ERRMSG_BAD_SUB_EXPR_NODE_1 |
"A-TM-0006 Invalid ParseNode passed for Sub-Expression output. Node must be either a VarHyp node or a SyntaxAxiom node -- i.e. a parse ParseNode, not a *proof* ParseNode!" |
public static final java.lang.String |
ERRMSG_BAD_UPD_FORMAT_NBR_1 |
"A-TM-0103 Input format number = " |
public static final java.lang.String |
ERRMSG_BAD_UPD_FORMAT_NBR_2 |
" is invalid. Must be within the range of 1 and " |
public static final java.lang.String |
ERRMSG_BAD_USE_INDENT |
"A-TM-0309 Input Use Indent amount %d is invalid. Must be within the range of 0 and %d" |
public static final java.lang.String |
ERRMSG_BAD_USER_METHOD_NAME |
"A-TM-0202 Invalid (user) name of TMFF Method = %s" |
public static final java.lang.String |
ERRMSG_CANNOT_UPD_FORMAT_0_1 |
"A-TM-0102 Format Number " |
public static final java.lang.String |
ERRMSG_CANNOT_UPD_FORMAT_0_2 |
" is RESERVED and cannot be updated." |
public static final java.lang.String |
ERRMSG_ERR_FORMAT_NBR_INPUT_1 |
" Input Format Nbr must be a number between 0 and " |
public static final java.lang.String |
ERRMSG_ERR_INDENT_INPUT_1 |
" Input Indent amount must be a number between 0 and " |
public static final java.lang.String |
ERRMSG_FORMAT_NBR_MISSING_1 |
"A-TM-0106 TMFFDefineFormat Format Number not input!" |
public static final java.lang.String |
ERRMSG_FORMAT_NBR_MISSING2_1 |
"A-TM-0304 TMFFUseFormat Format Number not input!" |
public static final java.lang.String |
ERRMSG_FORMAT_SCHEME_MISSING_1 |
"A-TM-0101 Cannot create TMFFFormat without Scheme!" |
public static final java.lang.String |
ERRMSG_FORMAT_SCHEME_NAME_NOTFND |
"A-TM-0303 TMFFDefineFormat Scheme Name not found among previously defined Schemes. Input name = %s" |
public static final java.lang.String |
ERRMSG_FORMAT_SCHEME_NAME_NOTFND2_1 |
"A-TM-0105 TMFFDefineFormat Scheme Name not found among previously defined Schemes. Input name = " |
public static final java.lang.String |
ERRMSG_MISSING_AT_VALUE_1 |
"A-TM-0005 Missing \'atValue\' String parameter!" |
public static final java.lang.String |
ERRMSG_MISSING_BY_VALUE |
"A-TM-0002 Missing \'%s\' String parameter!" |
public static final java.lang.String |
ERRMSG_MISSING_USER_METHOD_NAME |
"A-TM-0203 Missing (user) name of TMFF Method" |
public static final java.lang.String |
ERRMSG_NO_ROOM_SUB_EXPR_1 |
"I-TM-0007 Ran out of room on line formatting sub-expression. Either the lines are too narrow or the formula is so complex that the total indentation cannot fit on a normal line." |
public static final java.lang.String |
ERRMSG_RENDER_FORMULA_ERROR_1 |
"A-TM-0301 Programmer Error. The default formula formatting routine failed horribly. Call 911." |
public static final java.lang.String |
ERRMSG_SCHEME_CANNOT_BE_UPDATED |
"A-TM-0402 Scheme %s is RESERVED and cannot be updated." |
public static final java.lang.String |
ERRMSG_SCHEME_METHOD_MISSING |
"A-TM-0401 TMFFScheme Method is required!" |
public static final java.lang.String |
ERRMSG_SCHEME_NAME_MISSING_1 |
"A-TM-0107 TMFFDefineFormat Scheme Name not input!" |
public static final java.lang.String |
ERRMSG_SCHEME_NAME_REQUIRED |
"A-TM-0403 Scheme Name is required!" |
public static final java.lang.String |
ERRMSG_SCHEME_NM_CANT_BE_ASSIGNED |
"A-TM-0404 Scheme Name %s is RESERVED and cannot be assigned." |
public static final java.lang.String |
ERRMSG_UNFORMATTED_BAD_CALL_FLAT_1 |
"A-TM-0601 TMFFFlat.renderSubExprWithBreaks() was invoked. This indicates fried programmer. Bad. Call 911!" |
public static final java.lang.String |
ERRMSG_UNFORMATTED_BAD_CALL_UNF_1 |
"A-TM-0501 TMFFUnformatted.renderSubExprWithBreaks() was invoked. This indicates fried programmer. Bad. Call 911!" |
public static final java.lang.String |
ERRMSG_UPDATE_SCHEME_NOTFND_BUG_1 |
"A-TM-0305 TMFFDefineScheme not found to update. Call 911, programmer error because the name had already been looked up. Name = " |
public static final java.lang.String |
ERRMSG_USE_INDENT_MISSING2_1 |
"A-TM-0308 TMFFUseIndent Use Indent amount not input!" |
public static final int |
MAX_ALIGN_AT_NBR |
3 |
public static final int |
MIN_ALIGN_AT_NBR |
1 |
public static final int |
TMFF_ALT_FORMAT_NBR_DEFAULT |
7 |
public static final int |
TMFF_ALT_INDENT_DEFAULT |
1 |
public static final java.lang.String |
TMFF_AT_VALUE |
"atValue" |
public static final java.lang.String |
TMFF_BY_VALUE |
"byValue" |
public static final int |
TMFF_CURR_FORMAT_NBR_DEFAULT |
13 |
public static final int |
TMFF_MAX_FORMAT_NBR |
15 |
public static final int |
TMFF_MAX_INDENT |
5 |
public static final java.lang.String |
TMFF_METHOD_USER_NAME_ALIGN_COLUMN |
"AlignColumn" |
public static final java.lang.String |
TMFF_METHOD_USER_NAME_FLAT |
"Flat" |
public static final java.lang.String |
TMFF_METHOD_USER_NAME_TWO_COLUMN_ALIGNMENT |
"TwoColumnAlignment" |
public static final java.lang.String |
TMFF_METHOD_USER_NAME_UNFORMATTED |
"Unformatted" |
public static final int |
TMFF_UNFORMATTED_FORMAT_NBR_0 |
0 |
public static final java.lang.String |
TMFF_UNFORMATTED_SCHEME_NAME |
"Unformatted" |
public static final int |
TMFF_USE_INDENT_DEFAULT |
0 |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final java.lang.String |
ARGUMENTS_OPTION_REPORT_LINE_1 |
"\nCommandLineArguments.displayArgumentOptionReport():\n" |
public static final java.lang.String |
ARGUMENTS_OPTION_REPORT_LINE_2 |
" Command Line Arguments:" |
public static final java.lang.String |
ARGUMENTS_OPTION_REPORT_LINE_3A |
" Arg #" |
public static final java.lang.String |
ARGUMENTS_OPTION_REPORT_LINE_3B |
" = " |
public static final java.lang.String |
ARGUMENTS_OPTION_REPORT_LINE_4 |
" [2] displayMMJ2FailPopupWindow \n = " |
public static final java.lang.String |
ARGUMENTS_OPTION_REPORT_LINE_5 |
"\n***END CommandLineArguments.displayArgumentOptionReport()***\n" |
public static final int |
DISPLAY_MMJ2_FAIL_POPUP_WINDOW_ARGUMENT_INDEX |
1 |
public static final java.lang.String |
DISPLAY_MMJ2_FAIL_POPUP_WINDOW_ARGUMENT_LITERAL |
"displayMMJ2FailPopupWindow argument" |
public static final boolean |
DISPLAY_MMJ2_FAIL_POPUP_WINDOW_DEFAULT |
true |
public static final java.lang.String |
DUMP_ACTIVE_VARHYP |
" activeVarHyp: " |
public static final java.lang.String |
DUMP_AXIOM |
"Axiom: " |
public static final java.lang.String |
DUMP_AXIOM_UNIQUE_CNST |
" syntaxAxiomHasUniqueCnst " |
public static final java.lang.String |
DUMP_BM_AXIOM |
"Axiom " |
public static final java.lang.String |
DUMP_BM_CNST |
"Cnst " |
public static final java.lang.String |
DUMP_BM_DOT |
"." |
public static final java.lang.String |
DUMP_BM_EQ_COL |
"=: " |
public static final java.lang.String |
DUMP_BM_LOGHYP |
"LogHyp " |
public static final java.lang.String |
DUMP_BM_THEOREM |
"Theorem " |
public static final java.lang.String |
DUMP_BM_UNKNOWN |
"?Stmt? " |
public static final java.lang.String |
DUMP_BM_VAR |
"Var " |
public static final java.lang.String |
DUMP_BM_VARHYP |
"VarHyp " |
public static final java.lang.String |
DUMP_CNST |
"Cnst: " |
public static final char |
DUMP_COMMA |
44 |
public static final java.lang.String |
DUMP_EARLEY_FIRST |
" EarleyFIRST= [" |
public static final java.lang.String |
DUMP_END |
" End" |
public static final java.lang.String |
DUMP_END_BRACKET |
"] " |
public static final java.lang.String |
DUMP_EXPR_RPN |
"ExprRPN: " |
public static final java.lang.String |
DUMP_FORMULA |
"Formula:" |
public static final java.lang.String |
DUMP_GRAMMAR_RULE |
"GrammarRule: " |
public static final int |
DUMP_GRAMMAR_RULE_MAX_PRINT |
9999 |
public static final java.lang.String |
DUMP_GRAMMAR_RULE_REPLACEMENT_SYMBOL |
" =: " |
public static final java.lang.String |
DUMP_IS_ACTIVE |
" isActive" |
public static final java.lang.String |
DUMP_IS_ASSRT |
" isAssrt" |
public static final java.lang.String |
DUMP_IS_CNST |
" isCnst" |
public static final java.lang.String |
DUMP_IS_GIMME_MATCH_NBR |
" isGimmeMatchNbr = " |
public static final java.lang.String |
DUMP_IS_GRAMMATICAL_TYP |
" isGrammaticalTyp" |
public static final java.lang.String |
DUMP_IS_HYP |
" isHyp" |
public static final java.lang.String |
DUMP_IS_LOGIC_TYP |
" isLogicStmtTyp" |
public static final java.lang.String |
DUMP_IS_PROVABLE_TYP |
" isProvableLogicStmtTyp" |
public static final java.lang.String |
DUMP_IS_SYNTAX_AXIOM_TYP |
" isSyntaxAxiomTyp" |
public static final java.lang.String |
DUMP_IS_VAR_TYP |
" isVarTyp" |
public static final java.lang.String |
DUMP_LEN1_CNST_AXIOM |
" Axiom = " |
public static final java.lang.String |
DUMP_LEN1_CNST_RULE_NBR |
" len1CnstNotationRule ruleNbr = " |
public static final java.lang.String |
DUMP_LOGHYP |
"LogHyp: " |
public static final java.lang.String |
DUMP_LOGIC_TYP_SET |
"Grammar.logicStmtTypSet: " |
public static final java.lang.String |
DUMP_LOGICAL_SYSTEM |
"LogicalSystem: " |
public static final java.lang.String |
DUMP_LOGSYS_COUNTS |
"LogSysCounts: " |
public static final java.lang.String |
DUMP_LOGSYS_STMT_TBL |
"LogicalSystem.stmtTbl: " |
public static final java.lang.String |
DUMP_LOGSYS_SYM_TBL |
"LogicalSystem.symTbl: " |
public static final java.lang.String |
DUMP_MAND_FRAME_DJ_VARS |
" DjVars : [" |
public static final java.lang.String |
DUMP_MAND_FRAME_HYP_ARRAY |
"Mandframe, hypArray: [" |
public static final java.lang.String |
DUMP_MAND_VARHYP_ARRAY |
" VarHypArray: [" |
public static final java.lang.String |
DUMP_MAX_SEQ_NBR |
" MaxSeqNbr: " |
public static final java.lang.String |
DUMP_NBR_HYP_PARAMS_USED |
" NbrHypParamsUsed: " |
public static final int |
DUMP_NOTATION_LABEL_PADIT |
7 |
public static final java.lang.String |
DUMP_NOTATION_LIST |
"Notation List: " |
public static final java.lang.String |
DUMP_NOTATION_RULE |
"NotationRule: " |
public static final int |
DUMP_NOTATION_RULE_NBR_PADIT |
5 |
public static final int |
DUMP_NOTATION_RULE_TYP_PADIT |
7 |
public static final java.lang.String |
DUMP_NULLS_PERMITTED_LIST |
"NullsPermitted List: " |
public static final java.lang.String |
DUMP_NULLS_PERMITTED_RULE |
"NullsPermittedRule: " |
public static final java.lang.String |
DUMP_NULLS_PERMITTED_TYP_SET |
"Grammar.nullsPermittedTypSet: " |
public static final java.lang.String |
DUMP_OF_FIRST |
" dump of first " |
public static final java.lang.String |
DUMP_OPT_FRAME_DJ_VARS |
" DjVars : [" |
public static final java.lang.String |
DUMP_OPT_FRAME_HYP_ARRAY |
"Optframe, optHypArray: [" |
public static final java.lang.String |
DUMP_PARAM_TREE_AS_RPN |
" ParamTransformationTree as RPN: " |
public static final java.lang.String |
DUMP_PARAM_VARHYP_NODE_ARRAY |
" ParamVarHypNode Array: " |
public static final java.lang.String |
DUMP_PROOF |
"Proof: " |
public static final java.lang.String |
DUMP_PROOF_MISSING_STEP |
"? " |
public static final java.lang.String |
DUMP_PROVABLE_TYP_SET |
"Grammar.provableLogicStmtTypSet: " |
public static final java.lang.String |
DUMP_RIGHT_ARROW |
" -> " |
public static final java.lang.String |
DUMP_RULE_COLLECTION |
"GrammarRule Collection:" |
public static final java.lang.String |
DUMP_RULE_COLLECTION_IS_EMPTY |
"GrammarRule Collection IS EMPTY!" |
public static final java.lang.String |
DUMP_RULE_COLLECTION_UNDERSCORE |
"=======================" |
public static final java.lang.String |
DUMP_RULE_COLON |
" : " |
public static final java.lang.String |
DUMP_RULE_CONTINUATION_LIT |
" | " |
public static final java.lang.String |
DUMP_RULE_NBR |
" RuleNbr: " |
public static final java.lang.String |
DUMP_START |
" Start" |
public static final java.lang.String |
DUMP_START_BRACKET |
"[" |
public static final java.lang.String |
DUMP_STMT_TBL |
"stmtTbl:" |
public static final java.lang.String |
DUMP_STMT_TBL_IS_EMPTY |
"stmtTbl IS EMPTY!" |
public static final java.lang.String |
DUMP_STMT_TBL_SIZE |
" stmtTbl.size()= " |
public static final java.lang.String |
DUMP_STMT_TBL_UNDERSCORE |
"========" |
public static final java.lang.String |
DUMP_SYM_TBL |
"symTbl:" |
public static final java.lang.String |
DUMP_SYM_TBL_IS_EMPTY |
"symTbl IS EMPTY!" |
public static final java.lang.String |
DUMP_SYM_TBL_SIZE |
" symTbl.size()= " |
public static final java.lang.String |
DUMP_SYM_TBL_UNDERSCORE |
"=======" |
public static final java.lang.String |
DUMP_SYNTAX_AXIOM_TYP_SET |
"Grammar.syntaxAxiomTypSet: " |
public static final java.lang.String |
DUMP_THE_GRAMMAR |
"The Grammar" |
public static final java.lang.String |
DUMP_THE_GRAMMAR_IS_EMPTY |
"The Grammar is empty?!?" |
public static final java.lang.String |
DUMP_THE_GRAMMAR_UNDERSCORE |
"===========" |
public static final java.lang.String |
DUMP_THEOREM |
"Theorem: " |
public static final java.lang.String |
DUMP_TYP |
" Typ: " |
public static final java.lang.String |
DUMP_TYPE_CODE |
" Type Code: " |
public static final java.lang.String |
DUMP_TYPE_CONVERSION_LIST |
"TypeConversion List: " |
public static final java.lang.String |
DUMP_TYPE_CONVERSION_RULE |
"TypeConversionRule: " |
public static final java.lang.String |
DUMP_VAR |
"Var: " |
public static final java.lang.String |
DUMP_VARHYP |
"VarHyp: " |
public static final java.lang.String |
DUMP_VARHYP_RESEQ |
"syntaxAxiomVarHypReseq: [" |
public static final java.lang.String |
DUMP_VARHYP_TYP_SET |
"Grammar.varHypTypSet: " |
public static final java.lang.String |
ERRMSG_MACRO_LANGUAGE_MISSING_2 |
"To use %s, set language to one of %s.\n" |
public static final int |
JAVA_VERSION_MMJ2_MAJ |
1 |
public static final int |
JAVA_VERSION_MMJ2_MIN |
5 |
public static final java.lang.String |
JAVA_VERSION_MMJ2_RUNTIME_ERROR_MSG |
"BatchMMJ2 requires Java RunTime Environment Version 1.5 or higher. Version running now = " |
public static final java.lang.String |
JAVA_VERSION_PROPERTY_NAME |
"java.version" |
public static final int |
LINE_BREAK_MAX_LENGTH |
75 |
public static final int |
MAX_STARTUP_ERROR_MESSAGES |
4 |
public static final int |
MAX_STATEMENT_PRINT_COUNT_DEFAULT |
9999 |
public static final int |
METAMATH_PATH_ARGUMENT_INDEX |
3 |
public static final java.lang.String |
METAMATH_PATH_ARGUMENT_LITERAL |
"metamathPath argument" |
public static final java.lang.String |
METAMATH_PATH_REPORT_LINE_2 |
" [4] metamathPath = " |
public static final java.lang.String |
MMJ2_FAIL_DIALOG_TITLE |
"MMJ2 Fail" |
public static final java.lang.String |
MMJ2_FAIL_STARTUP_DIALOG_TITLE |
"MMJ2 Start-up Error" |
public static final int |
MMJ2_PATH_ARGUMENT_INDEX |
2 |
public static final java.lang.String |
MMJ2_PATH_ARGUMENT_LITERAL |
"mmj2Path argument" |
public static final java.lang.String |
MMJ2_PATH_REPORT_LINE_1 |
"\n [3] mmj2Path = " |
public static final java.lang.String |
MMJ2_STARTUP_MSG_LIT_1 |
"RunParm #" |
public static final java.lang.String |
MMJ2_STARTUP_MSG_LIT_2 |
" Command = " |
public static final java.lang.String |
MMJ2_STARTUP_MSG_LIT_3 |
" Error(s)\n" |
public static final char |
NEW_LINE_CHAR |
10 |
public static final java.lang.String |
NO_ARGUMENT |
"N" |
public static final java.lang.String |
OPTION_FILE_OUT_USAGE_DEFAULT |
"new" |
public static final int |
OUTPUT_VERBOSITY_DEFAULT |
9999 |
public static final java.lang.String |
PATH_REPORT_E_G_CAPTION_1 |
" (e.g. " |
public static final java.lang.String |
PATH_REPORT_E_G_CAPTION_2 |
")" |
public static final java.lang.String |
PATH_REPORT_EXAMPLE_FILE_NAME |
"YourFile.xyz" |
public static final java.lang.String |
PROOF_ASST_FONT_FAMILY_LIST_CAPTION |
" List of Font Families defined in the system: \n" |
public static final java.lang.String |
RUN_PARM_FILE_REPORT_LINE_1 |
" [1] runParmFile = " |
public static final char |
RUNPARM_COMMENT_CHAR_ASTERISK |
42 |
public static final char |
RUNPARM_COMMENT_CHAR_SLASH |
47 |
public static final char |
RUNPARM_COMMENT_CHAR_SPACE |
32 |
public static final char |
RUNPARM_FIELD_DELIMITER_DEFAULT |
44 |
public static final char |
RUNPARM_FIELD_QUOTER_DEFAULT |
34 |
public static final int |
RUNPARM_FILE_NAME_ARGUMENT_INDEX |
0 |
public static final java.lang.String |
RUNPARM_FILE_NAME_ARGUMENT_LITERAL |
"runParmFileName argument" |
public static final int |
RUNPARM_LINE_DUMP_VERBOSITY |
9 |
public static final boolean |
RUNPARM_MACRO_ENABLED_DEFAULT |
true |
public static final java.lang.String |
RUNPARM_OPTION_ASCII_RETEST |
"AsciiRetest" |
public static final java.lang.String |
RUNPARM_OPTION_ERASE_AND_REDERIVE_FORMULAS |
"EraseAndRederiveFormulas" |
public static final java.lang.String |
RUNPARM_OPTION_FILE_OUT_NEW |
"new" |
public static final java.lang.String |
RUNPARM_OPTION_FILE_OUT_UPDATE |
"update" |
public static final java.lang.String |
RUNPARM_OPTION_INHERIT |
"inherit" |
public static final java.lang.String |
RUNPARM_OPTION_INIT_MACRO |
"init" |
public static final java.lang.String |
RUNPARM_OPTION_MACRO_EXTENSION |
"js" |
public static final java.lang.String |
RUNPARM_OPTION_MACRO_LANGUAGE |
"js" |
public static final java.lang.String |
RUNPARM_OPTION_NO |
"no" |
public static final java.lang.String |
RUNPARM_OPTION_NO_ABBREVIATED |
"n" |
public static final java.lang.String |
RUNPARM_OPTION_OFF |
"off" |
public static final java.lang.String |
RUNPARM_OPTION_ON |
"on" |
public static final java.lang.String |
RUNPARM_OPTION_PREP_MACRO |
"prep" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_AUTOCOMPLETE |
"autocomplete" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_COMPARE_DJS |
"CompareDJs" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_CORRECT |
"correct" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_DERIVE_FORMULAS |
"DeriveFormulas" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_EXPORT_UN_UNIFIED |
"un-unified" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_EXPORT_UNIFIED |
"unified" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_HALF_REVERSE |
"halfreverse" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_NOT_RANDOMIZED |
"NotRandomized" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_PRINT |
"Print" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_REVERSE |
"reverse" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_SOME_ORDER |
"someorder" |
public static final java.lang.String |
RUNPARM_OPTION_PROOF_ASST_UPDATE_DJS |
"UpdateDJs" |
public static final java.lang.String |
RUNPARM_OPTION_VALUE_ALL |
"*" |
public static final java.lang.String |
RUNPARM_OPTION_VALUE_BASIC |
"basic" |
public static final java.lang.String |
RUNPARM_OPTION_VALUE_COMPLETE |
"complete" |
public static final java.lang.String |
RUNPARM_OPTION_YES |
"yes" |
public static final java.lang.String |
RUNPARM_OPTION_YES_ABBREVIATED |
"y" |
public static final int |
SVC_PATH_ARGUMENT_INDEX |
4 |
public static final java.lang.String |
SVC_PATH_ARGUMENT_LITERAL |
"svcPath argument" |
public static final java.lang.String |
SVC_PATH_REPORT_LINE_3 |
" [5] svcPath = " |
public static final int |
TEST_OPTION_ARGUMENT_INDEX |
5 |
public static final int |
THEOREM_LOADER_BOSS_FILE_BUFFER_SIZE |
32768 |
public static final java.lang.String |
YES_ARGUMENT |
"Y" |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final int |
BOTTOM_UP_GOVERNOR_LIMIT |
4 |
public static final int |
BOTTOM_UP_GOVERNOR_LIMIT_MAX |
1024 |
public static final int |
BOTTOM_UP_STACK_HARD_FAILURE_MAX |
1000 |
public static final boolean |
DEFAULT_COMPLETE_GRAMMAR_AMBIG_EDITS |
false |
public static final boolean |
DEFAULT_COMPLETE_STATEMENT_AMBIG_EDITS |
false |
public static final int |
EARLEY_PARSE_CITEMSET_ITEMSET_RATIO |
2 |
public static final int |
EARLEY_PARSE_MIN_ITEMSET_MAXIMUM |
50 |
public static final java.lang.String |
ERRMSG_AFTER_DOT_CAPTION |
" afterDot:" |
public static final java.lang.String |
ERRMSG_AT_CAPTION |
" at:" |
public static final java.lang.String |
ERRMSG_COLON_CAPTION |
":" |
public static final java.lang.String |
ERRMSG_DOT_CAPTION |
" dot:" |
public static final java.lang.String |
ERRMSG_N_PARSE_TREES_2 |
" ParseTree[%d] = %s" |
public static final java.lang.String |
ERRMSG_RULE_EXPR_CAPTION |
" ruleExpr:" |
public static final int |
MAX_DERIVED_RULE_QUEUE_SIZE |
1000 |
public static final int |
MAX_PARSE_RETRIES |
20 |
public static final int |
PARSE_TREE_MAX_FOR_AMBIG_EDIT |
2 |
Modifier and Type | Constant Field | Value |
---|---|---|
public static final int |
PROOF_ABSOLUTE_MAX_RETRIES |
7 |
public static final int |
PROOF_PSTACK_HARD_FAILURE_LEN |
6400 |
public static final int |
PROOF_PSTACK_INIT_LEN |
400 |
public static final int |
PROOF_SUBST_HARD_FAILURE_LEN |
6400 |
public static final int |
PROOF_SUBST_INIT_LEN |
400 |
public static final int |
PROOF_WEXPR_HARD_FAILURE_LEN |
32000 |
public static final int |
PROOF_WEXPR_INIT_LEN |
4000 |
public static final java.lang.String |
QED_STEP_NBR |
"qed" |