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