Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Structured Typesetting (STS) generation #9

Open
wants to merge 14 commits into
base: master
Choose a base branch
from
Open

Structured Typesetting (STS) generation #9

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
7742b5c
Structured Typesetting (STS) generation
tirix Dec 24, 2021
8af50bc
Merge branch 'master' into structured-typesetting
tirix Dec 24, 2021
eedc22f
Rename global variables (to adapt to change 0.187 15-Aug-2020)
tirix Dec 24, 2021
9202215
Delete makefile, formatting.
tirix Dec 25, 2021
991bd6c
Double-space after periods in help texts.
tirix Dec 25, 2021
1a66907
More help text formatting
tirix Dec 25, 2021
f3ae0fa
Typo: parsetSTSRules -> parseSTSRules
tirix Dec 26, 2021
2a870d8
Update comments in metamath.c
tirix Dec 26, 2021
ea0bde7
Merge branch 'structured-typesetting' of https://github.com/tirix/met…
digama0 Jan 4, 2022
59c02a3
Merge remote-tracking branch 'origin/master' into tirix-structured-ty…
digama0 Jan 4, 2022
6371dc7
Merge commit 'origin/master~' into tirix-structured-typesetting
digama0 Jan 8, 2022
dcbc83a
Merge remote-tracking branch 'origin/master' into tirix-structured-ty…
digama0 Jan 8, 2022
c5925cb
fix compile errors/warnings
digama0 Jan 8, 2022
e5f602f
tabs -> spaces
digama0 Jan 8, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
*.o
metamath
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@wlammen writes:

OK, see here (https://stackoverflow.com/questions/6626136/best-practice-for-adding-gitignore-to-repo)
Maybe one should put this info into the README?

I'm not sure which info you would like to add to the README.
There is a standard .gitignore file for C projects here, we could give it a try.
Maybe better in a separate PR?

Copy link
Contributor

@wlammen wlammen Dec 26, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The reason why I added this comment is, because the metamath sources are distributed via a tar archive as well. Obviously you wont need the gitignore in this case. I think, some kind of distribution how-to is finally called for. That are my thoughts. I was curious why you added the file. Separate PR is fine with me.

6 changes: 5 additions & 1 deletion Makefile.am
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,9 @@ noinst_HEADERS = \
mmveri.h \
mmvstr.h \
mmword.h \
mmwtex.h
mmwtex.h \
mmhtbl.h \
mmwsts.h

metamath_SOURCES = \
metamath.c \
Expand All @@ -30,6 +32,8 @@ metamath_SOURCES = \
mmvstr.c \
mmword.c \
mmwtex.c \
mmhtbl.c \
mmwsts.c \
$(noinst_HEADERS)


Expand Down
12,900 changes: 6,476 additions & 6,424 deletions metamath.c
View file
Open in desktop

Large diffs are not rendered by default.

33 changes: 29 additions & 4 deletions mmcmdl.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ flag processCommandLine(void)
"OPEN|CLOSE|SHOW|SEARCH|SET|VERIFY|SUBMIT|SYSTEM|PROVE|FILE|WRITE|",
"MARKUP|ASSIGN|REPLACE|MATCH|UNIFY|LET|INITIALIZE|DELETE|IMPROVE|",
"MINIMIZE_WITH|EXPAND|UNDO|REDO|SAVE|DEMO|INVOKE|CLI|EXPLORE|TEX|",
"LATEX|HTML|COMMENTS|BIBLIOGRAPHY|MORE|",
"LATEX|HTML|STS|COMMENTS|BIBLIOGRAPHY|MORE|",
"TOOLS|MIDI|$|<$>", NULL))) goto pclbad;
if (cmdMatches("HELP OPEN")) {
if (!getFullArg(2, "LOG|TEX|<LOG>")) goto pclbad;
Expand Down Expand Up @@ -111,7 +111,7 @@ flag processCommandLine(void)
goto pclgood;
}
if (cmdMatches("HELP VERIFY")) {
if (!getFullArg(2, "PROOF|MARKUP|<PROOF>"))
if (!getFullArg(2, "PROOF|MARKUP|STS|<PROOF>"))
goto pclbad;
goto pclgood;
}
Expand Down Expand Up @@ -518,9 +518,19 @@ flag processCommandLine(void)
if (lastArgMatches("/")) {
i++;
if (!getFullArg(i, cat(
"FULL|COMMENT|TEX|OLD_TEX|HTML|ALT_HTML|TIME|BRIEF_HTML",
"FULL|COMMENT|TEX|OLD_TEX|HTML|ALT_HTML|STS|TIME|BRIEF_HTML",
"|BRIEF_ALT_HTML|MNEMONICS|NO_VERSIONING|<FULL>", NULL)))
goto pclbad;
if (lastArgMatches("STS")) {
i++;
if (strlen(stsOutput)) {
if (!getFullArg(i,cat("* Using which output mode <",stsOutput,">? ",NULL)))
Copy link
Contributor

@wlammen wlammen Dec 27, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Incorrect indentation

goto pclbad;
} else {
if (!getFullArg(i,"* Using which output mode <mathml>? "))
goto pclbad;
}
}
} else {
break;
}
Expand Down Expand Up @@ -1196,7 +1206,7 @@ flag processCommandLine(void)

if (cmdMatches("VERIFY")) {
if (!getFullArg(1,
"PROOF|MARKUP|<PROOF>"))
"PROOF|MARKUP|STS|<PROOF>"))
goto pclbad;
if (cmdMatches("VERIFY PROOF")) {
if (g_sourceHasBeenRead == 0) {
Expand Down Expand Up @@ -1255,6 +1265,21 @@ flag processCommandLine(void)

goto pclgood;
}

if (cmdMatches("VERIFY STS")) {
if (g_statements == 0) {
print2("?No source file has been read in. Use READ first.\n");
goto pclbad;
}
if (strlen(stsOutput)) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Duplicated code from line 586 (with i == 2)

if (!getFullArg(2,cat("* Using which output mode <",stsOutput,">? ",NULL)))
goto pclbad;
} else {
if (!getFullArg(2,"* Using which output mode <mathml>? "))
goto pclbad;
}
goto pclgood;
}
}

if (cmdMatches("DBG")) {
Expand Down
Loading