/* Title: Tools/8bit/c-sources/isa2latex/conv-main.c
ID: $Id$
Author: Franz Regensburger
Copyright 1996 TU Muenchen
converter for isabelle files
definitions for the lexical analyzer
*/
%{
#include "conv-defs.h"
#define output(c) fputc(c, yyout)
#define BEGIN_ISA { if (accept_ASCII) \
BEGIN ISAA; /* we have -A option */ \
else \
BEGIN ISA;}
extern FILE *finput, *foutput;
extern int tabBlanks;
extern int tabcount;
extern char isa_env_beg0[], isa_env_beg1[], isa_env_end[];
extern int convMode;
extern int accept_ASCII;
extern int destCode;
extern int cc;
void reset_tabs(void);
void put(char c, int longDetect, int longCode);
int lineno=1;
int inline_mode=FALSE;
%}
%S LATEX ISA ISAA ESC
%option noyywrap
%%
void warning(char *what);
void not_suitable(char *what, char *where);
yyin = finput;
yyout = foutput;
if (convMode == MIXED)
BEGIN LATEX; /* we have -x option */
else
BEGIN_ISA;
<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++; }
<ISA,ISAA>\\I@ { if (inline_mode)
{ BEGIN LATEX; inline_mode=FALSE;
fprintf(foutput, "}}"); }
else
{ ECHO; not_suitable("\\I@","ISA"); }
}
<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) {
BEGIN LATEX; fprintf(foutput, isa_env_end); }
else {
ECHO; warning(
"\\I@isa only allowed with -x option"); }
}
}
<ISA,ISAA>\\E@ { BEGIN ESC; fprintf(foutput, "{\\isaescape{"); }
<ISA,ISAA><<EOF>> { if (convMode == MIXED)
not_suitable("EOF", inline_mode? "INLINE": "ISA");
yyterminate();
}
<ISA,ISAA>\n { if (inline_mode)
{ ECHO; not_suitable("\\n","INLINE"); }
else
{ put(*yytext,FALSE,0); }
lineno++;
}
<ISA,ISAA>\t { if (inline_mode)
{ ECHO; not_suitable("\\t","INLINE"); }
else
{ put(*yytext,FALSE,0); }
}
<ESC>\\I@ { ECHO; not_suitable("\\I@" ,"ESC"); }
<ESC>\\I@isa { ECHO; not_suitable("\\I@isa","ESC"); }
<ESC>\\E@ { BEGIN_ISA; fprintf(foutput, "}}"); }
<ESC><<EOF>> { not_suitable("EOF" ,"ESC"); yyterminate(); }
<ESC>\n { put(*yytext,FALSE,0); lineno++; }
/* The following is generated by the perl script gen-isa2latex. */
/* Make modifications in configuration file for gen-isa2latex! */
/* BEGIN_OF_HI_TABLE */
<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>\+\+ put((char)243,FALSE,0);
<ISAA>\\ominus put((char)244,FALSE,0);
<ISAA>\*\* 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>^and put((char)32,TRUE,11);
<ISAA>^@and 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>^end put((char)32,TRUE,19);
<ISAA>^@end put((char)32,TRUE,19);
<ISA,ISAA>^inductive put((char)32,TRUE,20);
<ISAA>^@inductive put((char)32,TRUE,20);
<ISA,ISAA>^instance put((char)32,TRUE,21);
<ISAA>^@instance put((char)32,TRUE,21);
<ISA,ISAA>^primrec put((char)32,TRUE,22);
<ISAA>^@primrec put((char)32,TRUE,22);
<ISA,ISAA>^recdef put((char)32,TRUE,23);
<ISAA>^@recdef put((char)32,TRUE,23);
<ISA,ISAA>^rules put((char)32,TRUE,24);
<ISAA>^@rules put((char)32,TRUE,24);
<ISA,ISAA>^syntax put((char)32,TRUE,25);
<ISAA>^@syntax put((char)32,TRUE,25);
<ISA,ISAA>^translations put((char)32,TRUE,26);
<ISAA>^@translations put((char)32,TRUE,26);
<ISA,ISAA>^typedef put((char)32,TRUE,27);
<ISAA>^@typedef put((char)32,TRUE,27);
<ISA,ISAA>^types put((char)32,TRUE,28);
<ISAA>^@types put((char)32,TRUE,28);
/* END_OF_SEQ_TABLE */
/* This is the end of the generated part */
. { put(*yytext,FALSE,0);}
%%
void warning(char *str)
{
fprintf(stderr,"WARNING: line %d: %s\n", lineno, str);
}
void not_suitable(char *what, char *where)
{
char buf[80];
sprintf(buf, "'%s' inside %s mode", what, where);
warning(buf);
}
void reset_tabs(void)
{
cc = 0;
tabcount = 1;
}
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 */
fputc(c,foutput);
else /* we are in ISA mode */
if (longDetect) { /* lexer has scanned a long sequence */
fprintf(foutput, "%s", translateLong(longCode, destCode));
if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
tabcount++;
}
else /* lexer has not scanned a long sequence */
if (c & 0x80) { /* Hi-bit is set... */
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++;
}
else /* simple char without Hi-Bit*/
if (destCode == TO_7bit)
fputc(c, foutput);
else
switch (c) { /* handle control codes */
case '\n': if (inline_mode)
c=' ';
else {
fprintf(foutput, "\\\\\n");
reset_tabs();
break;
}
case TAB: if (inline_mode)
c=' ';
else {
for (i = 0; i < tabcount; i++)
fprintf(foutput, "\\>");
reset_tabs();
break;
}
default:
if (++cc % tabBlanks == 0)
tabcount++;
if ((c >= START_LOW_TABLE) && (c <= END_LOW_TABLE))
{
fprintf(foutput, "%s", translateLow(c));}
else /* just reproduce the other control codes */
fputc(c, foutput);
} /* switch */
}