| author | oheimb |
| Wed, 05 Nov 1997 15:42:07 +0100 | |
| changeset 4168 | d158fdc5a075 |
| parent 4167 | c71e101c5bd8 |
| child 4169 | c63f261fb025 |
--- a/src/Tools/8bit/Makefile Wed Nov 05 15:38:40 1997 +0100 +++ b/src/Tools/8bit/Makefile Wed Nov 05 15:42:07 1997 +0100 @@ -108,7 +108,7 @@ all: $(CONFIGFILES)\ bin/gen-isa2latex bin/gen-isaterm bin/gen-isavim bin/gen-isaaxe\ bin/gen-isa_gnu_emacs bin/gen-isa_xemacs bin/gen-isadoc\ - configuration a2isa bin/isa2latex bin/a2isa\ + configuration a2isa bin/isa2latex bin/a2isa bin/ax2isa\ bin/isa_gnu_emacs bin/isa_xemacs bin/isavim bin/isaaxe\ bin/isaterm bin/isa_xmosaic bin/isapal bin/codetable bin/patcher\ fonts/install keyboard/install\ @@ -121,7 +121,7 @@ # ---------------------------------------------------- clean: - cd bin; rm -f a2isa codetable gen-* isa* patcher + cd bin; rm -f *2isa codetable gen-* isa* patcher cd c-sources/a2isa; $(GMAKE) clean cd c-sources/isa2latex; $(GMAKE) clean cd doc; $(GMAKE) clean @@ -250,6 +250,11 @@ @rm -f bin/a2isa;\ ln -s ../c-sources/a2isa/a2isa bin/a2isa +bin/ax2isa: c-sources/a2isa/ax2isa + @echo "installing ax2isa" + @rm -f bin/ax2isa;\ + ln -s ../c-sources/a2isa/ax2isa bin/ax2isa + ####### Editors # ----------------------------------------------------
--- a/src/Tools/8bit/c-sources/a2isa/Makefile Wed Nov 05 15:38:40 1997 +0100 +++ b/src/Tools/8bit/c-sources/a2isa/Makefile Wed Nov 05 15:42:07 1997 +0100 @@ -7,20 +7,28 @@ # Makefile for Isabelle ASCII to 8bit converter ################################################ -OBJECTS = main.o lex.o +AOBJECTS = main.o lex.o +AXOBJECTS = main.o xlex.o CC = gcc -# Application name -APPNAME = a2isa +.SUFFIXES: $(SUFFIXES) .x + +.x.o: + flex $<; $(CC) -c -o $@ lex.yy.c # ---------------------------------------------------- -$(APPNAME): $(OBJECTS) - $(CC) -o $(APPNAME) $(OBJECTS); strip $(APPNAME) +all: a2isa ax2isa + +a2isa: $(AOBJECTS) + $(CC) -o a2isa $(AOBJECTS); strip a2isa -lex.o: lex.x - flex lex.x; $(CC) -c -o lex.o lex.yy.c +ax2isa: $(AXOBJECTS) + $(CC) -o ax2isa $(AXOBJECTS); strip ax2isa + +#lex.o: lex.x +# flex lex.x; $(CC) -c -o lex.o lex.yy.c # ----------------------------------------------------
--- a/src/Tools/8bit/c-sources/a2isa/lex.x Wed Nov 05 15:38:40 1997 +0100 +++ b/src/Tools/8bit/c-sources/a2isa/lex.x Wed Nov 05 15:42:07 1997 +0100 @@ -45,36 +45,42 @@ <STRING>{ /* Pure */ -=> put("ë"); - !! put("Ä"); \[\| put("Ë"); \|\] put("Ì"); ==> put("êë"); == put("Ú"); +=> put("ë"); +:: put("å"); +'a put("ª"); +'b put("«"); +'c put("¬"); +'r put("¸"); +'s put("¹"); +'t put("º"); /* HOL */ -@ put("®"); +\ \*\ put(" ò "); +@[ A-Za-z] { *yytext='®'; put(yytext); } \ &\ put(" À "); \ \|\ put(" Á "); ~\ put("¿ "); --> put("çè"); ~= put("Û"); -\%[ A-Za-z_] { *yytext='³'; put(yytext); } +\%[ A-Za-z] { *yytext='³'; put(yytext); } EX! put("Ã!"); \?! put("Ã!"); EX\ put("Ã"); \?\ put("Ã"); ALL\ put("Â"); -![ A-Za-z_] { *yytext='Â'; put(yytext); } +![ A-Za-z] { *yytext='Â'; put(yytext); } /* Set */ -:: put("::"); ~: put("ñ"); : put("Î"); /* > "{}" "\mbox{$\emptyset$}" - > "<=" "\mbox{$\subseteq$}" +# > "<=" "\mbox{$\subseteq$}" */ \ Int\ put("Ð"); \ Un\ put("Ñ"); @@ -89,18 +95,17 @@ \*\* put("õ"); \+\+ put("ó"); +\<\<\| put("<<|"); +\<\| put("<|"); \<\< put("Ý"); - /* - > "<\|" "\mbox{$<\!\mid$}" - > "<<\|" "\mbox{$\ll\!\mid$}" - */ LAM\ put("¤"); lub\ put("×"); UU put("Ø"); -\(\| put("É"); -\|\) put("Ê"); /* misc */ +\|-put("É"); +\|= put("Ê"); + /* > "\Gamma\ " "\mbox{$\Gamma$}" > "\Delta\ " "\mbox{$\Delta$}" @@ -128,12 +133,11 @@ > "\lceil\ " "\mbox{$\lceil$}" > "\rceil\ " "\mbox{$\rceil$}" - > "\lfloor\ " "\mbox{$\lfloor$}" - > "\rfloor\ " "\mbox{$\rfloor$}" - > "\emptyset\ " "\mbox{$\emptyset$}" + > "\lfloor\ " "\mbox{$\lfloor$}" + > "\rfloor\ " "\mbox{$\rfloor$}" > "\sqcap\ " "\mbox{$\sqcap$}" - > "\sqcup\ " "\mbox{$\sqcup$}" - */ + > "\sqcup\ " "\mbox{$\sqcup$}" + > "\cdot\ " "\mbox{$\cdot$}" glb\ put("Ö"); === put("Ù"); @@ -143,7 +147,7 @@ > "\prec\ " "\mbox{$\prec$}" > "\preceq\ " "\mbox{$\preceq$}" > "\Succ\ " "\mbox{$\succ$}" - > "\Succeq\ " "\mbox{$\succeq$}" + > "\approx\ " "\mbox{$\approx$}" > "\sim\ " "\mbox{$\sim$}" > "\simeq\ " "\mbox{$\simeq$}" > "\le\ " "\mbox{$\le$}" @@ -157,22 +161,23 @@ \<- put("æ"); /* - > "\mapsto\ " "\mbox{$\mapsto$}" + > "\frown\ " "\mbox{$\frown$}" + > "\mapsto\ " "\mbox{$\mapsto$}" > "\leadsto\ " "\mbox{$\leadsto$}" > "\uparrow\ " "\mbox{$\uparrow$}" > "\downarrow\ " "\mbox{$\downarrow$}" - > "\ominus\ " "\mbox{$\varominus$}" - > "\oslash\ " "\mbox{$\varoslash$}" - > "\natural\ " "\mbox{$\natural$}" + > "\ominus\ " "\mbox{$\varominus$}" + > "\oslash\ " "\mbox{$\varoslash$}" + > "\subset\ " "\mbox{$\subset$}" > "\infty\ " "\mbox{$\infty$}" > "\Box\ " "\mbox{$\Box$}" > "\Diamond\ " "\mbox{$\Diamond$}" > "\circ\ " "\mbox{$\circ$}" - > "\bullet\ " "\mbox{$\bullet$}" + > "\bullet\ " "\mbox{$\bullet$}" > "||" "\mbox{$\parallel$}" > "\tick\ " "\mbox{$\surd$}" - > "\filter\ " "\mbox{\copyright}" + > "\filter\ " "\mbox{\copyright}" */ } %%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/8bit/c-sources/a2isa/xlex.x Wed Nov 05 15:42:07 1997 +0100 @@ -0,0 +1,183 @@ +/* Title: Tools/8bit/c-sources/a2isa/xlex.x + ID: $Id$ + Author: David von Oheimb + Copyright 1996 TU Muenchen + +Isabelle ASCII to 8bit converter +definitions for the lexical analyzer + +WARNING: the translations should be consistent with the configuration in + 8bit/config/conv-tables.inp +*/ + + +%{ +extern FILE *finput, *foutput; + +void put(char *s) +{ + while(*s) + { + fputc(*s++, yyout); + } +} +%} + +%option 8bit +%option yylineno +%option noyywrap +%x STRING + +%% + yyin = finput; + yyout = foutput; + +\\I@ { ECHO; BEGIN(STRING); } +. { ECHO; } +<STRING>\\I@ { ECHO; BEGIN(INITIAL); } +<STRING>\\[ \t]*\n[ \t]*\\ { ECHO; } +<STRING>\n { ECHO; /* fprintf(stderr, + "WARNING: line %d ends inside string\n", + yylineno-1); */} +<STRING><<EOF>> { fprintf(stderr, + "WARNING: EOF inside string\n"); + yyterminate(); } + +<STRING>{ + /* Pure */ +!! put("Ä"); +\[\| put("Ë"); +\|\] put("Ì"); +==> put("êë"); +== put("Ú"); +=> put("ë"); +:: put("å"); +'a put("ª"); +'b put("«"); +'c put("¬"); +'r put("¸"); +'s put("¹"); +'t put("º"); + + /* HOL */ +\ \*\ put(" ò "); +@[ A-Za-z] { *yytext='®'; put(yytext); } +\ &\ put(" À "); +\ \|\ put(" Á "); +~\ put("¿ "); +--> put("çè"); +~= put("Û"); +\%[ A-Za-z] { *yytext='³'; put(yytext); } +EX! put("Ã!"); +\?! put("Ã!"); +EX\ put("Ã"); +\?\ put("Ã"); +ALL\ put("Â"); +![ A-Za-z] { *yytext='Â'; put(yytext); } + + /* Set */ +~: put("ñ"); +: put("Î"); + /* + > "{}" "\mbox{$\emptyset$}" +# > "<=" "\mbox{$\subseteq$}" + */ +\ Int\ put("Ð"); +\ Un\ put("Ñ"); +Inter\ put("Ò"); +Union\ put("Ó"); + + /* Nat */ +LEAST\ put("´"); + + /* HOLCF */ +-> put("è"); +\*\* put("õ"); +\+\+ put("ó"); + +\<\<\| put("<<|"); +\<\| put("<|"); +\<\< put("Ý"); +LAM\ put("¤"); +lub\ put("×"); +UU put("Ø"); + + /* misc */ +\|- put("É"); +\|= put("Ê"); + + /* + > "\Gamma\ " "\mbox{$\Gamma$}" + > "\Delta\ " "\mbox{$\Delta$}" + > "\Theta\ " "\mbox{$\Theta$}" + > "\Pi\ " "\mbox{$\Pi$}" + > "\Sigma\ " "\mbox{$\Sigma$}" + > "\Phi\ " "\mbox{$\Phi$}" + > "\Psi\ " "\mbox{$\Psi$}" + > "\Omega\ " "\mbox{$\Omega$}" + + > "\delta\ " "\mbox{$\delta$}" + > "\epsilon\ " "\mbox{$\varepsilon$}" + > "\zeta\ " "\mbox{$\zeta$}" + > "\eta\ " "\mbox{$\eta$}" + > "\theta\ " "\mbox{$\vartheta$}" + > "\kappa\ " "\mbox{$\kappa$}" + > "\mu\ " "\mbox{$\mu$}" + > "\nu\ " "\mbox{$\nu$}" + > "\xi\ " "\mbox{$\xi$}" + > "\pi\ " "\mbox{$\pi$}" + > "\phi\ " "\mbox{$\varphi$}" + > "\chi\ " "\mbox{$\chi$}" + > "\psi\ " "\mbox{$\psi$}" + > "\omega\ " "\mbox{$\omega$}" + + > "\lceil\ " "\mbox{$\lceil$}" + > "\rceil\ " "\mbox{$\rceil$}" + > "\lfloor\ " "\mbox{$\lfloor$}" + > "\rfloor\ " "\mbox{$\rfloor$}" + > "\sqcap\ " "\mbox{$\sqcap$}" + > "\sqcup\ " "\mbox{$\sqcup$}" + > "\cdot\ " "\mbox{$\cdot$}" + +glb\ put("Ö"); +=== put("Ù"); + + /* + > "\sqsubset\ " "\mbox{$\sqsubset$}" + > "\prec\ " "\mbox{$\prec$}" + > "\preceq\ " "\mbox{$\preceq$}" + > "\Succ\ " "\mbox{$\succ$}" + > "\approx\ " "\mbox{$\approx$}" + > "\sim\ " "\mbox{$\sim$}" + > "\simeq\ " "\mbox{$\simeq$}" + > "\le\ " "\mbox{$\le$}" + > "\ge\ " "\mbox{$\ge$}" + */ + +\<== put("éê"); +\<=> put("éë"); +\<-- put("æç"); +\<-> put("æè"); +\<- put("æ"); + + /* + > "\frown\ " "\mbox{$\frown$}" + > "\mapsto\ " "\mbox{$\mapsto$}" + > "\leadsto\ " "\mbox{$\leadsto$}" + > "\uparrow\ " "\mbox{$\uparrow$}" + > "\downarrow\ " "\mbox{$\downarrow$}" + + > "\ominus\ " "\mbox{$\varominus$}" + > "\oslash\ " "\mbox{$\varoslash$}" + > "\subset\ " "\mbox{$\subset$}" + > "\infty\ " "\mbox{$\infty$}" + > "\Box\ " "\mbox{$\Box$}" + > "\Diamond\ " "\mbox{$\Diamond$}" + > "\circ\ " "\mbox{$\circ$}" + > "\bullet\ " "\mbox{$\bullet$}" + > "||" "\mbox{$\parallel$}" + > "\tick\ " "\mbox{$\surd$}" + > "\filter\ " "\mbox{\copyright}" + */ +} +%%