/*****************************************************************************/ /* Copyright (C) 2008 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) { printHelp = !strcmp(helpCmd, "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 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) 2006 Norman Megill"); H("License terms: GNU General Public License"); H(""); printHelp = !strcmp(helpCmd, "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(""); printHelp = !strcmp(helpCmd, "HELP CLI"); H("The Metamath program was first developed on a VAX/VMS system, and some"); H("aspects of its command line behavior reflect this heritage. Hopefully"); H( "you will find it reasonably user-friendly once you get used to it."); H(""); H("Each command line is a sequence of English-like words separated by"); H("spaces, as in SHOW SETTINGS. Command words are not case sensitive, and"); H("only as many letters are needed as are necessary to eliminate ambiguity;"); H("for example, \"sh se\" would work for the command SHOW SETTINGS. In some"); H("cases arguments such as file names, statement labels, or symbol names are"); H("required; these are case-sensitive (although file names may not be on"); H("some operating systems)."); H(""); H("A command line is entered by typing it in then pressing the key."); H(""); H("To find out what commands are available, type ? at the MM> prompt,"); H("followed by . (This is actually just a trick to force an error"); H("message, since ? is not a legal command.)"); H(""); H("To find out the choices at any point in a command, press and you"); H("will be prompted for them. The default choice (the one selected if you"); H("just press ) is shown in brackets (<>)."); H(""); H("You may also type ? in place of a command word to force Metamath to tell"); H("you what the choices are. The ? method won't work, though, if a"); H("non-keyword argument such as a file name is expected at that point,"); H("because the CLI will think the ? is the argument."); H(""); H("Some commands have one or more optional qualifiers that modify the"); H("behavior of the command. Qualifiers are indicated by a slash (/), such as"); H("in READ set.mm / VERIFY. Spaces are optional around / and =. If you need"); H("to use / or = in a command argument, as in a Unix file name, put single"); H("or double quotes around the command argument. See the last section of"); H("HELP LET for more information on special characters in arguments."); H(""); H("The OPEN LOG command will save everything you see on the screen, and is"); H("useful to help you recover should something go wrong in a proof, or if"); H("you want to document a bug."); H(""); H("If the response to a command is more than a screenful, you will be"); H("prompted to ' to continue, Q to quit, or S to scroll to end'."); H("Q will complete the command internally but suppress further output until"); H("the next \"MM>\" prompt. S will suppress further pausing until the next"); H("\"MM>\" prompt. After the first screen, you can also choose B to go back"); H("a screenful. Note that B may also be entered at the \"MM>\" prompt"); H("immediately after a command to scroll back through the output of that"); H("command. Scrolling can be disabled with SET SCROLL CONTINUOUS."); H(""); H("**Warning** Pressing CTRL-C will abort the Metamath program"); H("unconditionally. This means any unsaved work will be lost."); H(""); H("A command line enclosed in quotes is executed by your operating system."); H("See HELP SYSTEM."); H(""); H("Some additional CLI-related features are explained by:"); H(" HELP SET ECHO"); H(" HELP SET SCROLL"); H(" HELP SET WIDTH"); /* 18-Nov-05 nm Was SCREEN_WIDTH */ H(" HELP SET HEIGHT"); /* 18-Nov-05 nm New */ H(" HELP SUBMIT"); H(""); printHelp = !strcmp(helpCmd, "HELP SHOW MEMORY"); H("Syntax: SHOW MEMORY"); H(""); H("This command shows the available memory left. It may not be meaningful"); H("on machines with virtual memory."); H(""); printHelp = !strcmp(helpCmd, "HELP SHOW SETTINGS"); H("Syntax: SHOW SETTINGS"); H(""); H("This command shows the state of various parameters."); H(""); printHelp = !strcmp(helpCmd, "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(""); printHelp = !strcmp(helpCmd, "HELP SHOW SOURCE"); H("Syntax: SHOW SOURCE