Change latex render units from px (pdflatex specific) to bp (tex).
The px unit is a pdflatex specific adjustable unit that is 1 bp (big point = 1/72in) by default. This commit changes the latex renderer to use bp which is a standard TeX unit equivalent to the default px value. This change allows .tex files generated by scribble to work with other latex engines such as xelatex. http://nwalsh.com/tex/texhelp/Plain.html#dimensions http://tex.stackexchange.com/questions/41370/what-are-the-possible-dimensions-sizes-units-latex-understands Here is a small test of using scribble and xelatex: $ cat try.scrbl @(require scriblib/figure redex/reduction-semantics redex/pict) @(define-language L) @(render-term L (term 1)) $ scribble --latex try.scrbl ; xelatex try original commit: 0dfcf634ed29a9d6e9d99ea7bcd02121abd24a7b
This commit is contained in:
parent
0836269713
commit
cd18c13bf9
|
@ -324,7 +324,7 @@
|
||||||
(- (ceiling height) height)))]
|
(- (ceiling height) height)))]
|
||||||
[fn (install-file (format "pict~a" suffix) bstr)])
|
[fn (install-file (format "pict~a" suffix) bstr)])
|
||||||
(if descent
|
(if descent
|
||||||
(printf "\\raisebox{-~apx}{\\makebox[~apx][l]{\\includegraphics{~a}}}"
|
(printf "\\raisebox{-~abp}{\\makebox[~abp][l]{\\includegraphics{~a}}}"
|
||||||
descent
|
descent
|
||||||
width
|
width
|
||||||
fn)
|
fn)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user