// @(#)$Id: next_token.lh,v 1.6 1997/06/03 20:30:16 leavens Exp $
#include "istream.lh"
#include "Token.lh"
static Token current_token;
extern void next_token() throw();
//@ behavior {
//@ extern Token current_token; // global variable referenced
//@ extern istream cin; // another global variable
//@
//@ requires assigned(cin, pre);
//@ modifies current_token, cin;
//@ ensures current_token' = scan_token(cin^) /\ cin' = remove_token(cin^);
//@ }
[Index]
HTML generated using lcpp2html.