src/Pure/library.ML
changeset 1628 60136fdd80c4
parent 1592 d89d5ff2397f
child 2003 b48f066d52dc
     1.1 --- a/src/Pure/library.ML	Thu Mar 28 17:21:58 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Mar 28 17:27:54 1996 +0100
     1.3 @@ -708,6 +708,11 @@
     1.4  fun prs s = !prs_fn s;
     1.5  fun writeln s = prs (s ^ "\n");
     1.6  
     1.7 +(* output to LaTeX / xdvi *)
     1.8 +fun latex s = 
     1.9 +	execute ( "( cd /tmp ; echo \"" ^ s ^
    1.10 +	"\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
    1.11 +
    1.12  (*print warning*)
    1.13  val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
    1.14  fun warning s = !warning_fn ("Warning: " ^ s);