src/mathed/texify

   1 #!/usr/bin/tclsh
   2
   3 # Script built on an idea of Jules Bean to extract "what TeX would do" from
   4 # a given macro.
   5 #
   6 # Call it with  texify '\macro' [...] to get a line per item giving ascent,
   7 # descent, width, the font and the position in the font TeX would use to
   8 # typeset the symbol.
   9
  10 # Original script:
  11 #\batchmode
  12 #\def\entails{$1}
  13 #\edef\temp{\entails}
  14 #\message{\string\meaning\temp}
  15 #\setbox5=\box{$\entails$}
  16 #\showbox5
  17 #\bye
  18
  19 set filebase texifytmp
  20 set hboxexp {^\\hbox.([0-9.]+)\+([0-9.]+).x([0-9.]+)}
  21 set fontexp {^\.+\\ten([a-z]+) (.*)$}
  22
  23 foreach item $::argv {
  24         set font    unknown
  25         set char    {}
  26         set value   0
  27         set ascent  0
  28         set descent 0
  29         set widht   0
  30
  31         set f [open $filebase.tex w 0600]
  32         puts $f "\\nonstopmode"
  33         puts $f "\\setbox5=\\hbox\{\$$item\$\}"
  34         puts $f "\\showbox5"
  35         puts $f ""
  36         puts $f "\\end"
  37         close $f
  38
  39         if {[catch {exec tex $filebase.tex} err]} {
  40                 #puts "Error: '$err'"
  41         }
  42
  43         set f [open $filebase.log r]
  44         while {![eof $f]} {
  45                 gets $f line
  46                 # try to interpret it as a hbox line
  47                 regexp $hboxexp $line dummy ascent descent width
  48                 # try to interpret it as a font line
  49                 regexp $fontexp $line dummy font char
  50         }
  51         close $f
  52
  53         if {![string equal $font "unknown"]} {
  54                 if {[string equal -length 2 $char {^^}]} {
  55                         scan $char "%c%c%c" dummy1 dummy2 value
  56                         set value [expr {$value - 64}]
  57                 } else {
  58                         scan $char "%c" value
  59                 }
  60         }
  61
  62         puts [list $ascent $descent $width $font $value $char]
  63 }