Added functions pr_latex and printgoal_latex which
display current proof state in xdvi window

--- a/src/Pure/goals.ML	Thu Mar 28 17:21:58 1996 +0100
+++ b/src/Pure/goals.ML	Thu Mar 28 17:27:54 1996 +0100
@@ -42,6 +42,8 @@
   val goalw_cterm	: thm list -> cterm -> thm list
   val pop_proof		: unit -> thm list
   val pr		: unit -> unit
+  val pr_latex		: unit -> unit
+  val printgoal_latex	: int -> unit
   val premises		: unit -> thm list
   val prin		: term -> unit
   val printyp		: typ -> unit
@@ -430,6 +432,24 @@
 
 fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
 
+(* 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!*)
 fun print_exn e = (print_sign_exn_unit (top_sg()) e;  raise e);

--- a/src/Pure/library.ML	Thu Mar 28 17:21:58 1996 +0100
+++ b/src/Pure/library.ML	Thu Mar 28 17:27:54 1996 +0100
@@ -708,6 +708,11 @@
 fun prs s = !prs_fn s;
 fun writeln s = prs (s ^ "\n");
 
+(* output to LaTeX / xdvi *)
+fun latex s = 
+	execute ( "( cd /tmp ; echo \"" ^ s ^
+	"\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
+
 (*print warning*)
 val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
 fun warning s = !warning_fn ("Warning: " ^ s);