1 /*----------------------------------------------------------------------- 2 3 File : cio_output.h 4 5 Author: Stephan Schulz 6 7 Contents 8 9 Simple functions for secure opening of output files with - 10 convention and error checking. Much simpler than the input, because 11 much less can go wrong with output... 12 13 Copyright 1998, 1999 by the author. 14 This code is released under the GNU General Public Licence and 15 the GNU Lesser General Public License. 16 See the file COPYING in the main E directory for details.. 17 Run "eprover -h" for contact information. 18 19 Changes 20 21 <1> Fri Nov 28 11:55:59 MET 1997 22 New 23 24 -----------------------------------------------------------------------*/ 25 26 #ifndef CIO_OUTPUT 27 28 #define CIO_OUTPUT 29 30 #include <stdio.h> 31 #include <clb_dstrings.h> 32 33 /*---------------------------------------------------------------------*/ 34 /* Data type declarations */ 35 /*---------------------------------------------------------------------*/ 36 37 38 #define OUTPRINT(level, message)\ 39 if(level<= OutputLevel){fprintf(GlobalOut, message);} 40 41 42 /*---------------------------------------------------------------------*/ 43 /* Exported Functions and Variables */ 44 /*---------------------------------------------------------------------*/ 45 46 extern long OutputLevel; 47 extern FILE* GlobalOut; 48 extern int GlobalOutFD; 49 50 #define InitOutput() GlobalOut=stdout;GlobalOutFD=STDOUT_FILENO 51 void OpenGlobalOut(char* outname); 52 FILE* OutOpen(char* name); 53 void OutClose(FILE* file); 54 void PrintDashedStatuses(FILE* out, char *stat1, char *stat2, char *fallback); 55 56 #endif 57 58 /*---------------------------------------------------------------------*/ 59 /* End of File */ 60 /*---------------------------------------------------------------------*/ 61 62 63 64 65 66