/*****************************************************************************/ /* Copyright (C) 2020 NORMAN MEGILL nm at alum.mit.edu */ /* License terms: GNU General Public License */ /*****************************************************************************/ /*34567890123456 (79-character line to adjust editor window) 2345678901234567*/ /* Part 2 of help file for Metamath */ /* To add a new help entry, you must add the command syntax to mmcmdl.c as well as adding it here. */ #include #include #include "mmvstr.h" #include "mmdata.h" #include "mmcmds.h" #include "mmhlpb.h" void help2(vstring helpCmd) { /* 5-Sep-2012 nm */ vstring saveHelpCmd = ""; /* help2() may be called with a temporarily allocated argument (left(), cat(), etc.), and the let()s in the eventual print2() calls will deallocate and possibly corrupt helpCmd. So, we grab a non-temporarily allocated copy here. (And after this let(), helpCmd will become invalid for the same reason.) */ let(&saveHelpCmd, helpCmd); g_printHelp = !strcmp(saveHelpCmd, "HELP"); H("Welcome to Metamath. Here are some general guidelines."); H(""); H("To make the most effective use of Metamath, you should become familiar"); H("with the Metamath book. In particular, you will need to learn"); H("the syntax of the Metamath language."); H(""); H("For help using the command line, type HELP CLI."); H("For help invoking Metamath, type HELP INVOKE."); H("For a summary of the Metamath language, type HELP LANGUAGE."); H("For a summary of comment markup, type HELP VERIFY MARKUP."); H("For help getting started, type HELP DEMO."); H("For help exploring the data base, type HELP EXPLORE."); H("For help creating a LaTeX file, type HELP TEX."); H("For help creating Web pages, type HELP HTML."); H("For help proving new theorems, type HELP PROOF_ASSISTANT."); H("For a list of help topics, type HELP ? (to force an error message)."); H("For current program settings, type SHOW SETTINGS."); H("For a simple but general-purpose ASCII file manipulator, type TOOLS."); H("To exit Metamath, type EXIT (or its synonym QUIT)."); H(""); H(cat("If you need technical support, contact Norman Megill at nm", "@", "alum.mit.edu.", NULL)); H("Copyright (C) 2020 Norman Megill License terms: GPL 2.0 or later"); H(""); g_printHelp = !strcmp(saveHelpCmd, "HELP COMMENTS"); H("Comment markup is described near the end of HELP LANGUAGE. See also"); H("HELP HTML for the $t comment and HTML definitions."); H(""); g_printHelp = !strcmp(saveHelpCmd, "HELP INVOKE"); H("To invoke Metamath from a Unix/Linux/MacOSX prompt, assuming that the"); H("Metamath program is in the current directory, type"); H(""); H(" bash$ ./metamath"); H(""); H("To invoke Metamath from a Windows DOS or Command Prompt, assuming that"); H("the Metamath program is in the current directory (or in a directory"); H("included in the Path system environment variable), type"); H(""); H(" C:\\metamath>metamath"); H(""); H("To use command-line arguments at invocation, the command-line arguments"); H("should be a list of Metamath commands, surrounded by quotes if they"); H("contain spaces. In Windows DOS, the surrounding quotes must be double"); H("(not single) quotes. For example, to read the database set.mm, verify"); H("all proofs, and exit the program, type (under Unix)"); H(""); H(" bash$ ./metamath 'read set.mm' 'verify proof *' exit"); H(""); H("Note that in Unix, any directory path with /'s must be surrounded by"); H("quotes so Metamath will not interpret the / as a command qualifier. So"); H("if set.mm is in the /tmp directory, use for the above example"); H(""); H(" bash$ ./metamath 'read \"/tmp/set.mm\"' 'verify proof *' exit"); H(""); H("For convenience, if the command-line has one argument and no spaces in"); H("the argument, the command is implicitly assumed to be READ. In this one"); H("special case, /'s are not interpreted as command qualifiers, so you don't"); H("need quotes around a Unix file name. Thus"); H(""); H(" bash$ ./metamath /tmp/set.mm"); H(""); H("and"); H(""); H(" bash$ ./metamath \"read '/tmp/set.mm'\""); H(""); H("are equivalent."); H(""); g_printHelp = !strcmp(saveHelpCmd, "HELP SHOW MEMORY"); H("Syntax: SHOW MEMORY"); H(""); H("This command shows the available memory left. It is not meaningful"); H("on modern machines with virtual memory."); H(""); g_printHelp = !strcmp(saveHelpCmd, "HELP SHOW SETTINGS"); H("Syntax: SHOW SETTINGS"); H(""); H("This command shows the state of various parameters."); H(""); g_printHelp = !strcmp(saveHelpCmd, "HELP SHOW ELAPSED_TIME"); H("Syntax: SHOW ELAPSED_TIME"); H(""); H("This command shows the time elapsed in the session and from any"); H("previous use of SHOW ELAPSED_TIME."); H(""); g_printHelp = !strcmp(saveHelpCmd, "HELP SHOW LABELS"); H("Syntax: SHOW LABELS [/ ALL] [/ LINEAR]"); H(""); H("This command shows the labels of $a and $p statements that match"); H(". may contain * and ? wildcard characters;"); H("see HELP SEARCH for wildcard matching rules."); H(""); H("Optional qualifier:"); H(" / ALL - Include matches for $e and $f statement labels."); H(" / LINEAR - Display only one label per line. This can be useful for"); H(" building scripts in conjunction with the TOOLS utility."); H(""); g_printHelp = !strcmp(saveHelpCmd, "HELP SHOW DISCOURAGED"); H("Syntax: SHOW DISCOURAGED"); H(""); H("This command shows the usage and proof statistics for statements with"); H("\"(Proof modification is discouraged.)\" and \"(New usage is"); H("discouraged.)\" markup tags in their description comments. The output"); H("is intended to be used by scripts that compare a modified .mm file"); H("to a previous version."); H(""); g_printHelp = !strcmp(saveHelpCmd, "HELP SHOW SOURCE"); H("Syntax: SHOW SOURCE