Skip to content

Commit

Permalink
Convert comments to doxygen (#76)
Browse files Browse the repository at this point in the history
  • Loading branch information
digama0 authored Mar 7, 2022
1 parent e49422b commit c1d7148
Show file tree
Hide file tree
Showing 16 changed files with 761 additions and 684 deletions.
24 changes: 13 additions & 11 deletions src/mmcmdl.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@
#define METAMATH_MMCMDL_H_

/*!
* \file mmcmdl.h - includes for accessing the command line interpreter
* \file mmcmdl.h
* \brief includes for accessing the command line interpreter
*/

#include "mmvstr.h"
Expand All @@ -27,7 +28,7 @@ extern pntrString *g_rawArgPntr;
extern nmbrString *g_rawArgNmbr;
extern long g_rawArgs;
extern pntrString *g_fullArg;
extern vstring g_fullArgString; /* g_fullArg as one string */
extern vstring g_fullArgString; /*!< g_fullArg as one string */
/*!
* \var vstring g_commandPrompt
* text displayed at the beginning of the line where a user is supposed to
Expand All @@ -38,21 +39,22 @@ extern vstring g_commandLine;
extern long g_showStatement;
extern vstring g_logFileName;
extern vstring g_texFileName;
extern flag g_PFASmode; /* Proof assistant mode, invoked by PROVE command */
extern flag g_sourceChanged; /* Flag that user made some change to the source file*/
extern flag g_proofChanged; /* Flag that user made some change to proof in progress*/
extern flag g_commandEcho; /* Echo full command */
extern flag g_PFASmode; /*!< Proof assistant mode, invoked by PROVE command */
extern flag g_sourceChanged; /*!< Flag that user made some change to the source file*/
extern flag g_proofChanged; /*!< Flag that user made some change to proof in progress*/
extern flag g_commandEcho; /*!< Echo full command */
/*!
* \brief indicates whether the user has turned MEMORY STATUS on.
* \brief `MEMORY_STATUS` option: Always show memory
*
* If the user issues SET MEMORY_STATUS ON this \a flag is set to 1. It is
* Indicates whether the user has turned MEMORY_STATUS on.
* If the user issues SET MEMORY_STATUS ON this \ref flag is set to 1. It is
* reset to 0 again on a SET MEMORY_STATUS OFF command. When 1, certain
* memory de/allocations are monitored - see \a db3.
*/
extern flag g_memoryStatus; /* Always show memory */
extern flag g_memoryStatus;

extern flag g_sourceHasBeenRead; /* 1 if a source file has been read in */
extern vstring g_rootDirectory; /* Directory to use for included files */
extern flag g_sourceHasBeenRead; /*!< 1 if a source file has been read in */
extern vstring g_rootDirectory; /*!< Directory to use for included files */


#endif /* METAMATH_MMCMDL_H_ */
80 changes: 42 additions & 38 deletions src/mmcmds.h
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,20 @@
#ifndef METAMATH_MMCMDS_H_
#define METAMATH_MMCMDS_H_

/*! \file */

#include "mmvstr.h"
#include "mmdata.h"

/* Type (i.e. print) a statement */
/*! Type (i.e. print) a statement */
void typeStatement(long statemNum,
flag briefFlag,
flag commentOnlyFlag,
flag texFlag,
flag htmlFlag);
/* Type (i.e. print) a proof */
/*! Type (i.e. print) a proof */
void typeProof(long statemNum,
flag pipFlag, /* Type proofInProgress instead of source file proof */
flag pipFlag, /*!< Type proofInProgress instead of source file proof */
long startStep, long endStep,
long endIndent,
flag essentialFlag,
Expand All @@ -31,11 +33,11 @@ void typeProof(long statemNum,
flag skipRepeatedSteps,
flag texFlag,
flag htmlFlag);
/* Show details of step */
/*! Show details of step */
void showDetailStep(long statemNum, long detailStep);
/* Summary of statements in proof */
/*! Summary of statements in proof */
void proofStmtSumm(long statemNum, flag essentialFlag, flag texFlag);
/* Traces back the statements used by a proof, recursively. */
/*! Traces back the statements used by a proof, recursively. */
flag traceProof(long statemNum,
flag essentialFlag,
flag axiomFlag,
Expand All @@ -45,26 +47,26 @@ flag traceProof(long statemNum,
void traceProofWork(long statemNum,
flag essentialFlag,
vstring traceToList,
vstring *statementUsedFlagsP, /* 'y'/'n' flag that statement is used */
vstring *statementUsedFlagsP, /*!< 'y'/'n' flag that statement is used */
nmbrString **unprovedListP);
/* Traces back the statements used by a proof, recursively, with tree display.*/
/*! Traces back the statements used by a proof, recursively, with tree display.*/
void traceProofTree(long statemNum,
flag essentialFlag, long endIndent);
void traceProofTreeRec(long statemNum,
flag essentialFlag, long endIndent, long recursDepth);
/* Counts the number of steps a completely exploded proof would require */
/* (Recursive) */
/* 0 is returned if some assertions have incomplete proofs. */
/*! Counts the number of steps a completely exploded proof would require
(Recursive)
0 is returned if some assertions have incomplete proofs. */
double countSteps(long statemNum, flag essentialFlag);
/* Traces what statements require the use of a given statement */
/*! Traces what statements require the use of a given statement */
vstring traceUsage(long statemNum,
flag recursiveFlag,
long cutoffStmt /* if nonzero, stop scan there */);
vstring htmlDummyVars(long showStmt);
vstring htmlAllowedSubst(long showStmt);

void readInput(void);
/* WRITE SOURCE command */
/*! WRITE SOURCE command */
void writeSource(
flag reformatFlag /* 1 = "/ FORMAT", 2 = "/REWRAP" */,
flag splitFlag, /* /SPLIT - write out separate $[ $] includes */
Expand All @@ -73,7 +75,7 @@ void writeSource(
when /SPIT is not specified */
vstring extractLabels); /* "" means write everything */

/* Get info for WRITE SOURCE ... / EXTRACT */
/*! Get info for WRITE SOURCE ... / EXTRACT */
void writeExtractedSource(vstring extractLabels, /* EXTRACT argument provided by user */
vstring fullOutput_fn, flag noVersioningFlag);

Expand All @@ -84,7 +86,7 @@ void eraseSource(void);
void verifyProofs(vstring labelMatch, flag verifyFlag);


/* If checkFiles = 0, do not open external files.
/*! If checkFiles = 0, do not open external files.
If checkFiles = 1, check for presence of gifs and biblio file */
void verifyMarkup(vstring labelMatch, flag dateCheck, flag topDateCheck,
flag fileCheck,
Expand All @@ -95,51 +97,53 @@ void verifyMarkup(vstring labelMatch, flag dateCheck, flag topDateCheck,
void processMarkup(vstring inputFileName, vstring outputFileName,
flag processCss, long actionBits);

/* List "discouraged" statements with "(Proof modification is discouraged."
/*! List "discouraged" statements with "(Proof modification is discouraged."
and "(New usage is discouraged.)" comment markup tags. */
void showDiscouraged(void);

/* Take a relative step FIRST, LAST, +nn, -nn (relative to the unknown
/*! Take a relative step FIRST, LAST, +nn, -nn (relative to the unknown
essential steps) or ALL, and return the actual step for use by ASSIGN,
IMPROVE, REPLACE, LET (or 0 in case of ALL, used by IMPROVE). In case
stepStr is an unsigned integer nn, it is assumed to already be an actual
step and is returned as is. If format is illegal, -1 is returned. */
long getStepNum(vstring relStep, /* User's argument */
nmbrString *pfInProgress, /* proofInProgress.proof */
flag allFlag /* 1 = "ALL" is permissible */);
long getStepNum(vstring relStep, /*!< User's argument */
nmbrString *pfInProgress, /*!< proofInProgress.proof */
flag allFlag /*!< 1 = "ALL" is permissible */);

/* Convert the actual step numbers of an unassigned step to the relative
/*! Convert the actual step numbers of an unassigned step to the relative
-1, -2, etc. offset for SHOW NEW_PROOF ... /UNKNOWN, to make it easier
for the user to ASSIGN the relative step number. A 0 is returned
for the last unknown step. The step numbers of known steps are
unchanged. */
/* The caller must deallocate the returned nmbrString. */
unchanged.
The caller must deallocate the returned nmbrString. */
nmbrString *getRelStepNums(nmbrString *pfInProgress);

/* This procedure finds the next statement number whose label matches
/*! This procedure finds the next statement number whose label matches
stmtName. Wildcards are allowed. If uniqueFlag is 1,
there must be exactly one match, otherwise an error message is printed,
and -1 is returned. If uniqueFlag is 0, the next match is
returned, or -1 if there are no more matches. No error messages are
printed when uniqueFlag is 0, except for the special case of
startStmt=1. For use by PROVE, REPLACE, ASSIGN. */
long getStatementNum(vstring stmtName, /* Possibly with wildcards */
long startStmt, /* Starting statement number (1 for full scan) */
long maxStmt, /* Must be LESS THAN this statement number */
flag aAllowed, /* 1 means $a is allowed */
flag pAllowed, /* 1 means $p is allowed */
flag eAllowed, /* 1 means $e is allowed */
flag fAllowed, /* 1 means $f is allowed */
flag efOnlyForMaxStmt, /* If 1, $e and $f must belong to maxStmt */
flag uniqueFlag); /* If 1, match must be unique */

/* For HELP processing */
long getStatementNum(
vstring stmtName, /*!< Possibly with wildcards */
long startStmt, /*!< Starting statement number (1 for full scan) */
long maxStmt, /*!< Must be LESS THAN this statement number */
flag aAllowed, /*!< 1 means $a is allowed */
flag pAllowed, /*!< 1 means $p is allowed */
flag eAllowed, /*!< 1 means $e is allowed */
flag fAllowed, /*!< 1 means $f is allowed */
flag efOnlyForMaxStmt, /*!< If 1, $e and $f must belong to maxStmt */
flag uniqueFlag /*!< If 1, match must be unique */
);

/*! For HELP processing */
extern flag g_printHelp;
void H(vstring helpLine);

/* For MIDI files */
extern flag g_midiFlag; /* Set to 1 if typeProof() is to output MIDI file */
extern vstring g_midiParam; /* Parameter string for MIDI file */
/*! For MIDI files */
extern flag g_midiFlag; /*!< Set to 1 if typeProof() is to output MIDI file */
extern vstring g_midiParam; /*!< Parameter string for MIDI file */
void outputMidi(long plen, nmbrString *indentationLevels,
nmbrString *logicalFlags, vstring g_midiParameter, vstring statementLabel);

Expand Down
9 changes: 0 additions & 9 deletions src/mmdata.c
Original file line number Diff line number Diff line change
Expand Up @@ -2448,9 +2448,6 @@ temp_pntrString *pntrTempAlloc(long size) {
}


/* Make string have temporary allocation to be released by next pntrLet() */
/* Warning: after pntrMakeTempAlloc() is called, the pntrString may NOT be
assigned again with pntrLet() */
temp_pntrString *pntrMakeTempAlloc(pntrString *s) {
if (g_pntrTempAllocStackTop>=(M_MAX_ALLOC_STACK-1)) {
printf(
Expand All @@ -2469,12 +2466,6 @@ temp_pntrString *pntrMakeTempAlloc(pntrString *s) {
}


/* pntrString assignment */
/* This function must ALWAYS be called to make assignment to */
/* a pntrString in order for the memory cleanup routines, etc. */
/* to work properly. If a pntrString has never been assigned before, */
/* it is the user's responsibility to initialize it to NULL_PNTRSTRING (the */
/* null string). */
void pntrLet(pntrString **target, const pntrString *source) {
long targetLength,sourceLength;
long targetAllocLen;
Expand Down
Loading

0 comments on commit c1d7148

Please sign in to comment.