Re: [isabelle] Running Isabelle in batch mode



On Wed, 28 Oct 2015, Viorel Preoteasa wrote:

I am interested in processing a theory in batch mode, and outputting at the end (in the terminal) some specific information, and I want to suppress all the other output that is produced.

Of course, you can always use your own private output channel, e.g. a named pipe (fifo) on Unix-based systems.

A more basic approach is Outout.physical_stderr: it is used by the system in rare situations to emit messages to the terminal, bypassing almost everything else. You can hypersearch the Isabelle/ML sources, to see where this is used.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.