From 684d3bd252e55e207f77ac9f0866fd199302654f Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sun, 20 Aug 2023 17:04:19 +0200 Subject: [PATCH 01/10] add handling of double underscores --- src/mmhlpa.c | 4 +++- src/mmwtex.c | 26 ++++++++++++++++++++++++++ 2 files changed, 29 insertions(+), 1 deletion(-) diff --git a/src/mmhlpa.c b/src/mmhlpa.c index 36019a0c..4a52debf 100644 --- a/src/mmhlpa.c +++ b/src/mmhlpa.c @@ -635,7 +635,9 @@ H("interpreted by / SYMBOLS, / LABELS, and / BIB_REFS respectively, escape"); H("them with \"``\", \"~~\", and \"[[\" in the input file. Literal \"`\""); H("must always be escaped even if / SYMBOLS is omitted, because the"); H("algorithm will still use \"`...`\" to avoid interpreting special"); -H("characters in math symbols."); +H("characters in math symbols. Similarly, use a double underscore to"); +H("display one underscore \"_\" and not trigger an italic font or"); +H("subscripts."); H(""); } diff --git a/src/mmwtex.c b/src/mmwtex.c index ca1247c9..600aa502 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -1964,6 +1964,32 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, continue; } + /* Double-underscore handling: double-underscores are "escaped + underscores", so replace a double-underscore with a single + underscore and do not modify italic or subscript. */ + if (cmt[pos1 + 1] == '_') { + if (g_htmlFlag) { /* HTML */ + let(&cmt, cat(left(cmt, pos1 - 1), + "_", + seg(cmt, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ + "", right(cmt, pos1+2), NULL)); + let(&cmtMasked, cat(left(cmtMasked, pos1 - 1), + "_", + seg(cmtMasked, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ + "", right(cmtMasked, pos1+2), NULL)); + pos1 ++; /* Adjust for 1 extra char '_' */ + } else { /* LaTeX */ + let(&cmt, cat(left(cmt, pos1 - 1), "\texttt{\_}", + seg(cmt, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ + "", right(cmt, pos2), NULL)); + let(&cmtMasked, cat(left(cmtMasked, pos1 - 1), "$_{", + seg(cmtMasked, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ + "", right(cmtMasked, pos1 + 2), NULL)); + pos1 = pos1 + 11; /* Adjust for 11 extra chars "\texttt{\_}" */ + } + continue; + } /* End of double-underscore handling */ + // Opening "_" must be _ for tag if (pos1 > 1) { // Check for not whitespace and not opening punctuation From 49724dfd5613f2069046a2754db6aeaf46fad0ed Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sun, 20 Aug 2023 17:21:56 +0200 Subject: [PATCH 02/10] typo --- src/mmwtex.c | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/mmwtex.c b/src/mmwtex.c index 600aa502..2a6eab3a 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -1972,17 +1972,19 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, let(&cmt, cat(left(cmt, pos1 - 1), "_", seg(cmt, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ - "", right(cmt, pos1+2), NULL)); + "", right(cmt, pos1 + 2), NULL)); let(&cmtMasked, cat(left(cmtMasked, pos1 - 1), "_", seg(cmtMasked, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ - "", right(cmtMasked, pos1+2), NULL)); + "", right(cmtMasked, pos1 + 2), NULL)); pos1 ++; /* Adjust for 1 extra char '_' */ } else { /* LaTeX */ - let(&cmt, cat(left(cmt, pos1 - 1), "\texttt{\_}", + let(&cmt, cat(left(cmt, pos1 - 1), + "\texttt{\_}", seg(cmt, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ - "", right(cmt, pos2), NULL)); - let(&cmtMasked, cat(left(cmtMasked, pos1 - 1), "$_{", + "", right(cmt, pos1 + 2), NULL)); + let(&cmtMasked, cat(left(cmtMasked, pos1 - 1), + "\texttt{\_}", seg(cmtMasked, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ "", right(cmtMasked, pos1 + 2), NULL)); pos1 = pos1 + 11; /* Adjust for 11 extra chars "\texttt{\_}" */ From 567de4e63f5c7bd51d6479c50eb92d85150cb949 Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sun, 20 Aug 2023 17:24:10 +0200 Subject: [PATCH 03/10] simplify --- src/mmwtex.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/mmwtex.c b/src/mmwtex.c index 2a6eab3a..e94199fc 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -1969,12 +1969,12 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, underscore and do not modify italic or subscript. */ if (cmt[pos1 + 1] == '_') { if (g_htmlFlag) { /* HTML */ - let(&cmt, cat(left(cmt, pos1 - 1), - "_", + let(&cmt, cat(left(cmt, pos1), + "", seg(cmt, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ "", right(cmt, pos1 + 2), NULL)); - let(&cmtMasked, cat(left(cmtMasked, pos1 - 1), - "_", + let(&cmtMasked, cat(left(cmtMasked, pos1), + "", seg(cmtMasked, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ "", right(cmtMasked, pos1 + 2), NULL)); pos1 ++; /* Adjust for 1 extra char '_' */ From 44830f73f8ed0aeb11538b50bbe0e4ee55fbab60 Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sat, 2 Sep 2023 13:58:15 +0200 Subject: [PATCH 04/10] fix double-underscore handling --- src/mmwtex.c | 45 +++++++++++++++++++-------------------------- 1 file changed, 19 insertions(+), 26 deletions(-) diff --git a/src/mmwtex.c b/src/mmwtex.c index e94199fc..4ca9c36e 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -1963,34 +1963,27 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, if (!strcmp(mid(cmt, pos2 + 2, 2), "mm")) { continue; } - - /* Double-underscore handling: double-underscores are "escaped - underscores", so replace a double-underscore with a single - underscore and do not modify italic or subscript. */ - if (cmt[pos1 + 1] == '_') { - if (g_htmlFlag) { /* HTML */ - let(&cmt, cat(left(cmt, pos1), - "", - seg(cmt, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ - "", right(cmt, pos1 + 2), NULL)); - let(&cmtMasked, cat(left(cmtMasked, pos1), - "", - seg(cmtMasked, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ - "", right(cmtMasked, pos1 + 2), NULL)); - pos1 ++; /* Adjust for 1 extra char '_' */ - } else { /* LaTeX */ - let(&cmt, cat(left(cmt, pos1 - 1), - "\texttt{\_}", - seg(cmt, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ - "", right(cmt, pos1 + 2), NULL)); - let(&cmtMasked, cat(left(cmtMasked, pos1 - 1), - "\texttt{\_}", - seg(cmtMasked, pos1 + 1, pos1 + 2), /* Skip (delete) "_" */ - "", right(cmtMasked, pos1 + 2), NULL)); - pos1 = pos1 + 11; /* Adjust for 11 extra chars "\texttt{\_}" */ + // Double-underscore handling: double-underscores are "escaped + // underscores", so replace a double-underscore with a single + // underscore and do not modify italic or subscript. + if (cmt[pos1] == '_') { + if (g_htmlFlag) { // HTML + let(&cmt, cat(left(cmt, pos1), // Skip (delete) "_" + right(cmt, pos1 + 2), NULL)); + let(&cmtMasked, cat(left(cmtMasked, pos1), // Skip (delete) "_" + right(cmtMasked, pos1 + 2), NULL)); + pos1 ++; // Adjust for 1 extra char '_' + } else { // LaTeX + let(&cmt, cat(left(cmt, pos1 - 1), // Skip (delete) "_" + "\\texttt{\\_}", + right(cmt, pos1 + 2), NULL)); + let(&cmtMasked, cat(left(cmtMasked, pos1 - 1), // Skip (delete) "_" + "\\texttt{\\_}", + right(cmtMasked, pos1 + 2), NULL)); + pos1 = pos1 + 11; // Adjust for 11 extra chars "\texttt{\_}" } continue; - } /* End of double-underscore handling */ + } // End of double-underscore handling // Opening "_" must be _ for tag if (pos1 > 1) { From 99361578510ee3bb951a60231e056dbda0364f86 Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sat, 2 Sep 2023 14:24:04 +0200 Subject: [PATCH 05/10] add underscores test --- tests/underscores.expected | 104 +++++++++++++++++++++++++++++++++++++ tests/underscores.in | 2 + tests/underscores.mm | 9 ++++ 3 files changed, 115 insertions(+) create mode 100644 tests/underscores.expected create mode 100644 tests/underscores.in create mode 100644 tests/underscores.mm diff --git a/tests/underscores.expected b/tests/underscores.expected new file mode 100644 index 00000000..40f682ff --- /dev/null +++ b/tests/underscores.expected @@ -0,0 +1,104 @@ +MM> READ "underscores.mm" +Reading source file "underscores.mm"... 171 bytes +171 bytes were read into the source buffer. +The source has 2 statements; 1 are $a and 0 are $p. +SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. +No errors were found. However, proofs were not checked. Type VERIFY PROOF * +if you want to check them. +MM> Continuous scrolling is now in effect. +MM> Creating HTML file "b.html"... +Reading definitions from $t statement of underscores.mm... +1 typesetting statements were read from "underscores.mm". +MM> + + + + + + +b - Metamath Test Page + + + + + + + + + + + + + +
MTP Home + +Metamath Test Page + + + + < Wrap   + Wrap > + +
Nearby theorems + +
+ Mirrors  > +  Home  > +  MTP Home  > +  Th. List  > +  b + + + + + +
+
+
Syntax Definition b 1
+
Description: This is italic and +the command "MM-PA> MINIMIZE_WITH *".
+ +
+ + + +
Assertion
Ref +Expression
b +a
+ + +
+ + + +
  + +Copyright terms: +Public domain + + + +W3C validator +
+ diff --git a/tests/underscores.in b/tests/underscores.in new file mode 100644 index 00000000..b2859b84 --- /dev/null +++ b/tests/underscores.in @@ -0,0 +1,2 @@ +show statement b/alt_html +"cat b.html" \ No newline at end of file diff --git a/tests/underscores.mm b/tests/underscores.mm new file mode 100644 index 00000000..1731b5e1 --- /dev/null +++ b/tests/underscores.mm @@ -0,0 +1,9 @@ + $c a $. + + $( This is _italic_ and the command "MM-PA> MINIMIZE__WITH *". $) + b $a a $. + +$( $t + htmldef "a" as "a"; + althtmldef "a" as "a"; + latexdef "a" as "a"; $) From 8f3bd1012f9fed3af1bf91a66870b19bee45ddec Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sat, 2 Sep 2023 14:27:52 +0200 Subject: [PATCH 06/10] add subscript to the underscores test --- tests/underscores.expected | 7 ++++--- tests/underscores.mm | 3 ++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/tests/underscores.expected b/tests/underscores.expected index 40f682ff..f842f9a9 100644 --- a/tests/underscores.expected +++ b/tests/underscores.expected @@ -1,6 +1,6 @@ MM> READ "underscores.mm" -Reading source file "underscores.mm"... 171 bytes -171 bytes were read into the source buffer. +Reading source file "underscores.mm"... 193 bytes +193 bytes were read into the source buffer. The source has 2 statements; 1 are $a and 0 are $p. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. No errors were found. However, proofs were not checked. Type VERIFY PROOF * @@ -76,7 +76,8 @@ Metamath Test Page COLOR="#006633">b 1
Description: This is italic and -the command "MM-PA> MINIMIZE_WITH *".
+the command "MM-PA> MINIMIZE_WITH *" and a + subscript.
diff --git a/tests/underscores.mm b/tests/underscores.mm index 1731b5e1..aad42f1e 100644 --- a/tests/underscores.mm +++ b/tests/underscores.mm @@ -1,6 +1,7 @@ $c a $. - $( This is _italic_ and the command "MM-PA> MINIMIZE__WITH *". $) + $( This is _italic_ and the command "MM-PA> MINIMIZE__WITH *" and a + sub_script. $) b $a a $. $( $t From 77bc06f29d585976f4e266f4c6a03825645a6369 Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sat, 2 Sep 2023 15:13:47 +0200 Subject: [PATCH 07/10] simplify logic of conditions in mmwtex.c --- src/mmwtex.c | 93 ++++++++++++++++++++++++++-------------------------- 1 file changed, 47 insertions(+), 46 deletions(-) diff --git a/src/mmwtex.c b/src/mmwtex.c index 9baef211..eea7496d 100644 --- a/src/mmwtex.c +++ b/src/mmwtex.c @@ -16,21 +16,24 @@ #include "mmwtex.h" #include "mmcmdl.h" // For g_texFileName -// All LaTeX and HTML definitions are taken from the source -// file (read in the by READ... command). In the source file, there should -// be a single comment $( ... $) containing the keyword $t. The definitions -// start after the $t and end at the $). Between $t and $), the definition -// source should exist. See the file set.mm for an example. +// All LaTeX and HTML definitions are taken from the source file (read in by +// the READ command). In the source file, there should be a single comment +// $( ... $) containing the keyword $t. The definitions start after the $t and +// end at the $). Between $t and $), the definition source should exist. See +// the file set.mm for an example. flag g_oldTexFlag = 0; // Use TeX macros in output (obsolete) flag g_htmlFlag = 0; // HTML flag: 0 = TeX, 1 = HTML + // Use "althtmldef" instead of "htmldef". This is intended to allow the // generation of pages with the Unicode font instead of the individual GIF files. flag g_altHtmlFlag = 0; + // Output statement lists only, for statement display in other HTML pages, // such as the Proof Explorer home page. -flag g_briefHtmlFlag = 0; +flag g_briefHtmlFlag = 0; // TODO: unused + // 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 @@ -45,12 +48,12 @@ long g_extHtmlStmt = 0; // 0 means it hasn't been looked up yet; g_statements + 1 means there is // no mathbox. long g_mathboxStmt = 0; -long g_mathboxes = 0; // # of mathboxes +long g_mathboxes = 0; // number of mathboxes // The following 3 strings are 0-based e.g. g_mathboxStart[0] is for -// mathbox #1. -nmbrString_def(g_mathboxStart); // Start stmt vs. mathbox # -nmbrString_def(g_mathboxEnd); // End stmt vs. mathbox # -pntrString_def(g_mathboxUser); // User name vs. mathbox # +// mathbox number 1. +nmbrString_def(g_mathboxStart); // Start stmt vs. mathbox number +nmbrString_def(g_mathboxEnd); // End stmt vs. mathbox number +pntrString_def(g_mathboxUser); // User name vs. mathbox number // This is the list of characters causing the space before the opening "`" // in a math string in a comment to be removed for HTML output. @@ -188,7 +191,7 @@ flag readTexDefs( eraseTexDefs(); saveHtmlFlag = g_htmlFlag; // Save for next call to readTexDefs() saveAltHtmlFlag = g_altHtmlFlag; // Save for next call to readTexDefs() - if (g_htmlFlag == 0 /* Tex */ && g_altHtmlFlag == 1) { + if (!g_htmlFlag /* Tex */ && g_altHtmlFlag) { bug(2301); // Nonsensical combination } } else { @@ -1065,8 +1068,9 @@ vstring tokenToTex(vstring mtoken, long statemNum /* for error msgs */) for (i = 0; i < j; i++) { if (ispunct((unsigned char)(tex[i]))) { tmpStr = asciiToTt(chr(tex[i])); - if (!g_htmlFlag) + if (!g_htmlFlag) { // LaTeX let(&tmpStr, cat("{\\tt ", tmpStr, "}", NULL)); + } k = (long)strlen(tmpStr); let(&tex, cat(left(tex, i), tmpStr, right(tex, i + 2), NULL)); @@ -1077,9 +1081,10 @@ vstring tokenToTex(vstring mtoken, long statemNum /* for error msgs */) } // Next i // Make all letters Roman in math mode - if (!g_htmlFlag) + if (!g_htmlFlag) { // LaTeX let(&tex, cat("\\mathrm{", tex, "}", NULL)); - } // End if + } + } // End if (texDefsPtr) return tex; } // tokenToTex @@ -1113,7 +1118,7 @@ vstring asciiMathToTex(vstring mathComment, long statemNum) // tokenToTex allocates tex; we must deallocate it tex = tokenToTex(token, statemNum); - if (!g_htmlFlag) { + if (!g_htmlFlag) { // LaTeX // If this token and previous token begin with letter, add a thin // space between them. // Also, anything not in table will have space added. @@ -1221,13 +1226,14 @@ vstring getCommentModeSection(vstring *srcptr, char *mode) } ptr++; } // End while + assert(0); return NULL; // Dummy return - never executes } // getCommentModeSection // The texHeaderFlag means this: -// If !g_htmlFlag (i.e. TeX mode), then 1 means print header -// If g_htmlFlag, then 1 means include "Previous Next" links on page, -// based on the global g_showStatement variable. +// if !g_htmlFlag (i.e., TeX mode), then 1 means print header; +// if g_htmlFlag (i.e., HTML mode), then 1 means include "Previous Next" links +// on page, based on the global g_showStatement variable. void printTexHeader(flag texHeaderFlag) { @@ -1253,7 +1259,7 @@ void printTexHeader(flag texHeaderFlag) // } g_outputToString = 1; // Redirect print2 and printLongLine to g_printString - if (!g_htmlFlag) { + if (!g_htmlFlag) { // LaTeX print2("%s This LaTeX file was created by Metamath on %s %s.\n", "%", date(), time_()); @@ -1326,7 +1332,7 @@ void printTexHeader(flag texHeaderFlag) print2(" \\box\\mlinebox\n"); print2("}\n"); } - } else { // g_htmlFlag + } else { // g_htmlFlag // HTML print2("\n"); @@ -1745,7 +1751,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // Convert line to the old $m..$n and $l..$n formats (using DOLLAR_SUBST // instead of "$") - the old syntax is obsolete but we do this conversion // to re-use some old code. - if (metamathComment != 0) { + if (metamathComment) { i = instr(1, cmtptr, "$)"); // If it points to source buffer if (!i) i = (long)strlen(cmtptr) + 1; // If it's a stand-alone string } else { @@ -1758,12 +1764,12 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, let(&cmtMasked, cmt); // This section is independent and can be removed without side effects - if (g_htmlFlag) { + if (g_htmlFlag) { // HTML // Convert special characters <, &, etc. to HTML entities. // But skip converting math symbols inside ` `. // Detect preformatted HTML (this is crude, since it // will apply to whole comment - perhaps fine-tune this later). - if (convertToHtml != 0) { + if (convertToHtml) { if (instr(1, cmt, "") != 0) preformattedMode = 1; } else { preformattedMode = 1; // For MARKUP command - don't convert HTML @@ -1810,11 +1816,9 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, let(&cmtMasked, tmpMasked); free_vstring(tmpStr); // Deallocate free_vstring(tmpStrMasked); - } - // Add leading and trailing HTML markup to comment here - // (instead of in caller). Also convert special characters. - if (g_htmlFlag) { + // Add leading and trailing HTML markup to comment here + // (instead of in caller). Also convert special characters. // This used to be done in mmcmds.c if (htmlCenterFlag) { // Note: this should be 0 in MARKUP command let(&cmt, cat("
Description: ", @@ -1823,12 +1827,9 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, cat("
Description: ", cmtMasked, "
", NULL)); } - } - // Mask out _ (underscore) in labels so they won't become subscripts - // (reported by Benoit Jubin). - // This section is independent and can be removed without side effects. - if (g_htmlFlag != 0) { + // Mask out _ (underscore) in labels so they won't become subscripts. + // This section is independent and can be removed without side effects. pos1 = 0; while (1) { // Look for label start pos1 = instr(pos1 + 1, cmtMasked, "~"); @@ -1888,7 +1889,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // below, so that "{\em...}" won't be converted to "\}\em...\}". // Convert any remaining special characters for LaTeX. // This section is independent and can be removed without side effects. - if (!g_htmlFlag) { // i.e. LaTeX mode. + if (!g_htmlFlag) { // LaTeX // At this point, the comment begins e.g "\begin{lemma}\label{lem:abc}". pos1 = instr(1, cmt, "} "); if (pos1) { @@ -1938,7 +1939,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // to abc for book titles, etc.; convert a_n to an for // subscripts. // This section is independent and can be removed without side effects - if (g_htmlFlag != 0 && processUnderscores != 0) { + if (g_htmlFlag && processUnderscores) { pos1 = 0; while (1) { // Only look at non-math part of comment @@ -1967,13 +1968,13 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // underscores", so replace a double-underscore with a single // underscore and do not modify italic or subscript. if (cmt[pos1] == '_') { - if (g_htmlFlag) { // HTML + if (g_htmlFlag) { // HTML; TODO: extraneous since in a "if (g_htmlFlag && processUnderscores)" let(&cmt, cat(left(cmt, pos1), // Skip (delete) "_" right(cmt, pos1 + 2), NULL)); let(&cmtMasked, cat(left(cmtMasked, pos1), // Skip (delete) "_" right(cmtMasked, pos1 + 2), NULL)); pos1 ++; // Adjust for 1 extra char '_' - } else { // LaTeX + } else { // LaTeX; TODO: unreachable since in a "if (g_htmlFlag && processUnderscores)" let(&cmt, cat(left(cmt, pos1 - 1), // Skip (delete) "_" "\\texttt{\\_}", right(cmt, pos1 + 2), NULL)); @@ -2010,7 +2011,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, pos2++; // Move forward through subscript } pos2++; // Adjust for left, seg, etc. that start at 1 not 0 - if (g_htmlFlag) { // HTML + if (g_htmlFlag) { // HTML; TODO: extraneous since in a "if (g_htmlFlag && processUnderscores)" // Put ... around subscript let(&cmt, cat(left(cmt, pos1 - 1), "", @@ -2021,7 +2022,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, seg(cmtMasked, pos1 + 1, pos2 - 1), // Skip (delete) "_" "", right(cmtMasked, pos2), NULL)); pos1 = pos2 + 33; // Adjust for 34-1 extra chars in "let" above - } else { // LaTeX + } else { // LaTeX; TODO: unreachable since in a "if (g_htmlFlag && processUnderscores)" // Put _{...} around subscript let(&cmt, cat(left(cmt, pos1 - 1), "$_{", seg(cmt, pos1 + 1, pos2 - 1), // Skip (delete) "_" @@ -2046,7 +2047,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // Closing "_" must be _ if (!isalnum((unsigned char)(cmt[pos2 - 2]))) continue; if (isalnum((unsigned char)(cmt[pos2]))) continue; - if (g_htmlFlag) { // HTML + if (g_htmlFlag) { // HTML; TODO: extraneous since in a "if (g_htmlFlag && processUnderscores)" let(&cmt, cat(left(cmt, pos1 - 1), "", seg(cmt, pos1 + 1, pos2 - 1), "", right(cmt, pos2 + 1), NULL)); @@ -2054,7 +2055,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, seg(cmtMasked, pos1 + 1, pos2 - 1), "", right(cmtMasked, pos2 + 1), NULL)); pos1 = pos2 + 5; // Adjust for 7-2 extra chars in "let" above - } else { // LaTeX + } else { // LaTeX; TODO: unreachable since in a "if (g_htmlFlag && processUnderscores)" let(&cmt, cat(left(cmt, pos1 - 1), "{\\em ", seg(cmt, pos1 + 1, pos2 - 1), "}", right(cmt, pos2 + 1), NULL)); @@ -2064,11 +2065,11 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, pos1 = pos2 + 4; // Adjust for 6-2 extra chars in "let" above } } - } + } // End if (g_htmlFlag && processUnderscores) // Convert opening double quote to `` for LaTeX. // This section is independent and can be removed without side effects - if (!g_htmlFlag) { // If LaTeX mode + if (!g_htmlFlag) { // LaTeX i = 1; // Even/odd counter: 1 = left quote, 0 = right quote pos1 = 0; while (1) { @@ -2091,7 +2092,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // Put bibliography hyperlinks in comments converted to HTML: // [Monk2] becomes \n"); @@ -1751,7 +1745,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // Convert line to the old $m..$n and $l..$n formats (using DOLLAR_SUBST // instead of "$") - the old syntax is obsolete but we do this conversion // to re-use some old code. - if (metamathComment) { + if (metamathComment != 0) { i = instr(1, cmtptr, "$)"); // If it points to source buffer if (!i) i = (long)strlen(cmtptr) + 1; // If it's a stand-alone string } else { @@ -1764,12 +1758,12 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, let(&cmtMasked, cmt); // This section is independent and can be removed without side effects - if (g_htmlFlag) { // HTML + if (g_htmlFlag) { // Convert special characters <, &, etc. to HTML entities. // But skip converting math symbols inside ` `. // Detect preformatted HTML (this is crude, since it // will apply to whole comment - perhaps fine-tune this later). - if (convertToHtml) { + if (convertToHtml != 0) { if (instr(1, cmt, "") != 0) preformattedMode = 1; } else { preformattedMode = 1; // For MARKUP command - don't convert HTML @@ -1816,9 +1810,11 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, let(&cmtMasked, tmpMasked); free_vstring(tmpStr); // Deallocate free_vstring(tmpStrMasked); + } - // Add leading and trailing HTML markup to comment here - // (instead of in caller). Also convert special characters. + // Add leading and trailing HTML markup to comment here + // (instead of in caller). Also convert special characters. + if (g_htmlFlag) { // This used to be done in mmcmds.c if (htmlCenterFlag) { // Note: this should be 0 in MARKUP command let(&cmt, cat("
@@ -61,7 +61,7 @@ Metamath Test Page  Home  >  MTP Home  >  Th. List  > -  b +  underscores
Description: ", @@ -1827,9 +1823,12 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, cat("
Description: ", cmtMasked, "
", NULL)); } + } - // Mask out _ (underscore) in labels so they won't become subscripts. - // This section is independent and can be removed without side effects. + // Mask out _ (underscore) in labels so they won't become subscripts + // (reported by Benoit Jubin). + // This section is independent and can be removed without side effects. + if (g_htmlFlag != 0) { pos1 = 0; while (1) { // Look for label start pos1 = instr(pos1 + 1, cmtMasked, "~"); @@ -1889,7 +1888,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // below, so that "{\em...}" won't be converted to "\}\em...\}". // Convert any remaining special characters for LaTeX. // This section is independent and can be removed without side effects. - if (!g_htmlFlag) { // LaTeX + if (!g_htmlFlag) { // i.e. LaTeX mode. // At this point, the comment begins e.g "\begin{lemma}\label{lem:abc}". pos1 = instr(1, cmt, "} "); if (pos1) { @@ -1939,7 +1938,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // to abc for book titles, etc.; convert a_n to an for // subscripts. // This section is independent and can be removed without side effects - if (g_htmlFlag && processUnderscores) { + if (g_htmlFlag != 0 && processUnderscores != 0) { pos1 = 0; while (1) { // Only look at non-math part of comment @@ -1968,13 +1967,13 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // underscores", so replace a double-underscore with a single // underscore and do not modify italic or subscript. if (cmt[pos1] == '_') { - if (g_htmlFlag) { // HTML; TODO: extraneous since in a "if (g_htmlFlag && processUnderscores)" + if (g_htmlFlag) { // HTML let(&cmt, cat(left(cmt, pos1), // Skip (delete) "_" right(cmt, pos1 + 2), NULL)); let(&cmtMasked, cat(left(cmtMasked, pos1), // Skip (delete) "_" right(cmtMasked, pos1 + 2), NULL)); pos1 ++; // Adjust for 1 extra char '_' - } else { // LaTeX; TODO: unreachable since in a "if (g_htmlFlag && processUnderscores)" + } else { // LaTeX let(&cmt, cat(left(cmt, pos1 - 1), // Skip (delete) "_" "\\texttt{\\_}", right(cmt, pos1 + 2), NULL)); @@ -2011,7 +2010,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, pos2++; // Move forward through subscript } pos2++; // Adjust for left, seg, etc. that start at 1 not 0 - if (g_htmlFlag) { // HTML; TODO: extraneous since in a "if (g_htmlFlag && processUnderscores)" + if (g_htmlFlag) { // HTML // Put ... around subscript let(&cmt, cat(left(cmt, pos1 - 1), "", @@ -2022,7 +2021,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, seg(cmtMasked, pos1 + 1, pos2 - 1), // Skip (delete) "_" "", right(cmtMasked, pos2), NULL)); pos1 = pos2 + 33; // Adjust for 34-1 extra chars in "let" above - } else { // LaTeX; TODO: unreachable since in a "if (g_htmlFlag && processUnderscores)" + } else { // LaTeX // Put _{...} around subscript let(&cmt, cat(left(cmt, pos1 - 1), "$_{", seg(cmt, pos1 + 1, pos2 - 1), // Skip (delete) "_" @@ -2047,7 +2046,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // Closing "_" must be _ if (!isalnum((unsigned char)(cmt[pos2 - 2]))) continue; if (isalnum((unsigned char)(cmt[pos2]))) continue; - if (g_htmlFlag) { // HTML; TODO: extraneous since in a "if (g_htmlFlag && processUnderscores)" + if (g_htmlFlag) { // HTML let(&cmt, cat(left(cmt, pos1 - 1), "", seg(cmt, pos1 + 1, pos2 - 1), "", right(cmt, pos2 + 1), NULL)); @@ -2055,7 +2054,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, seg(cmtMasked, pos1 + 1, pos2 - 1), "", right(cmtMasked, pos2 + 1), NULL)); pos1 = pos2 + 5; // Adjust for 7-2 extra chars in "let" above - } else { // LaTeX; TODO: unreachable since in a "if (g_htmlFlag && processUnderscores)" + } else { // LaTeX let(&cmt, cat(left(cmt, pos1 - 1), "{\\em ", seg(cmt, pos1 + 1, pos2 - 1), "}", right(cmt, pos2 + 1), NULL)); @@ -2065,11 +2064,11 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, pos1 = pos2 + 4; // Adjust for 6-2 extra chars in "let" above } } - } // End if (g_htmlFlag && processUnderscores) + } // Convert opening double quote to `` for LaTeX. // This section is independent and can be removed without side effects - if (!g_htmlFlag) { // LaTeX + if (!g_htmlFlag) { // If LaTeX mode i = 1; // Even/odd counter: 1 = left quote, 0 = right quote pos1 = 0; while (1) { @@ -2092,7 +2091,7 @@ flag printTexComment(vstring commentPtr, flag htmlCenterFlag, // Put bibliography hyperlinks in comments converted to HTML: // [Monk2] becomes MINIMIZE__WITH *" and a sub_script. $) - b $a a $. + underscores $a a $. $( $t htmldef "a" as "a"; From b68713b5fdbd549dea4d167959ddafb135de13da Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sat, 9 Sep 2023 15:20:31 +0200 Subject: [PATCH 10/10] promote underscores test results --- tests/underscores.expected | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/tests/underscores.expected b/tests/underscores.expected index f842f9a9..2a74827c 100644 --- a/tests/underscores.expected +++ b/tests/underscores.expected @@ -1,12 +1,12 @@ MM> READ "underscores.mm" -Reading source file "underscores.mm"... 193 bytes -193 bytes were read into the source buffer. +Reading source file "underscores.mm"... 203 bytes +203 bytes were read into the source buffer. The source has 2 statements; 1 are $a and 0 are $p. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. No errors were found. However, proofs were not checked. Type VERIFY PROOF * if you want to check them. MM> Continuous scrolling is now in effect. -MM> Creating HTML file "b.html"... +MM> Creating HTML file "underscores.html"... Reading definitions from $t statement of underscores.mm... 1 typesetting statements were read from "underscores.mm". MM> -b - Metamath Test Page +underscores - Metamath Test Page @@ -46,11 +46,11 @@ Metamath Test Page 		- + < Wrap   - Wrap > + Wrap > -
Nearby theorems +
Nearby theorems
@@ -73,7 +73,7 @@ Metamath Test Page
Syntax Definition b underscores 1
-
Description: This is italic and the command "MM-PA> MINIMIZE_WITH *" and a @@ -84,7 +84,7 @@ SUMMARY="Assertion">
Assertion
Ref Expression
b +
underscores a