--- 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;