--- a/src/Tools/8bit/c-sources/isa2latex/conv-lex.x Fri Jun 29 18:12:18 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,350 +0,0 @@
-/* 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 */
-}
-
-
-
-
-
-