--- 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
# ----------------------------------------------------
Binary file src/Tools/8bit/c-sources/a2isa/a2isa has changed
Binary file src/Tools/8bit/c-sources/a2isa/ax2isa has changed
--- 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}"
+ */
+}
+%%