--- a/src/Tools/8bit/c-sources/isa2latex/conv-lex.x Wed Nov 05 15:42:30 1997 +0100
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-lex.x Wed Nov 05 15:45:51 1997 +0100
@@ -18,7 +18,7 @@
extern FILE *finput, *foutput;
extern int tabBlanks;
extern int tabcount;
-extern char isa_env_beg[], isa_env_end[];
+extern char isa_env_beg0[], isa_env_beg1[], isa_env_end[];
extern int convMode;
extern int accept_ASCII;
extern int destCode;
@@ -44,11 +44,14 @@
else
BEGIN_ISA;
-<LATEX>\\I@ { BEGIN_ISA; inline_mode=TRUE ; fprintf(foutput,
- "{\\isainline{"); }
-<LATEX>\\I@isa[ \t]*\n? { BEGIN_ISA; inline_mode=FALSE; fprintf(foutput,
- isa_env_beg); reset_tabs();
- if (yytext[strlen(yytext)-1] == '\n') lineno++;
+<LATEX>\\I@@? { BEGIN_ISA; inline_mode=TRUE ; fprintf(foutput,
+ (yytext[3]=='@' ? "\\mbox{\\isainline[\\isamodify]{"
+ : "\\mbox{\\isainline{")); }
+<LATEX>\\I@isa@?[ \t]*\n? { BEGIN_ISA; inline_mode=FALSE; fprintf(foutput,
+ (yytext[6]=='@' ? isa_env_beg1
+ : isa_env_beg0)); reset_tabs();
+ if (yytext[strlen(yytext)-1] == '\n')
+ { fprintf(foutput, "\n"); lineno++; }
}
<LATEX>\\E@ { ECHO; not_suitable("\\E@","LATEX"); }
<LATEX>\n { put(*yytext,FALSE,0); lineno++; }
@@ -59,7 +62,9 @@
else
{ ECHO; not_suitable("\\I@","ISA"); }
}
-<ISA,ISAA>\n?[ \t]*\\I@isa { if (inline_mode)
+<ISA,ISAA>\n?[ \t]*\\I@isa {if (yytext[0] == '\n')
+ { fprintf(foutput, "\n"); lineno++; };
+ if (inline_mode)
{ ECHO; not_suitable("\\I@isa","INLINE"); }
else
{ if (convMode == MIXED) {
@@ -68,7 +73,6 @@
ECHO; warning(
"\\I@isa only allowed with -x option"); }
}
- if (yytext[0] == '\n') lineno++;
}
<ISA,ISAA>\\E@ { BEGIN ESC; fprintf(foutput, "{\\isaescape{"); }
<ISA,ISAA><<EOF>> { if (convMode == MIXED)
@@ -96,129 +100,162 @@
/* The following is generated by the perl script gen-isa2latex. */
/* Make modifications in configuration file for gen-isa2latex! */
/* BEGIN_OF_HI_TABLE */
-<ISAA>\\Gamma\ put((char)161,FALSE,0);
-<ISAA>\\Delta\ put((char)162,FALSE,0);
-<ISAA>\\Theta\ put((char)163,FALSE,0);
-<ISAA>LAM\ put((char)164,FALSE,0);
-<ISAA>\\Pi\ put((char)165,FALSE,0);
-<ISAA>\\Sigma\ put((char)166,FALSE,0);
-<ISAA>\\Phi\ put((char)167,FALSE,0);
-<ISAA>\\Psi\ put((char)168,FALSE,0);
-<ISAA>\\Omega\ put((char)169,FALSE,0);
-<ISAA>'a put((char)170,FALSE,0);
-<ISAA>'b put((char)171,FALSE,0);
-<ISAA>'c put((char)172,FALSE,0);
-<ISAA>\\delta\ put((char)173,FALSE,0);
-<ISAA>\\varepsilon\ put((char)174,FALSE,0);
-<ISAA>\\zeta\ put((char)175,FALSE,0);
-<ISAA>\\eta\ put((char)176,FALSE,0);
-<ISAA>\\vartheta\ put((char)177,FALSE,0);
-<ISAA>\\kappa\ put((char)178,FALSE,0);
-<ISAA>%\ put((char)179,FALSE,0);
-<ISAA>\\mu\ put((char)180,FALSE,0);
-<ISAA>\\nu\ put((char)181,FALSE,0);
-<ISAA>\\xi\ put((char)182,FALSE,0);
-<ISAA>\\pi\ put((char)183,FALSE,0);
-<ISAA>'r put((char)184,FALSE,0);
-<ISAA>'s put((char)185,FALSE,0);
-<ISAA>'t put((char)186,FALSE,0);
-<ISAA>\\varphi\ put((char)187,FALSE,0);
-<ISAA>\\chi\ put((char)188,FALSE,0);
-<ISAA>\\psi\ put((char)189,FALSE,0);
-<ISAA>\\omega\ put((char)190,FALSE,0);
-<ISAA>~\ put((char)191,FALSE,0);
-<ISAA>&\ put((char)192,FALSE,0);
-<ISAA>\|\ put((char)193,FALSE,0);
-<ISAA>!\ put((char)194,FALSE,0);
-<ISAA>\?\ put((char)195,FALSE,0);
-<ISAA>!! put((char)196,FALSE,0);
-<ISAA>\\lceil\ put((char)197,FALSE,0);
-<ISAA>\\rceil\ put((char)198,FALSE,0);
-<ISAA>\\lfloor\ put((char)199,FALSE,0);
-<ISAA>\\rfloor\ put((char)200,FALSE,0);
-<ISAA>\(\| put((char)201,FALSE,0);
-<ISAA>\|\) put((char)202,FALSE,0);
-<ISAA>\[\| put((char)203,FALSE,0);
-<ISAA>\|\] put((char)204,FALSE,0);
-<ISAA>{} put((char)205,FALSE,0);
-<ISAA>\ :\ put((char)206,FALSE,0);
-<ISAA>\subseteq\ put((char)207,FALSE,0);
-<ISAA>\ Int\ put((char)208,FALSE,0);
-<ISAA>\ Un\ put((char)209,FALSE,0);
-<ISAA>Inter\ put((char)210,FALSE,0);
-<ISAA>Union\ put((char)211,FALSE,0);
-<ISAA>\sqcap\ put((char)212,FALSE,0);
-<ISAA>\sqcup\ put((char)213,FALSE,0);
-<ISAA>glb\ put((char)214,FALSE,0);
-<ISAA>lub\ put((char)215,FALSE,0);
-<ISAA>UU put((char)216,FALSE,0);
-<ISAA>=== put((char)217,FALSE,0);
-<ISAA>== put((char)218,FALSE,0);
-<ISAA>~= put((char)219,FALSE,0);
-<ISAA>\\sqsubset\ put((char)220,FALSE,0);
-<ISAA><< put((char)221,FALSE,0);
-<ISAA>\\prec\ put((char)222,FALSE,0);
-<ISAA>\\preceq\ put((char)223,FALSE,0);
-<ISAA>\\succ\ put((char)224,FALSE,0);
-<ISAA>\\succeq\ put((char)225,FALSE,0);
-<ISAA>\\sim\ put((char)226,FALSE,0);
-<ISAA>\\simeq\ put((char)227,FALSE,0);
-<ISAA>\\le\ put((char)228,FALSE,0);
-<ISAA>\\ge\ put((char)229,FALSE,0);
-<ISAA><- put((char)230,FALSE,0);
-<ISAA>-@@@@@ put((char)231,FALSE,0);
-<ISAA>-> put((char)232,FALSE,0);
-<ISAA>\\Leftarrow\ put((char)233,FALSE,0);
-<ISAA>=@@@@@ put((char)234,FALSE,0);
-<ISAA>=> put((char)235,FALSE,0);
-<ISAA>->> put((char)236,FALSE,0);
-<ISAA>\\mapsto\ put((char)237,FALSE,0);
-<ISAA>\\leadsto\ put((char)238,FALSE,0);
-<ISAA>\\uparrow\ put((char)239,FALSE,0);
-<ISAA>\\downarrow\ put((char)240,FALSE,0);
-<ISAA>~: put((char)241,FALSE,0);
-<ISAA>\\times\ put((char)242,FALSE,0);
-<ISAA>\\oplus\ put((char)243,FALSE,0);
-<ISAA>\\ominus\ put((char)244,FALSE,0);
-<ISAA>\\otimes\ put((char)245,FALSE,0);
-<ISAA>\\oslash\ put((char)246,FALSE,0);
-<ISAA>\\natural\ put((char)247,FALSE,0);
-<ISAA>\\infty\ put((char)248,FALSE,0);
-<ISAA>\\Box\ put((char)249,FALSE,0);
-<ISAA>\\Diamond\ put((char)250,FALSE,0);
-<ISAA>\\circ\ put((char)251,FALSE,0);
-<ISAA>\\bullet\ put((char)252,FALSE,0);
-<ISAA>\|\| put((char)253,FALSE,0);
-<ISAA>\\tick\ put((char)254,FALSE,0);
-<ISAA>\\filter\ put((char)255,FALSE,0);
+<ISAA>\ \ put((char)160,FALSE,0);
+<ISAA>\\Gamma put((char)161,FALSE,0);
+<ISAA>\\Delta put((char)162,FALSE,0);
+<ISAA>\\Theta put((char)163,FALSE,0);
+<ISAA>LAM\ put((char)164,FALSE,0);
+<ISAA>\\Pi put((char)165,FALSE,0);
+<ISAA>\\Sigma put((char)166,FALSE,0);
+<ISAA>\\Phi put((char)167,FALSE,0);
+<ISAA>\\Psi put((char)168,FALSE,0);
+<ISAA>\\Omega put((char)169,FALSE,0);
+<ISAA>'a put((char)170,FALSE,0);
+<ISAA>'b put((char)171,FALSE,0);
+<ISAA>'c put((char)172,FALSE,0);
+<ISAA>\\delta put((char)173,FALSE,0);
+<ISAA>\\varepsilon put((char)174,FALSE,0);
+<ISAA>\\zeta put((char)175,FALSE,0);
+<ISAA>\\eta put((char)176,FALSE,0);
+<ISAA>\\vartheta put((char)177,FALSE,0);
+<ISAA>\\kappa put((char)178,FALSE,0);
+<ISAA>%\ put((char)179,FALSE,0);
+<ISAA>\\mu put((char)180,FALSE,0);
+<ISAA>\\nu put((char)181,FALSE,0);
+<ISAA>\\xi put((char)182,FALSE,0);
+<ISAA>\\pi put((char)183,FALSE,0);
+<ISAA>'r put((char)184,FALSE,0);
+<ISAA>'s put((char)185,FALSE,0);
+<ISAA>'t put((char)186,FALSE,0);
+<ISAA>\\varphi put((char)187,FALSE,0);
+<ISAA>\\chi put((char)188,FALSE,0);
+<ISAA>\\psi put((char)189,FALSE,0);
+<ISAA>\\omega put((char)190,FALSE,0);
+<ISAA>~\ put((char)191,FALSE,0);
+<ISAA>&\ put((char)192,FALSE,0);
+<ISAA>\|\ put((char)193,FALSE,0);
+<ISAA>!\ put((char)194,FALSE,0);
+<ISAA>\?\ put((char)195,FALSE,0);
+<ISAA>!! put((char)196,FALSE,0);
+<ISAA>\\lceil put((char)197,FALSE,0);
+<ISAA>\\rceil put((char)198,FALSE,0);
+<ISAA>\\lfloor put((char)199,FALSE,0);
+<ISAA>\\rfloor put((char)200,FALSE,0);
+<ISAA>\|- put((char)201,FALSE,0);
+<ISAA>\|= put((char)202,FALSE,0);
+<ISAA>\[\| put((char)203,FALSE,0);
+<ISAA>\|\] put((char)204,FALSE,0);
+<ISAA>\\cdot put((char)205,FALSE,0);
+<ISAA>\ :\ put((char)206,FALSE,0);
+<ISAA>\ \subseteq\ put((char)207,FALSE,0);
+<ISAA>\ Int\ put((char)208,FALSE,0);
+<ISAA>\ Un\ put((char)209,FALSE,0);
+<ISAA>Inter\ put((char)210,FALSE,0);
+<ISAA>Union\ put((char)211,FALSE,0);
+<ISAA>\\sqcap put((char)212,FALSE,0);
+<ISAA>\\sqcup put((char)213,FALSE,0);
+<ISAA>glb\ put((char)214,FALSE,0);
+<ISAA>LUB\ put((char)215,FALSE,0);
+<ISAA>UU put((char)216,FALSE,0);
+<ISAA>=== put((char)217,FALSE,0);
+<ISAA>== put((char)218,FALSE,0);
+<ISAA>~= put((char)219,FALSE,0);
+<ISAA>\\sqsubset put((char)220,FALSE,0);
+<ISAA><< put((char)221,FALSE,0);
+<ISAA><: put((char)222,FALSE,0);
+<ISAA><=: put((char)223,FALSE,0);
+<ISAA>:> put((char)224,FALSE,0);
+<ISAA>~~ put((char)225,FALSE,0);
+<ISAA>\\sim\ put((char)226,FALSE,0);
+<ISAA>\\simeq put((char)227,FALSE,0);
+<ISAA><= put((char)228,FALSE,0);
+<ISAA>:: put((char)229,FALSE,0);
+<ISAA><- put((char)230,FALSE,0);
+<ISAA>-@@@@@ put((char)231,FALSE,0);
+<ISAA>-> put((char)232,FALSE,0);
+<ISAA>\\Leftarrow put((char)233,FALSE,0);
+<ISAA>=@@@@@ put((char)234,FALSE,0);
+<ISAA>=> put((char)235,FALSE,0);
+<ISAA>\\frown put((char)236,FALSE,0);
+<ISAA>\\mapsto put((char)237,FALSE,0);
+<ISAA>\\leadsto put((char)238,FALSE,0);
+<ISAA>\\uparrow put((char)239,FALSE,0);
+<ISAA>\\downarrow put((char)240,FALSE,0);
+<ISAA>~: put((char)241,FALSE,0);
+<ISAA>\\times put((char)242,FALSE,0);
+<ISAA>\\oplus put((char)243,FALSE,0);
+<ISAA>\\ominus put((char)244,FALSE,0);
+<ISAA>\\otimes put((char)245,FALSE,0);
+<ISAA>\\oslash put((char)246,FALSE,0);
+<ISAA>\\subset put((char)247,FALSE,0);
+<ISAA>\\infty put((char)248,FALSE,0);
+<ISAA>\\Box put((char)249,FALSE,0);
+<ISAA>\\Diamond put((char)250,FALSE,0);
+<ISAA>\\circ put((char)251,FALSE,0);
+<ISAA>\\bullet put((char)252,FALSE,0);
+<ISAA>\|\| put((char)253,FALSE,0);
+<ISAA>\\tick put((char)254,FALSE,0);
+<ISAA>\\filter put((char)255,FALSE,0);
/* END_OF_HI_TABLE */
/* This is the end of the generated part */
/* The following is generated by the perl script gen-isa2latex. */
/* Make modifications in configuration file for gen-isa2latex! */
/* BEGIN_OF_SEQ_TABLE */
-<ISA,ISAA>êë put((char)32,TRUE,0);
-<ISAA>==> put((char)32,TRUE,0);
-<ISA,ISAA>çè put((char)32,TRUE,1);
-<ISAA>--> put((char)32,TRUE,1);
-<ISA,ISAA>Ã! put((char)32,TRUE,2);
-<ISAA>\?! put((char)32,TRUE,2);
-<ISA,ISAA>ALL@@@@@ put((char)32,TRUE,3);
-<ISAA>ALL\ put((char)32,TRUE,3);
-<ISA,ISAA>EX@@@@@ put((char)32,TRUE,4);
-<ISAA>EX\ put((char)32,TRUE,4);
-<ISA,ISAA><\|@@@@@ put((char)32,TRUE,5);
-<ISAA><\| put((char)32,TRUE,5);
-<ISA,ISAA><<\|@@@@@ put((char)32,TRUE,6);
-<ISAA><<\| put((char)32,TRUE,6);
-<ISA,ISAA>éê put((char)32,TRUE,7);
-<ISAA><== put((char)32,TRUE,7);
-<ISA,ISAA>éë put((char)32,TRUE,8);
-<ISAA><=> put((char)32,TRUE,8);
-<ISA,ISAA>æç put((char)32,TRUE,9);
-<ISAA><-- put((char)32,TRUE,9);
-<ISA,ISAA>æè put((char)32,TRUE,10);
-<ISAA><-> put((char)32,TRUE,10);
+<ISA,ISAA>êë put((char)32,TRUE,0);
+<ISAA>==> put((char)32,TRUE,0);
+<ISA,ISAA>çè put((char)32,TRUE,1);
+<ISAA>--> put((char)32,TRUE,1);
+<ISA,ISAA>Ã! put((char)32,TRUE,2);
+<ISAA>\?! put((char)32,TRUE,2);
+<ISA,ISAA>ALL@@@@@ put((char)32,TRUE,3);
+<ISAA>ALL\ put((char)32,TRUE,3);
+<ISA,ISAA>EX@@@@@ put((char)32,TRUE,4);
+<ISAA>EX\ put((char)32,TRUE,4);
+<ISA,ISAA><<\| put((char)32,TRUE,5);
+<ISAA><<\| put((char)32,TRUE,5);
+<ISA,ISAA><\| put((char)32,TRUE,6);
+<ISAA><\| put((char)32,TRUE,6);
+<ISA,ISAA>éê put((char)32,TRUE,7);
+<ISAA><== put((char)32,TRUE,7);
+<ISA,ISAA>éë put((char)32,TRUE,8);
+<ISAA><=> put((char)32,TRUE,8);
+<ISA,ISAA>æç put((char)32,TRUE,9);
+<ISAA><-- put((char)32,TRUE,9);
+<ISA,ISAA>æè put((char)32,TRUE,10);
+<ISAA><-> put((char)32,TRUE,10);
+<ISA,ISAA>\^-1 put((char)32,TRUE,11);
+<ISAA>\^-1 put((char)32,TRUE,11);
+<ISA,ISAA>arities put((char)32,TRUE,12);
+<ISAA>@arities put((char)32,TRUE,12);
+<ISA,ISAA>axclass put((char)32,TRUE,13);
+<ISAA>@axclass put((char)32,TRUE,13);
+<ISA,ISAA>constdefs put((char)32,TRUE,14);
+<ISAA>@constdefs put((char)32,TRUE,14);
+<ISA,ISAA>consts put((char)32,TRUE,15);
+<ISAA>@consts put((char)32,TRUE,15);
+<ISA,ISAA>datatype put((char)32,TRUE,16);
+<ISAA>@datatype put((char)32,TRUE,16);
+<ISA,ISAA>defs put((char)32,TRUE,17);
+<ISAA>@defs put((char)32,TRUE,17);
+<ISA,ISAA>domain put((char)32,TRUE,18);
+<ISAA>@domain put((char)32,TRUE,18);
+<ISA,ISAA>inductive put((char)32,TRUE,19);
+<ISAA>@inductive put((char)32,TRUE,19);
+<ISA,ISAA>instance put((char)32,TRUE,20);
+<ISAA>@instance put((char)32,TRUE,20);
+<ISA,ISAA>primrec put((char)32,TRUE,21);
+<ISAA>@primrec put((char)32,TRUE,21);
+<ISA,ISAA>recdef put((char)32,TRUE,22);
+<ISAA>@recdef put((char)32,TRUE,22);
+<ISA,ISAA>rules put((char)32,TRUE,23);
+<ISAA>@rules put((char)32,TRUE,23);
+<ISA,ISAA>translations put((char)32,TRUE,24);
+<ISAA>@translations put((char)32,TRUE,24);
+<ISA,ISAA>typedef put((char)32,TRUE,25);
+<ISAA>@typedef put((char)32,TRUE,25);
+<ISA,ISAA>types put((char)32,TRUE,26);
+<ISAA>@types put((char)32,TRUE,26);
/* END_OF_SEQ_TABLE */
/* This is the end of the generated part */
@@ -247,6 +284,8 @@
void put(char c, int longDetect,int longCode)
{
int i;
+ char s[100];
+ extern char *translateHi(int ch, int code);
if (YY_START == LATEX || YY_START == ESC)
/* do not translate in these modes */
@@ -260,7 +299,12 @@
}
else /* lexer has not scanned a long sequence */
if (c & 0x80) { /* Hi-bit is set... */
- fprintf(foutput, "%s", translateHi(c, destCode));
+ strcpy(s, translateHi(c, destCode));
+ i = strlen(s);
+ if((unsigned char)c != 0xa0 &&
+ i >= 2 && s[i-2] == '\\' && s[i-1] == ' ' && (yytext[0] & 0x80))
+ s[i-2] ='\0';
+ fprintf(foutput, "%s", s);
if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
tabcount++;
}
--- a/src/Tools/8bit/c-sources/isa2latex/conv-tables.h Wed Nov 05 15:42:30 1997 +0100
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-tables.h Wed Nov 05 15:45:51 1997 +0100
@@ -13,17 +13,17 @@
"\\ ",
"!",
"\x22{}",
- "\\#",
+ "\\mbox{$\\#$}",
"\\$",
"\\%",
- "\\mbox{$\\&$}",
+ "\\&",
"'",
- "(",
- ")",
- "\\mbox{$*$}",
- "\\mbox{$+$}",
+ "\\mbox{$($}",
+ "\\mbox{$)$}",
+ "{*}",
+ "+",
",",
- "\\mbox{$-$}",
+ "-",
".",
"/",
"0",
@@ -70,10 +70,10 @@
"Y",
"Z",
"\\mbox{$[$}",
- "\\mbox{$\\backslash$}",
+ "\\ttbackslash{}",
"\\mbox{$]$}",
"\\^{}",
- "\\_",
+ "{\\_\\hspace{.344ex}}",
"`",
"a",
"b",
@@ -101,10 +101,10 @@
"x",
"y",
"z",
- "\\{",
- "\\mbox{$|$}",
- "\\}",
- "\\~{}"
+ "\\mbox{$\\{$}",
+ "\\mbox{$\\mid$}",
+ "\\mbox{$\\}$}",
+ "\\tttilde{}"
};
/* END_OF_LOW_TABLE */
@@ -123,10 +123,11 @@
/* BEGIN_OF_HI_TABLE */
char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2] = {
+ {" " ,"\\ \\ "},
{"\\Gamma" ,"\\mbox{$\\Gamma$}"},
{"\\Delta" ,"\\mbox{$\\Delta$}"},
{"\\Theta" ,"\\mbox{$\\Theta$}"},
- {"LAM" ,"\\mbox{$\\Lambda$}"},
+ {"LAM " ,"\\mbox{$\\Lambda$}"},
{"\\Pi" ,"\\mbox{$\\Pi$}"},
{"\\Sigma" ,"\\mbox{$\\Sigma$}"},
{"\\Phi" ,"\\mbox{$\\Phi$}"},
@@ -136,7 +137,7 @@
{"'b" ,"\\mbox{$\\beta$}"},
{"'c" ,"\\mbox{$\\gamma$}"},
{"\\delta" ,"\\mbox{$\\delta$}"},
- {"\\varepsilon" ,"\\mbox{$\\varepsilon$}"},
+ {"@" ,"\\mbox{$\\varepsilon$}"},
{"\\zeta" ,"\\mbox{$\\zeta$}"},
{"\\eta" ,"\\mbox{$\\eta$}"},
{"\\vartheta" ,"\\mbox{$\\vartheta$}"},
@@ -145,7 +146,7 @@
{"\\mu" ,"\\mbox{$\\mu$}"},
{"\\nu" ,"\\mbox{$\\nu$}"},
{"\\xi" ,"\\mbox{$\\xi$}"},
- {"\\pi" ,"\\mbox{$\\pi$}"},
+ {"\\p" ,"\\mbox{$\\pi$}"},
{"'r" ,"\\mbox{$\\rho$}"},
{"'s" ,"\\mbox{$\\sigma$}"},
{"'t" ,"\\mbox{$\\tau$}"},
@@ -153,67 +154,67 @@
{"\\chi" ,"\\mbox{$\\chi$}"},
{"\\psi" ,"\\mbox{$\\psi$}"},
{"\\omega" ,"\\mbox{$\\omega$}"},
- {"~" ,"\\mbox{$\\neg$}"},
- {"&" ,"\\mbox{$\\wedge$}"},
- {"|" ,"\\mbox{$\\vee$}"},
- {"!" ,"\\mbox{$\\forall$}"},
- {"?" ,"\\mbox{$\\exists$}"},
+ {"~ " ,"\\mbox{$\\neg$}"},
+ {"& " ,"\\mbox{$\\hspace{-.185ex}\\wedge\\hspace{-.185ex}$}\\ "},
+ {"| " ,"\\mbox{$\\hspace{-.185ex}\\vee\\hspace{-.185ex}$}\\ "},
+ {"!" ,"\\mbox{$\\hspace{-.07ex}\\forall$}"},
+ {"? " ,"\\mbox{$\\hspace{-.07ex}\\exists$}"},
{"!!" ,"\\mbox{$\\bigwedge$}"},
{"\\lceil" ,"\\mbox{$\\lceil$}"},
{"\\rceil" ,"\\mbox{$\\rceil$}"},
{"\\lfloor" ,"\\mbox{$\\lfloor$}"},
{"\\rfloor" ,"\\mbox{$\\rfloor$}"},
- {"(|" ,"\\mbox{$(\\!|$}"},
- {"|)" ,"\\mbox{$|\\!)$}"},
- {"[|" ,"\\mbox{$[\\![$}"},
- {"|]" ,"\\mbox{$]\\!]$}"},
- {"\\emptyset" ,"\\mbox{$\\emptyset$}"},
- {":" ,"\\mbox{$\\in$}"},
- {"\\subseteq" ,"\\mbox{$\\subseteq$}"},
- {"Int" ,"\\mbox{$\\cap$}"},
- {"Un" ,"\\mbox{$\\cup$}"},
- {"Inter" ,"\\mbox{$\\bigcap$}"},
- {"Union" ,"\\mbox{$\\bigcup$}"},
- {"\\sqcap" ,"\\mbox{$\\sqcap$}"},
- {"\\sqcup" ,"\\mbox{$\\sqcup$}"},
- {"glb" ,"\\mbox{$\\overline{|\\,\\,|}$}"},
- {"lub" ,"\\mbox{$\\bigsqcup$}"},
- {"UU" ,"\\mbox{$\\perp$}"},
- {"===" ,"\\mbox{$\\doteq$}"},
- {"==" ,"\\mbox{$\\equiv$}"},
+ {"|-" ,"\\mbox{$\\hspace{.49ex}\\vdash\\hspace{.49ex}$}"},
+ {"|=" ,"\\mbox{$\\models$}"},
+ {"[|" ,"\\mbox{$[\\![\\hspace{.32ex}$}"},
+ {"|]" ,"\\mbox{$\\hspace{.32ex}]\\!]$}"},
+ {"\\cdot" ,"\\mbox{$\\hspace{.28ex}\\cdot\\hspace{.28ex}$}"},
+ {":" ,"\\hspace{.1ex}\\mbox{$\\in$}\\hspace{.1ex}"},
+ {" \\subseteq " ,"\\mbox{$\\subseteq$}"},
+ {" Int " ,"\\mbox{$\\cap$}"},
+ {" Un " ,"\\mbox{$\\cup$}"},
+ {"Inter " ,"\\mbox{$\\bigcap$}"},
+ {"Union " ,"\\mbox{$\\bigcup$}"},
+ {"\\sqcap" ,"\\mbox{$\\hspace{.29ex}\\sqcap\\hspace{.29ex}$}"},
+ {"\\sqcup" ,"\\mbox{$\\hspace{.29ex}\\sqcup\\hspace{.29ex}$}"},
+ {"glb " ,"\\mbox{$\\overline{|\\,\\,|}$}"},
+ {"LUB " ,"\\mbox{$\\bigsqcup$}"},
+ {"UU" ,"\\mbox{$\\bot$}"},
+ {".=" ,"\\mbox{$\\doteq$}"},
+ {"==" ,"\\mbox{$\\hspace{.29ex}\\equiv\\hspace{.29ex}$}"},
{"~=" ,"\\mbox{$\\not=$}"},
- {"\\sqsubset" ,"\\mbox{$\\sqsubset$}"},
- {"<<" ,"\\mbox{$\\sqsubseteq$}"},
- {"\\prec" ,"\\mbox{$\\prec$}"},
- {"\\preceq" ,"\\mbox{$\\preceq$}"},
- {"\\succ" ,"\\mbox{$\\succ$}"},
- {"\\succeq" ,"\\mbox{$\\succeq$}"},
- {"\\sim" ,"\\mbox{$\\sim$}"},
- {"\\simeq" ,"\\mbox{$\\simeq$}"},
- {"\\le" ,"\\mbox{$\\le$}"},
- {"\\ge" ,"\\mbox{$\\ge$}"},
+ {"\\sqsubset" ,"\\mbox{$\\hspace{.29ex}\\sqsubset\\hspace{.29ex}$}"},
+ {"<<" ,"\\mbox{$\\hspace{.29ex}\\sqsubseteq\\hspace{.29ex}$}"},
+ {"<:" ,"\\mbox{$\\hspace{.29ex}\\prec\\hspace{.29ex}$}\\ "},
+ {"<=:" ,"\\mbox{$\\hspace{.29ex}\\preceq\\hspace{.29ex}$}"},
+ {":>" ,"\\mbox{$\\hspace{.29ex}\\succ\\hspace{.29ex}$}\\ "},
+ {"~~" ,"\\mbox{$\\hspace{.29ex}\\approx\\hspace{.29ex}$}"},
+ {"\\sim " ,"\\mbox{$\\hspace{.29ex}\\sim\\hspace{.29ex}$}\\ "},
+ {"\\simeq" ,"\\mbox{$\\hspace{.29ex}\\simeq\\hspace{.29ex}$}"},
+ {"<=" ,"\\mbox{$\\hspace{.29ex}\\le\\hspace{.29ex}$}"},
+ {"::" ,"\\mbox{$\\hspace{-.1ex}:\\hspace{-.07ex}:\\hspace{.1ex}$}"},
{"<-" ,"\\mbox{$\\leftarrow$}"},
{"-" ,"\\mbox{$-$}"},
{"->" ,"\\mbox{$\\rightarrow$}"},
{"<=" ,"\\mbox{$\\Leftarrow$}"},
{"=" ,"\\mbox{$=$}"},
- {"=>" ,"\\mbox{$\\Rightarrow$}"},
- {"->>" ,"\\mbox{$\\twoheadrightarrow$}"},
- {"\\mapsto" ,"\\mbox{$\\mapsto$}"},
- {"\\leadsto" ,"\\mbox{$\\leadsto$}"},
+ {"=>" ,"\\mbox{$\\hspace{.12ex}\\Rightarrow$}"},
+ {"\\frown" ,"\\mbox{$\\frown$}"},
+ {"|->" ,"\\mbox{$\\mapsto$}"},
+ {"~>" ,"\\mbox{$\\hspace{.05ex}\\leadsto$}"},
{"\\uparrow" ,"\\mbox{$\\uparrow$}"},
{"\\downarrow" ,"\\mbox{$\\downarrow$}"},
{"~:" ,"\\mbox{$\\notin$}"},
- {"*" ,"\\mbox{$\\times$}"},
- {"++" ,"\\mbox{$\\oplus$}"},
- {"\\ominus" ,"\\mbox{$\\ominus$}"},
- {"**" ,"\\mbox{$\\otimes$}"},
- {"\\oslash" ,"\\mbox{$\\oslash$}"},
- {"\\natural" ,"\\mbox{$\\natural$}"},
+ {"*" ,"\\mbox{$\\hspace{-.29ex}\\times\\hspace{-.29ex}$}"},
+ {"++" ,"\\mbox{$\\hspace{.29ex}\\oplus\\hspace{.29ex}$}"},
+ {"--" ,"\\mbox{$\\hspace{.29ex}\\ominus\\hspace{.29ex}$}"},
+ {"**" ,"\\mbox{$\\hspace{.29ex}\\otimes\\hspace{.29ex}$}"},
+ {"//" ,"\\mbox{$\\hspace{.29ex}\\oslash\\hspace{.29ex}$}"},
+ {"\\subset" ,"\\mbox{$\\subset$}"},
{"\\infty" ,"\\mbox{$\\infty$}"},
{"\\Box" ,"\\mbox{$\\Box$}"},
- {"\\Diamond" ,"\\mbox{$\\Diamond$}"},
- {"\\circ" ,"\\mbox{$\\circ$}"},
+ {"<>" ,"\\mbox{$\\hspace{.29ex}\\Diamond\\hspace{.29ex}$}"},
+ {" o " ,"\\mbox{$\\circ$}"},
{"\\bullet" ,"\\mbox{$\\bullet$}"},
{"||" ,"\\mbox{$\\parallel$}"},
{"\\tick" ,"\\mbox{$\\surd$}"},
@@ -236,17 +237,33 @@
/* BEGIN_OF_SEQ_TABLE */
char *translationTableSeq[SEQ_TABLE][2] = {
- {"==>" ,"\\mbox{$\\Longrightarrow$}"},
- {"-->" ,"\\mbox{$\\longrightarrow$}"},
- {"?!" ,"\\mbox{$\\exists$}!"},
- {"ALL" ,"\\mbox{$\\forall$}"},
- {"EX" ,"\\mbox{$\\exists$}"},
- {"<|" ,"\\mbox{$<\\!\\mid$}"},
- {"<<|" ,"\\mbox{$\\ll\\!\\mid$}"},
- {"<==" ,"\\mbox{$\\Longleftarrow$}"},
- {"<=>" ,"\\mbox{$\\Leftrightarrow$}"},
- {"<--" ,"\\mbox{$\\longleftarrow$}"},
- {"<->" ,"\\mbox{$\\leftrightarrow$}"}
+ {"==>" ,"\\mbox{$\\hspace{-.083ex}\\Longrightarrow$}"},
+ {"-->" ,"\\mbox{$\\longrightarrow$}"},
+ {"?!" ,"\\mbox{$\\exists_1$}"},
+ {"ALL " ,"\\mbox{$\\forall$}"},
+ {"EX " ,"\\mbox{$\\exists$}"},
+ {"<<|" ,"\\mbox{$\\ll\\!\\mid$}"},
+ {"<|" ,"\\mbox{$<\\!\\mid$}"},
+ {"<==" ,"\\mbox{$\\Longleftarrow$}"},
+ {"<=>" ,"\\mbox{$\\Leftrightarrow$}"},
+ {"<--" ,"\\mbox{$\\longleftarrow$}"},
+ {"<->" ,"\\mbox{$\\leftrightarrow$}"},
+ {"^-1" ,"\\mbox{$^{\\tt -1}$}"},
+ {"arities" ,"\\mbox{\\bf arities}"},
+ {"axclass" ,"\\mbox{\\bf axclass}"},
+ {"constdefs" ,"\\mbox{\\bf constdefs}"},
+ {"consts" ,"\\mbox{\\bf consts}"},
+ {"datatype" ,"\\mbox{\\bf datatype}"},
+ {"defs" ,"\\mbox{\\bf defs}"},
+ {"domain" ,"\\mbox{\\bf domain}"},
+ {"inductive" ,"\\mbox{\\bf inductive}"},
+ {"instance" ,"\\mbox{\\bf instance}"},
+ {"primrec" ,"\\mbox{\\bf primrec}"},
+ {"recdef" ,"\\mbox{\\bf recdef}"},
+ {"rules" ,"\\mbox{\\bf rules}"},
+ {"translations" ,"\\mbox{\\bf translations}"},
+ {"typedef" ,"\\mbox{\\bf typedef}"},
+ {"types" ,"\\mbox{\\bf types}"}
};
/* END_OF_SEQ_TABLE */