Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: reetz@ira.uka.de, info-hol@leopard.cs.byu.edu
In-Reply-To: <"i80fs2.ira.526:30.09.94.14.00.33"@ira.uka.de> (message from reetz on Fri, 30 Sep 1994 21:00:23 +0100)
Subject: Re: redirect print_theory from screen into file
Message-Id: <94Oct4.163236met.8067@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 4 Oct 1994 16:32:28 +0100


Ralph Reetz asks:

> Does anybody know a fast and easy way to redirect the output of
> print_theory "xxxx" from the screen into a file for HOL90.6? I just
> don't want to start trying to "hack around" redirecting std_out or
> something similiar...

You could use the following, although it does work by temporarily
redirecting the compiler's output stream:

    fun theory_to_file {theory, file} = 
       let val ostrm = open_out file
           val old = !System.Print.out
       in System.Print.out := ostrm;
          Theory.print_theory theory handle e => (close_out ostrm;
                                                  System.Print.out := old;
                                                  raise e); 
          flush_out ostrm; (* Maybe overkill *)
          close_out ostrm;
          System.Print.out := old
       end;

A better solution would be to have a visible, but abstract, type of
theories. Then the standard prettyprinting tools could be used.


> Theories are sometimes too large to simply use cut and paste and just
> a command would be easier, too. In general, it IMHO might be nice to
> have a changeable io-stream, where HOL90 emits its ``messages'' like
> in print_theory, theorems, definitions, and so on.

HOL interaction can be viewed as a "multiplexing" of various different
interaction channels. Right now, everything is basically being forced
through std_in and std_out. Separating the different dialogues, perhaps
by use of the ML type system, might be a useful idea.

Konrad.