From a764632d29c79933e8c54633831e4aac0fb204f6 Mon Sep 17 00:00:00 2001
From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Mon, 7 Mar 2011 05:42:04 -0800
Subject: [PATCH] make latex output use the preview package to set the page
 size

---
 src/Extraction.v |   20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/Extraction.v b/src/Extraction.v
index 1a26e58..57e08a3 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -91,13 +91,16 @@ Section core2proof.
     "\usepackage{proof}"+++eol+++
     "\usepackage{mathpartir}"+++eol+++
     "\usepackage{trfrac}"+++eol+++
-    "\pdfpagewidth 50in"+++eol+++
-    "\pdfpageheight 10in"+++eol+++
     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
-    "\begin{document}"+++eol.
+    "\usepackage[paperwidth=20in,centering]{geometry}"+++eol+++
+    "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
+    "\begin{document}"+++eol+++
+    "\begin{preview}"+++eol.
 
   Definition footer : string :=
-    eol+++"\end{document}"+++eol.
+    eol+++"\end{preview}"+++
+    eol+++"\end{document}"+++
+    eol.
 
   Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
     match coreExprToWeakExpr ce with
@@ -107,7 +110,10 @@ Section core2proof.
           | Indexed_Error  s  => fail ("unable to convert HaskWeak to HaskStrong due to:\n  "+++s)
           | Indexed_OK    τ e => match e with
                                    | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n  "+++s)
-                                   | OK e'   => header +++ (nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')) +++ footer
+                                   | OK e'   =>
+                                     eol+++"$$"+++
+                                     nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++
+                                     "$$"+++eol
                                  end
         end
     end.
@@ -119,7 +125,9 @@ Section core2proof.
     end.
 
   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
-    fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "".
+    header +++
+    (fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "")
+    +++ footer.
 
   Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
     lbinds.
-- 
1.7.10.4