# HG changeset patch
# User oheimb
# Date 878740927 -3600
# Node ID d158fdc5a075e139c6c1b140b9a6de88b5b53da3
# Parent  c71e101c5bd847bffa7f3a9fa6f6218d47fb3c9f
added ax2isa

diff -r c71e101c5bd8 -r d158fdc5a075 src/Tools/8bit/Makefile
--- 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        
 
 # ----------------------------------------------------
diff -r c71e101c5bd8 -r d158fdc5a075 src/Tools/8bit/c-sources/a2isa/Makefile
--- 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
 
 # ----------------------------------------------------
 
diff -r c71e101c5bd8 -r d158fdc5a075 src/Tools/8bit/c-sources/a2isa/a2isa
Binary file src/Tools/8bit/c-sources/a2isa/a2isa has changed
diff -r c71e101c5bd8 -r d158fdc5a075 src/Tools/8bit/c-sources/a2isa/ax2isa
Binary file src/Tools/8bit/c-sources/a2isa/ax2isa has changed
diff -r c71e101c5bd8 -r d158fdc5a075 src/Tools/8bit/c-sources/a2isa/lex.x
--- 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}"
   */
 }
 %%
diff -r c71e101c5bd8 -r d158fdc5a075 src/Tools/8bit/c-sources/a2isa/xlex.x
--- /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}"
+  */
+}
+%%