Added functions pr_latex and printgoal_latex which
authorberghofe
Thu Mar 28 17:27:54 1996 +0100 (1996-03-28)
changeset 162860136fdd80c4
parent 1627 64ee96ebf32a
child 1629 b5e43a60443a
Added functions pr_latex and printgoal_latex which
display current proof state in xdvi window
src/Pure/goals.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/goals.ML	Thu Mar 28 17:21:58 1996 +0100
     1.2 +++ b/src/Pure/goals.ML	Thu Mar 28 17:27:54 1996 +0100
     1.3 @@ -42,6 +42,8 @@
     1.4    val goalw_cterm	: thm list -> cterm -> thm list
     1.5    val pop_proof		: unit -> thm list
     1.6    val pr		: unit -> unit
     1.7 +  val pr_latex		: unit -> unit
     1.8 +  val printgoal_latex	: int -> unit
     1.9    val premises		: unit -> thm list
    1.10    val prin		: term -> unit
    1.11    val printyp		: typ -> unit
    1.12 @@ -430,6 +432,24 @@
    1.13  
    1.14  fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
    1.15  
    1.16 +(* Redirect output of function f:unit->unit to LaTeX *)
    1.17 +fun redirect_to_latex f =
    1.18 +	let
    1.19 +		val s = ref ""
    1.20 +		val old_prs_fn = !prs_fn
    1.21 +	in
    1.22 +		(prs_fn := (fn a => s := !s ^ a);
    1.23 +		f ();
    1.24 +		latex (!s);
    1.25 +		prs_fn := old_prs_fn)
    1.26 +	end;
    1.27 +
    1.28 +(* Display current proof state in xdvi window *)
    1.29 +fun pr_latex () = redirect_to_latex pr;
    1.30 +
    1.31 +(* Display goal n of current proof state in xdvi window *)
    1.32 +fun printgoal_latex n = redirect_to_latex (fn () => prin(getgoal n));
    1.33 +
    1.34  (*Prints exceptions nicely at top level; 
    1.35    raises the exception in order to have a polymorphic type!*)
    1.36  fun print_exn e = (print_sign_exn_unit (top_sg()) e;  raise e);
     2.1 --- a/src/Pure/library.ML	Thu Mar 28 17:21:58 1996 +0100
     2.2 +++ b/src/Pure/library.ML	Thu Mar 28 17:27:54 1996 +0100
     2.3 @@ -708,6 +708,11 @@
     2.4  fun prs s = !prs_fn s;
     2.5  fun writeln s = prs (s ^ "\n");
     2.6  
     2.7 +(* output to LaTeX / xdvi *)
     2.8 +fun latex s = 
     2.9 +	execute ( "( cd /tmp ; echo \"" ^ s ^
    2.10 +	"\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
    2.11 +
    2.12  (*print warning*)
    2.13  val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
    2.14  fun warning s = !warning_fn ("Warning: " ^ s);