Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-09-20 17:00:18 -0700 (Fri, 20 Sep 2002)
Revision: 3884
Log message:

      I am working on creating a proper locale mapping
      of MetaPRL font table ("mode[prl]") to Unicode.
      
      I fixed a few bugs with nuprl_font doing some mappings incorrectly.
      
      The rest is still work-in-progress.
      

Changes  Path
+29 -27 metaprl/doc/htmlman/chars/table.html
Added metaprl/editor/fonts/charset.txt
Properties metaprl/editor/fonts/charset.txt
Added metaprl/editor/fonts/extract_charset.pl
Properties metaprl/editor/fonts/extract_charset.pl
+22 -21 metaprl/theories/tactic/nuprl_font.ml