extern void closeinput(void);
extern int ded_inline(char *, int (*)());
extern void openinput(char *fname, int (*)());