Translating HTML 4.0 Symbols

The program symbol.awk translates HTML 4.0 symbols to a representation that uses the Adobe font named Symbol, which is available on many systems including Linux, OS/2, and Windows. For example, the HTML symbol ∃ represents the existential quantifier, but it is not yet supported by most browsers. Following is the HTML source that uses the Symbol font to print the character $.

     <font face="symbol">&#036</font>
The awk program can be run under the awk interpreter available on most Unix systems. For other systems, including MS Windows, you can download Brian Kernighan's "one true awk". After finding a copy of the awk interpreter and downloading the program symbol.awk, you can translate a file named version1.htm to another file named version2.htm by typing
     awk -f symbol.awk version1.htm > version2.htm
The awk program uses the gsub (global substitution) function to translate the HTML 4.0 symbols listed in the table below to the HTML code that prints them with the Symbol font. All other characters in the input file are copied unchanged to the output file.

For example, the program translates the following HTML source

     &forall;x &exist;y(y=x&minus;1 &and; y&le;x).
to HTML code that displays the following result.
     "x $y(y=x-1  yx).
Note that &minus; displays a minus sign "-", which is normally longer than a hyphen "-".

The current version of symbol.awk does not recognize all the symbols defined in the complete list of HTML 4.0 character entities, nor does it generate all the characters in the Symbol font. The following table shows the HTML source for the characters currently supported, the translated HTML for all the characters in the Symbol font, and the result displayed by the browser you are now using.

HTML Source Translated HTML Result
  <font face=symbol>&#033;</font> !
&forall; <font face=symbol>&#034;</font> "
  <font face=symbol>&#035;</font> #
&exist; <font face=symbol>&#036;</font> $
  <font face=symbol>&#037;</font> %
  <font face=symbol>&#038;</font> &
&bepsi; <font face=symbol>&#039;</font> '
  <font face=symbol>&#040;</font> (
  <font face=symbol>&#041;</font> )
&lowast; <font face=symbol>&#042;</font> *
  <font face=symbol>&#043;</font> +
  <font face=symbol>&#044;</font> ,
&minus; <font face=symbol>&#045;</font> -
  <font face=symbol>&#046;</font> .
  <font face=symbol>&#047;</font> /
  <font face=symbol>&#048;</font> 0
  <font face=symbol>&#049;</font> 1
  <font face=symbol>&#050;</font> 2
  <font face=symbol>&#051;</font> 3
  <font face=symbol>&#052;</font> 4
  <font face=symbol>&#053;</font> 5
  <font face=symbol>&#054;</font> 6
  <font face=symbol>&#055;</font> 7
  <font face=symbol>&#056;</font> 8
  <font face=symbol>&#057;</font> 9
  <font face=symbol>&#058;</font> :
  <font face=symbol>&#059;</font> ;
  <font face=symbol>&#060;</font> <
  <font face=symbol>&#061;</font> =
  <font face=symbol>&#062;</font> >
  <font face=symbol>&#063;</font> ?
&cong; <font face=symbol>&#064;</font> @
&Alpha; <font face=symbol>&#065;</font> A
&Beta; <font face=symbol>&#066;</font> B
&Chi; <font face=symbol>&#067;</font> C
&Delta; <font face=symbol>&#068;</font> D
&Epsilon; <font face=symbol>&#069;</font> E
&Phi; <font face=symbol>&#070;</font> F
&Gamma; <font face=symbol>&#071;</font> G
&Eta; <font face=symbol>&#072;</font> H
&Iota; <font face=symbol>&#073;</font> I
&thetasym; <font face=symbol>&#074;</font> J
&Kappa; <font face=symbol>&#075;</font> K
&Lambda; <font face=symbol>&#076;</font> L
&Mu; <font face=symbol>&#077;</font> M
&Nu; <font face=symbol>&#078;</font> N
&Omicron; <font face=symbol>&#079;</font> O
&Pi; <font face=symbol>&#080;</font> P
&Theta; <font face=symbol>&#081;</font> Q
&Rho; <font face=symbol>&#082;</font> R
&Sigma; <font face=symbol>&#083;</font> S
&Tau; <font face=symbol>&#084;</font> T
&Upsilon; <font face=symbol>&#085;</font> U
&sigmaf; <font face=symbol>&#086;</font> V
&Omega; <font face=symbol>&#087;</font> W
&Xi; <font face=symbol>&#088;</font> X
&Psi; <font face=symbol>&#089;</font> Y
&Zeta; <font face=symbol>&#090;</font> Z
  <font face=symbol>&#091;</font> [
&there4; <font face=symbol>&#092;</font> \
  <font face=symbol>&#093;</font> ]
&perp; <font face=symbol>&#094;</font> ^
  <font face=symbol>&#095;</font> _
&oline; <font face=symbol>&#096;</font> `
&alpha; <font face=symbol>&#097;</font> a
&beta; <font face=symbol>&#098;</font> b
&chi; <font face=symbol>&#099;</font> c
&delta; <font face=symbol>&#100;</font> d
&epsilon; <font face=symbol>&#101;</font> e
&phi; <font face=symbol>&#102;</font> f
&gamma; <font face=symbol>&#103;</font> g
&eta; <font face=symbol>&#104;</font> h
&iota; <font face=symbol>&#105;</font> i
&phiv; <font face=symbol>&#106;</font> j
&kappa; <font face=symbol>&#107;</font> k
&lambda; <font face=symbol>&#108;</font> l
&mu; <font face=symbol>&#109;</font> m
&nu; <font face=symbol>&#110;</font> n
&omicron; <font face=symbol>&#111;</font> o
&pi; <font face=symbol>&#112;</font> p
&theta; <font face=symbol>&#113;</font> q
&rho; <font face=symbol>&#114;</font> r
&sigma; <font face=symbol>&#115;</font> s
&tau; <font face=symbol>&#116;</font> t
&upsilon; <font face=symbol>&#117;</font> u
&piv; <font face=symbol>&#118;</font> v
&omega; <font face=symbol>&#119;</font> w
&xi; <font face=symbol>&#120;</font> x
&psi; <font face=symbol>&#121;</font> y
&zeta; <font face=symbol>&#122;</font> z
  <font face=symbol>&#123;</font> {
  <font face=symbol>&#124;</font> |
  <font face=symbol>&#125;</font> }
  <font face=symbol>&#126;</font> ~
&upsih; <font face=symbol>&#161;</font> ¡
&prime; <font face=symbol>&#162;</font> ¢
&le; <font face=symbol>&#163;</font> £
&frasl; <font face=symbol>&#164;</font> ¤
&infin; <font face=symbol>&#165;</font> ¥
&fnof; <font face=symbol>&#166;</font> ¦
&clubs; <font face=symbol>&#167;</font> §
&diams; <font face=symbol>&#168;</font> ¨
&hearts; <font face=symbol>&#169;</font> ©
&spades; <font face=symbol>&#170;</font> ª
&harr; <font face=symbol>&#171;</font> «
&larr; <font face=symbol>&#172;</font> ¬
&uarr; <font face=symbol>&#173;</font> ­
&rarr; <font face=symbol>&#174;</font> ®
&darr; <font face=symbol>&#175;</font> ¯
&deg; <font face=symbol>&#176;</font> °
&plusmn; <font face=symbol>&#177;</font> ±
&Prime; <font face=symbol>&#178;</font> ²
&ge; <font face=symbol>&#179;</font> ³
&times; <font face=symbol>&#180;</font> ´
&prop; <font face=symbol>&#181;</font> µ
&part; <font face=symbol>&#182;</font>
&bull; <font face=symbol>&#183;</font> ·
&divide; <font face=symbol>&#184;</font> ¸
&ne; <font face=symbol>&#185;</font> ¹
&equiv; <font face=symbol>&#186;</font> º
&asymp; <font face=symbol>&#187;</font> »
&hellip; <font face=symbol>&#188;</font> ¼
  <font face=symbol>&#189;</font> ½
&mdash; <font face=symbol>&#190;</font> ¾
&crarr; <font face=symbol>&#191;</font> ¿
&alefsym; <font face=symbol>&#192;</font> À
&image; <font face=symbol>&#193;</font> Á
&real; <font face=symbol>&#194;</font> Â
&weirp; <font face=symbol>&#195;</font> Ã
&otimes; <font face=symbol>&#196;</font> Ä
&oplus; <font face=symbol>&#197;</font> Å
&empty; <font face=symbol>&#198;</font> Æ
&cap; <font face=symbol>&#199;</font> Ç
&cup; <font face=symbol>&#200;</font> È
&sup; <font face=symbol>&#201;</font> É
&supe; <font face=symbol>&#202;</font> Ê
&nsup; <font face=symbol>&#203;</font> Ë
&sub; <font face=symbol>&#204;</font> Ì
&sube; <font face=symbol>&#205;</font> Í
&isin; <font face=symbol>&#206;</font> Î
&notin; <font face=symbol>&#207;</font> Ï
&ang; <font face=symbol>&#208;</font> Ð
&nabla; <font face=symbol>&#209;</font> Ñ
&reg; <font face=symbol>&#210;</font> Ò
&copy; <font face=symbol>&#211;</font> Ó
&trade; <font face=symbol>&#212;</font> Ô
&prod; <font face=symbol>&#213;</font> Õ
&radic; <font face=symbol>&#214;</font> Ö
&middot; <font face=symbol>&#215;</font> ×
&not; <font face=symbol>&#216;</font> Ø
&and; <font face=symbol>&#217;</font> Ù
&or; <font face=symbol>&#218;</font> Ú
&hArr; <font face=symbol>&#219;</font> Û
&lArr; <font face=symbol>&#220;</font> Ü
&uArr; <font face=symbol>&#221;</font> Ý
&rArr; <font face=symbol>&#222;</font> Þ
&dArr; <font face=symbol>&#223;</font> ß
&loz; <font face=symbol>&#224;</font> à
<font face=symbol>&#225;</font> á
  <font face=symbol>&#226;</font> â
  <font face=symbol>&#227;</font> ã
  <font face=symbol>&#228;</font> ä
&sum; <font face=symbol>&#229;</font> å
&rang; <font face=symbol>&#241;</font> ñ

Certain HTML characters in the Symbol font are also available in the default ASCII fonts: &amp;, &lt;, &gt;, &times;, &divide;, &deg;, &not;, &reg;, and &copy;. Those symbols are left untranslated by the symbol.awk program. Other characters are available in the Wingdings font, but the character &box; is the only one recognized by the symbol.awk program.


Copyright ©1999 by John F. Sowa. Permission is hereby granted for anyone to copy and use this documentation and the symbol.awk program under the LGPL license.

  Last Modified: