/* 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_beg[], 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,
"{\\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>\\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 (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"); }
}
if (yytext[0] == '\n') lineno++;
}
<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>\\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);
/* 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);
/* 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;
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... */
fprintf(foutput, "%s", translateHi(c, destCode));
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 */
}