# HG changeset patch
# User wenzelm
# Date 879348086 -3600
# Node ID 6ae637493076628866c472bc97c33147576083fc
# Parent  abce78c8a9313cc7aa19adeeae15234468dfe2e3
moved 'latex' from library.ML to goals.ML;

diff -r abce78c8a931 -r 6ae637493076 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed Nov 12 16:21:15 1997 +0100
+++ b/src/Pure/goals.ML	Wed Nov 12 16:21:26 1997 +0100
@@ -447,6 +447,12 @@
 
 fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
 
+(* FIXME !? *)
+(* output to LaTeX / xdvi *)
+fun latex s =
+  execute ("( cd /tmp ; echo \"" ^ s ^
+    "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &");
+
 (* Redirect output of function f:unit->unit to LaTeX *)
 fun redirect_to_latex f =
 	let