Function debug_mi_format_token

src/engine/debugger.cpp:1780–1786

};

static void debug_mi_format_token( void )
{
    if ( current_token != 0 )
    {
        printf( "%d", current_token );
    }
}

static void debug_mi_format_breakpoint( int id )
{