# HG changeset patch
# User wenzelm
# Date 911998637 -3600
# Node ID 6727d29d164f20c1ea37e8d4e5c2653a6bceda81
# Parent  4ec8b8f957e64e9c228b7509ae4815dbe4c081d5
removed redirect_to_latex stuff;

diff -r 4ec8b8f957e6 -r 6727d29d164f src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Nov 24 12:03:56 1998 +0100
+++ b/src/Pure/goals.ML	Wed Nov 25 13:57:17 1998 +0100
@@ -49,8 +49,6 @@
   val pr		: unit -> unit
   val prlev		: int -> unit
   val prlim		: int -> unit
-  val pr_latex		: unit -> unit
-  val printgoal_latex	: int -> unit
   val premises		: unit -> thm list
   val prin		: term -> unit
   val printyp		: typ -> unit
@@ -507,29 +505,6 @@
 
 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
-		val s = ref ""
-		val old_prs_fn = !prs_fn
-	in
-		(prs_fn := (fn a => s := !s ^ a);
-		f ();
-		latex (!s);
-		prs_fn := old_prs_fn)
-	end;
-
-(* Display current proof state in xdvi window *)
-fun pr_latex () = redirect_to_latex pr;
-
-(* Display goal n of current proof state in xdvi window *)
-fun printgoal_latex n = redirect_to_latex (fn () => prin(getgoal n));
 
 (*Prints exceptions nicely at top level; 
   raises the exception in order to have a polymorphic type!*)
@@ -537,6 +512,4 @@
 
 end;
 
-
-
 open Goals;