245 lines
10 KiB
C
245 lines
10 KiB
C
/*****************************************************************************/
|
|
/* 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*/
|
|
|
|
#ifndef METAMATH_MMWTEX_H_
|
|
#define METAMATH_MMWTEX_H_
|
|
|
|
#include "mmvstr.h"
|
|
#include "mmdata.h"
|
|
|
|
/* Colors for HTML pages. */
|
|
#define GREEN_TITLE_COLOR "\"#006633\""
|
|
#define MINT_BACKGROUND_COLOR "\"#EEFFFA\""
|
|
#define PINK_NUMBER_COLOR "\"#FA8072\"" /* =salmon; was FF6666 */
|
|
#define PURPLISH_BIBLIO_COLOR "\"#FAEEFF\""
|
|
|
|
|
|
/* 29-Jul-2008 nm Sandbox stuff */
|
|
#define SANDBOX_COLOR "\"#FFFFD9\""
|
|
|
|
/* TeX flags */
|
|
/* 14-Sep-2010 nm Removed simpleTexFlag; added g_oldTexFlag */
|
|
extern flag g_oldTexFlag; /* Use macros in output; obsolete; take out someday */
|
|
|
|
/* HTML flags */
|
|
extern flag g_htmlFlag; /* HTML flag: 0 = TeX, 1 = HTML */
|
|
extern flag g_altHtmlFlag; /* Use "althtmldef" instead of "htmldef". This is
|
|
intended to allow the generation of pages with the old Symbol font
|
|
instead of the individual GIF files. */
|
|
extern flag g_briefHtmlFlag; /* Output statement only, for statement display
|
|
in other HTML pages, such as the Proof Explorer home page */
|
|
extern long g_extHtmlStmt; /* At this statement and above, use the exthtmlxxx
|
|
variables for title, links, etc. This was put in to allow proper
|
|
generation of the Hilbert Space Explorer extension to the set.mm
|
|
database. */
|
|
extern vstring g_extHtmlTitle; /* Title of extended section if any; set by
|
|
by exthtmltitle command in special $t comment of database source */
|
|
extern vstring g_htmlVarColor; /* Set by htmlvarcolor commands */
|
|
/* Added 26-Aug-2017 nm for use by mmcmds.c */
|
|
extern vstring g_htmlHome; /* Set by htmlhome command */
|
|
/* Added 10/13/02 for use in metamath.c bibliography cross-reference */
|
|
extern vstring g_htmlBibliography; /* Optional; set by htmlbibliography command */
|
|
extern vstring g_extHtmlBibliography; /* Optional; set by exthtmlbibliography
|
|
command */
|
|
extern vstring g_htmlCSS; /* Set by htmlcss commands */ /* 14-Jan-2016 nm */
|
|
/* Added 14-Jan-2016 */
|
|
extern vstring g_htmlFont; /* Optional; set by g_htmlFont command */
|
|
|
|
void eraseTexDefs(void); /* Undo readTexDefs() */
|
|
|
|
/* TeX/HTML/ALT_HTML word-processor-specific routines */
|
|
/* Returns 2 if there were severe parsing errors, 1 if there were warnings but
|
|
no errors, 0 if no errors or warnings */
|
|
flag readTexDefs(
|
|
flag errorsOnly, /* 1 = supprees non-error messages */
|
|
flag noGifCheck /* 1 = don't check for missing GIFs */);
|
|
|
|
extern flag g_texDefsRead;
|
|
struct texDef_struct { /* 27-Oct-2012 nm Made global for "erase" */
|
|
vstring tokenName; /* ASCII token */
|
|
vstring texEquiv; /* Converted to TeX */
|
|
};
|
|
extern struct texDef_struct *g_TexDefs; /* 27-Oct-2012 nm Now glob for "erase" */
|
|
|
|
|
|
long texDefWhiteSpaceLen(char *ptr);
|
|
long texDefTokenLen(char *ptr);
|
|
/* Token comparison for qsort */
|
|
int texSortCmp(const void *key1, const void *key2);
|
|
/* Token comparison for bsearch */
|
|
int texSrchCmp(const void *key, const void *data);
|
|
/* Convert ascii to a string of \tt tex */
|
|
/* (The caller must surround it by {\tt }) */
|
|
vstring asciiToTt(vstring s);
|
|
vstring tokenToTex(vstring mtoken, long statemNum);
|
|
/* Converts a comment section in math mode to TeX. Each math token
|
|
MUST be separated by white space. TeX "$" does not surround the output. */
|
|
vstring asciiMathToTex(vstring mathComment, long statemNum);
|
|
/* Gets the next section of a comment that is in the current mode (text,
|
|
label, or math). If 1st char. is not "$", text mode is assumed.
|
|
mode = 0 means end of comment reached. srcptr is left at 1st char.
|
|
of start of next comment section. */
|
|
vstring getCommentModeSection(vstring *srcptr, char *mode);
|
|
void printTexHeader(flag texHeaderFlag);
|
|
|
|
/* Prints an embedded comment in TeX. The commentPtr must point to the first
|
|
character after the "$(" in the comment. The printout ends when the first
|
|
"$)" or null character is encountered. commentPtr must not be a temporary
|
|
allocation. htmlCenterFlag, if 1, means to center the HTML and add a
|
|
"Description:" prefix.*/
|
|
/* void printTexComment(vstring commentPtr, char htmlCenterFlag); */
|
|
/* 17-Nov-2015 nm Added 3rd & 4th arguments; returns 1 if error/warning */
|
|
flag printTexComment(vstring commentPtr, /* Sends result to g_texFilePtr */
|
|
flag htmlCenterFlag, /* 1 = htmlCenterFlag */
|
|
long actionBits, /* see indicators below */
|
|
flag noFileCheck /* 1 = noFileCheck */);
|
|
/* Indicators for actionBits */
|
|
#define ERRORS_ONLY 1
|
|
#define PROCESS_SYMBOLS 2
|
|
#define PROCESS_LABELS 4
|
|
#define ADD_COLORED_LABEL_NUMBER 8
|
|
#define PROCESS_BIBREFS 16
|
|
#define PROCESS_UNDERSCORES 32
|
|
/* CONVERT_TO_HTML means '<' to '<'; unless <HTML> in comment (and strip it) */
|
|
#define CONVERT_TO_HTML 64
|
|
/* METAMATH_COMMENT means $) (as well as end-of-string) terminates string. */
|
|
#define METAMATH_COMMENT 128
|
|
/* PROCESS_ALL is for convenience */
|
|
#define PROCESS_EVERYTHING PROCESS_SYMBOLS + PROCESS_LABELS \
|
|
+ ADD_COLORED_LABEL_NUMBER + PROCESS_BIBREFS \
|
|
+ PROCESS_UNDERSCORES + CONVERT_TO_HTML + METAMATH_COMMENT
|
|
|
|
void printTexLongMath(nmbrString *proofStep, vstring startPrefix,
|
|
vstring contPrefix, long hypStmt, long indentationLevel);
|
|
void printTexTrailer(flag texHeaderFlag);
|
|
|
|
/* Added 4-Dec-03
|
|
Function implementing WRITE THEOREM_LIST / THEOREMS_PER_PAGE nn */
|
|
void writeTheoremList(long theoremsPerPage, flag showLemmas,
|
|
flag noVersioning);
|
|
|
|
#define HUGE_DECORATION "####"
|
|
#define BIG_DECORATION "#*#*"
|
|
#define SMALL_DECORATION "=-=-"
|
|
#define TINY_DECORATION "-.-."
|
|
|
|
/* 2-Aug-2009 nm - broke this function out from writeTheoremList() */
|
|
/* 20-Jun-2014 nm - added hugeHdrAddr */
|
|
/* 21-Aug-2017 nm - added tinyHdrAddr */
|
|
/* 6-Aug-2019 nm - changed return type from void to flag (=char) */
|
|
/* 24-Aug-2020 nm - added fineResolution */
|
|
/* 12-Sep-2020 nm - added fullComment */
|
|
flag getSectionHeadings(long stmt, vstring *hugeHdrTitle,
|
|
vstring *bigHdrTitle,
|
|
vstring *smallHdrTitle,
|
|
vstring *tinyHdrTitle,
|
|
/* Added 8-May-2015 nm */
|
|
vstring *hugeHdrComment,
|
|
vstring *bigHdrComment,
|
|
vstring *smallHdrComment,
|
|
vstring *tinyHdrComment,
|
|
/* Added 24-Aug-2020 nm */
|
|
flag fineResolution, /* 0 = consider just successive $a/$p, 1 = all stmts */
|
|
flag fullComment /* 1 = put $( + header + comment + $) into xxxHdrTitle */
|
|
);
|
|
|
|
/****** 15-Aug-2020 nm Obsolete
|
|
/@ TeX symbol dictionary @/
|
|
extern FILE @g_tex_dict_fp; /@ File pointers @/
|
|
extern vstring g_tex_dict_fn; /@ File names @/
|
|
******/
|
|
|
|
/* TeX normal output */
|
|
extern flag g_texFileOpenFlag;
|
|
extern FILE *g_texFilePtr;
|
|
|
|
/* Pink statement number for HTML pages */
|
|
/* 10/10/02 (This is no longer used?) */
|
|
/*
|
|
long pinkNumber(long statemNum);
|
|
*/
|
|
|
|
/* Pink statement number HTML code for HTML pages - added 10/10/02 */
|
|
/* Warning: caller must deallocate returned string */
|
|
vstring pinkHTML(long statemNum);
|
|
|
|
/* Pink statement number range HTML code for HTML pages, separated by a
|
|
"-" - added 24-Aug-04 */
|
|
/* Warning: caller must deallocate returned string */
|
|
vstring pinkRangeHTML(long statemNum1, long statemNum2);
|
|
|
|
#define PINK_NBSP " " /* Either "" or " " depending on taste, it is
|
|
the separator between a statement href and its pink number */
|
|
|
|
/* 30-Jan-04 nm Comment out the following line to go back to the pink-only
|
|
color for the little statement numbers on the HTML pages */
|
|
#define RAINBOW_OPTION /* "Rainbow" instead of pink color for little numbers */
|
|
|
|
#ifdef RAINBOW_OPTION
|
|
/* This function converts a "spectrum" color (1 to maxColor) to an
|
|
RBG value in hex notation for HTML. The caller must deallocate the
|
|
returned vstring. color = 1 (red) to maxColor (violet). */
|
|
/* ndm 10-Jan-04 */
|
|
vstring spectrumToRGB(long color, long maxColor);
|
|
#endif
|
|
|
|
#define INDENT_HTML_PROOFS /* nm 3-Feb-04 - indentation experiment */
|
|
|
|
/* Added 20-Sep-03 (broken out of printTexLongMath() for better
|
|
modularization) */
|
|
/* Returns the HTML code for GIFs (!g_altHtmlFlag) or Unicode (g_altHtmlFlag),
|
|
or LaTeX when !g_htmlFlag, for the math string (hypothesis or conclusion) that
|
|
is passed in. */
|
|
/* Warning: The caller must deallocate the returned vstring. */
|
|
vstring getTexLongMath(nmbrString *mathString, long statemNum);
|
|
|
|
/* Added 18-Sep-03 (transferred from metamath.c) */
|
|
/* Returns the TeX, or HTML code for GIFs (!g_altHtmlFlag) or Unicode
|
|
(g_altHtmlFlag), for a statement's hypotheses and assertion in the form
|
|
hyp & ... & hyp => assertion */
|
|
/* Warning: The caller must deallocate the returned vstring. */
|
|
/* 14-Sep-2010 nm Changed name from getHTMLHypAndAssertion() */
|
|
vstring getTexOrHtmlHypAndAssertion(long statemNum);
|
|
|
|
/* Added 17-Nov-2015 (broken out of metamath.c for better modularization) */
|
|
/* For WRITE BIBLIOGRAPHY command and error checking by VERIFY MARKUP */
|
|
/* Returns 0 if OK, 1 if error or warning found */
|
|
flag writeBibliography(vstring bibFile,
|
|
vstring labelMatch, /* Normally "*" except by verifyMarkup() */
|
|
flag errorsOnly, /* 1 = no output, just warning msgs if any */
|
|
flag noFileCheck); /* 1 = ignore missing external files (gifs, bib, etc.) */
|
|
|
|
/* 5-Aug-2020 nm */
|
|
/* Globals to hold mathbox information. They should be re-initialized
|
|
by the ERASE command (eraseSource()). g_mathboxStmt = 0 indicates
|
|
it and the other variables haven't been initialized. */
|
|
extern long g_mathboxStmt; /* stmt# of "mathbox" label; statements+1 if none */
|
|
extern long g_mathboxes; /* # of mathboxes */
|
|
/* The following 3 "strings" are 0-based e.g. g_mathboxStart[0] is for
|
|
mathbox #1 */
|
|
extern nmbrString *g_mathboxStart; /* Start stmt vs. mathbox # */
|
|
extern nmbrString *g_mathboxEnd; /* End stmt vs. mathbox # */
|
|
extern pntrString *g_mathboxUser; /* User name vs. mathbox # */
|
|
|
|
/* 5-Aug-2020 nm */
|
|
/* Returns 1 if statements are in different mathboxes */
|
|
flag inDiffMathboxes(long stmt1, long stmt2);
|
|
/* Returns the user of the mathbox that a statement is in, or ""
|
|
if the statement is not in a mathbox. */
|
|
/* Caller should NOT deallocate returned string (it points directly to
|
|
g_mathboxUser[] entry); use directly in print2() messages */
|
|
vstring getMathboxUser(long stmt);
|
|
/* Returns the mathbox number (starting at 1) that stmt is in, or 0 if not
|
|
in a mathbox */
|
|
long getMathboxNum(long stmt);
|
|
/* Populates mathbox information */
|
|
void assignMathboxInfo(void);
|
|
/* Creates lists of mathbox starts and user names */
|
|
long getMathboxLoc(nmbrString **mathboxStart, nmbrString **mathboxEnd,
|
|
pntrString **mathboxUser);
|
|
|
|
#endif /* METAMATH_MMWTEX_H_ */
|