} else if (tokens[0] === 'ANNOTATION') {
let position = parser.parse_yx(tokens[1]);
explorer.update_info_db(position, tokens[2]);
+ tui.restore_input_values();
+ tui.full_refresh();
} else if (tokens[0] === 'UNHANDLED_INPUT') {
tui.log_msg('? unknown command');
} else if (tokens[0] === 'PLAY_ERROR') {
this.map_mode = 'terrain';
if (mode.shows_info && game.player_id in game.things) {
explorer.position = game.things[game.player_id].position;
+ explorer.query_info();
}
this.mode = mode;
this.empty_input();