Skip to content

Commit bec06db

Browse files
digama0digama0
committed
renormalize line endings
1 parent 73b6b8d commit bec06db

25 files changed

+31247
-31247
lines changed

‎mmcmdl.c‎

Lines changed: 2302 additions & 2302 deletions
Large diffs are not rendered by default.

‎mmcmdl.h‎

Lines changed: 43 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -1,43 +1,43 @@
1-
/*****************************************************************************/
2-
/* Copyright (C) 2018 NORMAN MEGILL nm at alum.mit.edu */
3-
/* License terms: GNU General Public License */
4-
/*****************************************************************************/
5-
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
6-
7-
#ifndef METAMATH_MMCMDL_H_
8-
#define METAMATH_MMCMDL_H_
9-
10-
#include "mmvstr.h"
11-
#include "mmdata.h"
12-
13-
flag processCommandLine(void);
14-
flag getFullArg(long arg, vstring cmdList);
15-
void parseCommandLine(vstring line);
16-
flag lastArgMatches(vstring argString);
17-
flag cmdMatches(vstring cmdString);
18-
long switchPos(vstring swString);
19-
void printCommandError(vstring line, long arg, vstring errorMsg);
20-
void freeCommandLine(void);
21-
22-
#define DEFAULT_COLUMN 16
23-
extern pntrString *g_rawArgPntr;
24-
extern nmbrString *g_rawArgNmbr;
25-
extern long g_rawArgs;
26-
extern pntrString *g_fullArg;
27-
extern vstring g_fullArgString; /* g_fullArg as one string */
28-
extern vstring g_commandPrompt;
29-
extern vstring g_commandLine;
30-
extern long g_showStatement;
31-
extern vstring g_logFileName;
32-
extern vstring g_texFileName;
33-
extern flag g_PFASmode; /* Proof assistant mode, invoked by PROVE command */
34-
extern flag g_sourceChanged; /* Flag that user made some change to the source file*/
35-
extern flag g_proofChanged; /* Flag that user made some change to proof in progress*/
36-
extern flag g_commandEcho; /* Echo full command */
37-
extern flag g_memoryStatus; /* Always show memory */
38-
39-
extern flag g_sourceHasBeenRead; /* 1 if a source file has been read in */
40-
extern vstring g_rootDirectory; /* Directory to use for included files */
41-
42-
43-
#endif /* METAMATH_MMCMDL_H_ */
1+
/*****************************************************************************/
2+
/* Copyright (C) 2018 NORMAN MEGILL nm at alum.mit.edu */
3+
/* License terms: GNU General Public License */
4+
/*****************************************************************************/
5+
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
6+
7+
#ifndef METAMATH_MMCMDL_H_
8+
#define METAMATH_MMCMDL_H_
9+
10+
#include "mmvstr.h"
11+
#include "mmdata.h"
12+
13+
flag processCommandLine(void);
14+
flag getFullArg(long arg, vstring cmdList);
15+
void parseCommandLine(vstring line);
16+
flag lastArgMatches(vstring argString);
17+
flag cmdMatches(vstring cmdString);
18+
long switchPos(vstring swString);
19+
void printCommandError(vstring line, long arg, vstring errorMsg);
20+
void freeCommandLine(void);
21+
22+
#define DEFAULT_COLUMN 16
23+
extern pntrString *g_rawArgPntr;
24+
extern nmbrString *g_rawArgNmbr;
25+
extern long g_rawArgs;
26+
extern pntrString *g_fullArg;
27+
extern vstring g_fullArgString; /* g_fullArg as one string */
28+
extern vstring g_commandPrompt;
29+
extern vstring g_commandLine;
30+
extern long g_showStatement;
31+
extern vstring g_logFileName;
32+
extern vstring g_texFileName;
33+
extern flag g_PFASmode; /* Proof assistant mode, invoked by PROVE command */
34+
extern flag g_sourceChanged; /* Flag that user made some change to the source file*/
35+
extern flag g_proofChanged; /* Flag that user made some change to proof in progress*/
36+
extern flag g_commandEcho; /* Echo full command */
37+
extern flag g_memoryStatus; /* Always show memory */
38+
39+
extern flag g_sourceHasBeenRead; /* 1 if a source file has been read in */
40+
extern vstring g_rootDirectory; /* Directory to use for included files */
41+
42+
43+
#endif /* METAMATH_MMCMDL_H_ */

‎mmcmds.h‎

Lines changed: 147 additions & 147 deletions
Original file line numberDiff line numberDiff line change
@@ -1,147 +1,147 @@
1-
/*****************************************************************************/
2-
/* Copyright (C) 2020 NORMAN MEGILL nm at alum.mit.edu */
3-
/* License terms: GNU General Public License */
4-
/*****************************************************************************/
5-
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
6-
7-
#ifndef METAMATH_MMCMDS_H_
8-
#define METAMATH_MMCMDS_H_
9-
10-
#include "mmvstr.h"
11-
#include "mmdata.h"
12-
13-
/* Type (i.e. print) a statement */
14-
void typeStatement(long statemNum,
15-
flag briefFlag,
16-
flag commentOnlyFlag,
17-
flag texFlag,
18-
flag htmlFlg);
19-
/* Type (i.e. print) a proof */
20-
void typeProof(long statemNum,
21-
flag pipFlag, /* Type proofInProgress instead of source file proof */
22-
long startStep, long endStep,
23-
long endIndent,
24-
flag essentialFlag,
25-
flag renumberFlag,
26-
flag unknownFlag,
27-
flag notUnifiedFlag,
28-
flag reverseFlag,
29-
flag noIndentFlag,
30-
long startColumn,
31-
flag skipRepeatedSteps,
32-
flag texFlag,
33-
flag htmlFlg);
34-
/* Show details of step */
35-
void showDetailStep(long statemNum, long detailStep);
36-
/* Summary of statements in proof */
37-
void proofStmtSumm(long statemNum, flag essentialFlag, flag texFlag);
38-
/* Traces back the statements used by a proof, recursively. */
39-
flag traceProof(long statemNum,
40-
flag essentialFlag,
41-
flag axiomFlag,
42-
vstring matchList,
43-
vstring traceToList,
44-
flag testOnlyFlag);
45-
void traceProofWork(long statemNum,
46-
flag essentialFlag,
47-
vstring traceToList,
48-
vstring *statementUsedFlagsP, /* 'y'/'n' flag that statement is used */
49-
nmbrString **unprovedListP);
50-
/* Traces back the statements used by a proof, recursively, with tree display.*/
51-
void traceProofTree(long statemNum,
52-
flag essentialFlag, long endIndent);
53-
void traceProofTreeRec(long statemNum,
54-
flag essentialFlag, long endIndent, long recursDepth);
55-
/* Counts the number of steps a completely exploded proof would require */
56-
/* (Recursive) */
57-
/* 0 is returned if some assertions have incomplete proofs. */
58-
double countSteps(long statemNum, flag essentialFlag);
59-
/* Traces what statements require the use of a given statement */
60-
vstring traceUsage(long statemNum,
61-
flag recursiveFlag,
62-
long cutoffStmt /* if nonzero, stop scan there */);
63-
vstring htmlDummyVars(long showStmt);
64-
vstring htmlAllowedSubst(long showStmt);
65-
66-
void readInput(void);
67-
/* WRITE SOURCE command */
68-
void writeSource(
69-
flag reformatFlag /* 1 = "/ FORMAT", 2 = "/REWRAP" */,
70-
flag splitFlag, /* /SPLIT - write out separate $[ $] includes */
71-
flag noVersioningFlag, /* /NO_VERSIONING - no ~1 backup */
72-
flag keepSplitsFlag, /* /KEEP_SPLITS - don't delete included files
73-
when /SPIT is not specified */
74-
vstring extractLabels); /* "" means write everything */
75-
76-
/* Get info for WRITE SOURCE ... / EXTRACT */
77-
void writeExtractedSource(vstring extractLabels, /* EXTRACT argument provided by user */
78-
vstring fullOutput_fn, flag noVersioningFlag);
79-
80-
void fixUndefinedLabels(vstring extractNeeded, vstring *buf);
81-
82-
void writeDict(void);
83-
void eraseSource(void);
84-
void verifyProofs(vstring labelMatch, flag verifyFlag);
85-
86-
87-
/* If checkFiles = 0, do not open external files.
88-
If checkFiles = 1, check mm*.html, presence of gifs, etc. */
89-
void verifyMarkup(vstring labelMatch, flag dateCheck, flag topDateCheck,
90-
flag fileCheck,
91-
flag underscoreCheck,
92-
flag mathboxCheck,
93-
flag verboseMode);
94-
95-
void processMarkup(vstring inputFileName, vstring outputFileName,
96-
flag processCss, long actionBits);
97-
98-
/* List "discouraged" statements with "(Proof modification is discouraged."
99-
and "(New usage is discourged.)" comment markup tags. */
100-
void showDiscouraged(void);
101-
102-
/* Take a relative step FIRST, LAST, +nn, -nn (relative to the unknown
103-
essential steps) or ALL, and return the actual step for use by ASSIGN,
104-
IMPROVE, REPLACE, LET (or 0 in case of ALL, used by IMPROVE). In case
105-
stepStr is an unsigned integer nn, it is assumed to already be an actual
106-
step and is returned as is. If format is illegal, -1 is returned. */
107-
long getStepNum(vstring relStep, /* User's argument */
108-
nmbrString *pfInProgress, /* proofInProgress.proof */
109-
flag allFlag /* 1 = "ALL" is permissable */);
110-
111-
/* Convert the actual step numbers of an unassigned step to the relative
112-
-1, -2, etc. offset for SHOW NEW_PROOF ... /UNKNOWN, to make it easier
113-
for the user to ASSIGN the relative step number. A 0 is returned
114-
for the last unknown step. The step numbers of known steps are
115-
unchanged. */
116-
/* The caller must deallocate the returned nmbrString. */
117-
nmbrString *getRelStepNums(nmbrString *pfInProgress);
118-
119-
/* This procedure finds the next statement number whose label matches
120-
stmtName. Wildcards are allowed. If uniqueFlag is 1,
121-
there must be exactly one match, otherwise an error message is printed,
122-
and -1 is returned. If uniqueFlag is 0, the next match is
123-
returned, or -1 if there are no more matches. No error messages are
124-
printed when uniqueFlag is 0, except for the special case of
125-
startStmt=1. For use by PROVE, REPLACE, ASSIGN. */
126-
long getStatementNum(vstring stmtName, /* Possibly with wildcards */
127-
long startStmt, /* Starting statement number (1 for full scan) */
128-
long maxStmt, /* Must be LESS THAN this statement number */
129-
flag aAllowed, /* 1 means $a is allowed */
130-
flag pAllowed, /* 1 means $p is allowed */
131-
flag eAllowed, /* 1 means $e is allowed */
132-
flag fAllowed, /* 1 means $f is allowed */
133-
flag efOnlyForMaxStmt, /* If 1, $e and $f must belong to maxStmt */
134-
flag uniqueFlag); /* If 1, match must be unique */
135-
136-
/* For HELP processing */
137-
extern flag g_printHelp;
138-
void H(vstring helpLine);
139-
140-
/* For MIDI files */
141-
extern flag g_midiFlag; /* Set to 1 if typeProof() is to output MIDI file */
142-
extern vstring g_midiParam; /* Parameter string for MIDI file */
143-
void outputMidi(long plen, nmbrString *indentationLevels,
144-
nmbrString *logicalFlags, vstring g_midiParameter, vstring statementLabel);
145-
146-
147-
#endif /* METAMATH_MMCMDS_H_ */
1+
/*****************************************************************************/
2+
/* Copyright (C) 2020 NORMAN MEGILL nm at alum.mit.edu */
3+
/* License terms: GNU General Public License */
4+
/*****************************************************************************/
5+
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
6+
7+
#ifndef METAMATH_MMCMDS_H_
8+
#define METAMATH_MMCMDS_H_
9+
10+
#include "mmvstr.h"
11+
#include "mmdata.h"
12+
13+
/* Type (i.e. print) a statement */
14+
void typeStatement(long statemNum,
15+
flag briefFlag,
16+
flag commentOnlyFlag,
17+
flag texFlag,
18+
flag htmlFlg);
19+
/* Type (i.e. print) a proof */
20+
void typeProof(long statemNum,
21+
flag pipFlag, /* Type proofInProgress instead of source file proof */
22+
long startStep, long endStep,
23+
long endIndent,
24+
flag essentialFlag,
25+
flag renumberFlag,
26+
flag unknownFlag,
27+
flag notUnifiedFlag,
28+
flag reverseFlag,
29+
flag noIndentFlag,
30+
long startColumn,
31+
flag skipRepeatedSteps,
32+
flag texFlag,
33+
flag htmlFlg);
34+
/* Show details of step */
35+
void showDetailStep(long statemNum, long detailStep);
36+
/* Summary of statements in proof */
37+
void proofStmtSumm(long statemNum, flag essentialFlag, flag texFlag);
38+
/* Traces back the statements used by a proof, recursively. */
39+
flag traceProof(long statemNum,
40+
flag essentialFlag,
41+
flag axiomFlag,
42+
vstring matchList,
43+
vstring traceToList,
44+
flag testOnlyFlag);
45+
void traceProofWork(long statemNum,
46+
flag essentialFlag,
47+
vstring traceToList,
48+
vstring *statementUsedFlagsP, /* 'y'/'n' flag that statement is used */
49+
nmbrString **unprovedListP);
50+
/* Traces back the statements used by a proof, recursively, with tree display.*/
51+
void traceProofTree(long statemNum,
52+
flag essentialFlag, long endIndent);
53+
void traceProofTreeRec(long statemNum,
54+
flag essentialFlag, long endIndent, long recursDepth);
55+
/* Counts the number of steps a completely exploded proof would require */
56+
/* (Recursive) */
57+
/* 0 is returned if some assertions have incomplete proofs. */
58+
double countSteps(long statemNum, flag essentialFlag);
59+
/* Traces what statements require the use of a given statement */
60+
vstring traceUsage(long statemNum,
61+
flag recursiveFlag,
62+
long cutoffStmt /* if nonzero, stop scan there */);
63+
vstring htmlDummyVars(long showStmt);
64+
vstring htmlAllowedSubst(long showStmt);
65+
66+
void readInput(void);
67+
/* WRITE SOURCE command */
68+
void writeSource(
69+
flag reformatFlag /* 1 = "/ FORMAT", 2 = "/REWRAP" */,
70+
flag splitFlag, /* /SPLIT - write out separate $[ $] includes */
71+
flag noVersioningFlag, /* /NO_VERSIONING - no ~1 backup */
72+
flag keepSplitsFlag, /* /KEEP_SPLITS - don't delete included files
73+
when /SPIT is not specified */
74+
vstring extractLabels); /* "" means write everything */
75+
76+
/* Get info for WRITE SOURCE ... / EXTRACT */
77+
void writeExtractedSource(vstring extractLabels, /* EXTRACT argument provided by user */
78+
vstring fullOutput_fn, flag noVersioningFlag);
79+
80+
void fixUndefinedLabels(vstring extractNeeded, vstring *buf);
81+
82+
void writeDict(void);
83+
void eraseSource(void);
84+
void verifyProofs(vstring labelMatch, flag verifyFlag);
85+
86+
87+
/* If checkFiles = 0, do not open external files.
88+
If checkFiles = 1, check mm*.html, presence of gifs, etc. */
89+
void verifyMarkup(vstring labelMatch, flag dateCheck, flag topDateCheck,
90+
flag fileCheck,
91+
flag underscoreCheck,
92+
flag mathboxCheck,
93+
flag verboseMode);
94+
95+
void processMarkup(vstring inputFileName, vstring outputFileName,
96+
flag processCss, long actionBits);
97+
98+
/* List "discouraged" statements with "(Proof modification is discouraged."
99+
and "(New usage is discourged.)" comment markup tags. */
100+
void showDiscouraged(void);
101+
102+
/* Take a relative step FIRST, LAST, +nn, -nn (relative to the unknown
103+
essential steps) or ALL, and return the actual step for use by ASSIGN,
104+
IMPROVE, REPLACE, LET (or 0 in case of ALL, used by IMPROVE). In case
105+
stepStr is an unsigned integer nn, it is assumed to already be an actual
106+
step and is returned as is. If format is illegal, -1 is returned. */
107+
long getStepNum(vstring relStep, /* User's argument */
108+
nmbrString *pfInProgress, /* proofInProgress.proof */
109+
flag allFlag /* 1 = "ALL" is permissable */);
110+
111+
/* Convert the actual step numbers of an unassigned step to the relative
112+
-1, -2, etc. offset for SHOW NEW_PROOF ... /UNKNOWN, to make it easier
113+
for the user to ASSIGN the relative step number. A 0 is returned
114+
for the last unknown step. The step numbers of known steps are
115+
unchanged. */
116+
/* The caller must deallocate the returned nmbrString. */
117+
nmbrString *getRelStepNums(nmbrString *pfInProgress);
118+
119+
/* This procedure finds the next statement number whose label matches
120+
stmtName. Wildcards are allowed. If uniqueFlag is 1,
121+
there must be exactly one match, otherwise an error message is printed,
122+
and -1 is returned. If uniqueFlag is 0, the next match is
123+
returned, or -1 if there are no more matches. No error messages are
124+
printed when uniqueFlag is 0, except for the special case of
125+
startStmt=1. For use by PROVE, REPLACE, ASSIGN. */
126+
long getStatementNum(vstring stmtName, /* Possibly with wildcards */
127+
long startStmt, /* Starting statement number (1 for full scan) */
128+
long maxStmt, /* Must be LESS THAN this statement number */
129+
flag aAllowed, /* 1 means $a is allowed */
130+
flag pAllowed, /* 1 means $p is allowed */
131+
flag eAllowed, /* 1 means $e is allowed */
132+
flag fAllowed, /* 1 means $f is allowed */
133+
flag efOnlyForMaxStmt, /* If 1, $e and $f must belong to maxStmt */
134+
flag uniqueFlag); /* If 1, match must be unique */
135+
136+
/* For HELP processing */
137+
extern flag g_printHelp;
138+
void H(vstring helpLine);
139+
140+
/* For MIDI files */
141+
extern flag g_midiFlag; /* Set to 1 if typeProof() is to output MIDI file */
142+
extern vstring g_midiParam; /* Parameter string for MIDI file */
143+
void outputMidi(long plen, nmbrString *indentationLevels,
144+
nmbrString *logicalFlags, vstring g_midiParameter, vstring statementLabel);
145+
146+
147+
#endif /* METAMATH_MMCMDS_H_ */

0 commit comments

Comments
 (0)