enum ui_input_mode input_mode;
struct rule *rule;
struct point *slot;
- WINDOW *workspace_w;
- WINDOW *support_w;
- WINDOW *echo_w;
+ WINDOW *workspace;
+ WINDOW *status_bar;
+ WINDOW *echo_area;
GHashTable *rules; /* str -> rule */
GHashTable *globals; /* str -> name */
GHashTable *temporaries; /* str -> name */
GHashTable *gctxs; /* str -> name */
GHashTable *gtheses; /* str -> name */
+ GSList *ordered_rules; /* rule names */
GSList *support; /* rules */
GString *input;
GString *special;
g_hash_table_insert(temporaries, name->str, name);
}
+void
+insert_rule(struct state *state, struct rule *rule)
+{
+ g_hash_table_insert(state->rules, rule->name, rule);
+ state->ordered_rules = g_slist_prepend(state->ordered_rules, rule->name);
+}
+
/*
* Remove entries with contextual scope. This is the end of the line for
* variables.
strs[i]);
}
if (state->input_mode == ui_input_mode_command)
- echo_esc(state->echo_w, state->command->str);
+ echo_esc(state->echo_area, state->command->str);
refresh();
}
addch(c);
fclose(fd);
if (state->input_mode == ui_input_mode_command)
- echo_esc(state->echo_w, state->command->str);
+ echo_esc(state->echo_area, state->command->str);
refresh();
}
wattroff(w, COLOR_PAIR(pair));
}
+int
+status_bar_str(char *buf, size_t len,
+ enum ui_major_mode major_mode, enum ui_input_mode input_mode,
+ struct point *p, char *input, char key, GHashTable *temporaries)
+{
+ int n = 0;
+ GSList *l;
+ GList *head, *l1;
+
+ n += snprintf(buf, len, " %d:%d (%d,%d,%d,%d,[",
+ major_mode, input_mode,
+ p->is_conclusion,
+ p->st,
+ p->judgment_idx,
+ p->vdecl_idx);
+ l = p->stack;
+ if (!l)
+ n += snprintf(buf + n, len - n, "NULL])");
+ while (l) {
+ n += snprintf(buf + n, len - n, "%d", GPOINTER_TO_INT(l->data));
+ if (l->next)
+ n += snprintf(buf + n, len - n, ",");
+ else
+ n += snprintf(buf + n, len - n, "])");
+ l = l->next;
+ }
+ n += snprintf(buf + n, len - n, " \"%s\"", input);
+ if (key > 31 && key < 127)
+ n += snprintf(buf + n, len - n, " '%c'", key);
+ else if (key == '\t')
+ n += snprintf(buf + n, len - n, " 'TAB'");
+ else if (key == '\n')
+ n += snprintf(buf + n, len - n, " 'RET'");
+ else if (key == 27)
+ n += snprintf(buf + n, len - n, " 'ESC'");
+ else
+ n += snprintf(buf + n, len - n, " UNKNOWN_KEY");
+ head = g_hash_table_get_keys(temporaries);
+ if (head)
+ n += snprintf(buf + n, len - n, " ");
+ l1 = head;
+ while (l1) {
+ n += snprintf(buf + n, len - n, "%s", l1->data);
+ if (l1->next)
+ n += snprintf(buf + n, len - n, " ");
+ l1 = l1->next;
+ }
+ n += snprintf(buf + n, len - n, " ");
+ g_list_free(head);
+ return n;
+}
+
void
render(struct state *state, char kkey)
{
- int y, x, q, i, caret_offset;
+ int caret_offset;
+ int y, x, h, w, h1, w1, yoff, xoff, maxw, maxn, n;
static const char *str1 = "g: generic t: type e: element "
"=t: judgmentally equal types =e: judgmentally equal elements";
static const char *str2 = "=t: judgmentally equal types "
"=e: judgmentally equal elements";
- GHashTableIter iter;
- /* GSList *l, *deps; */
- GList *head, *l1;
+ char buf[COLS];
GSList *l;
- gpointer key, value;
struct rule *rule;
struct point *p;
- q = (LINES - 3) / 2;
clear();
- /* draw debug info */
- i = 0;
- head = g_hash_table_get_keys(state->temporaries);
- l1 = head;
- while (l1) {
- mvwprintw(stdscr, LINES - 4, i, "%s", l1->data);
- i += strlen(l1->data) + 1;
- l1 = l1->next;
- }
- g_list_free(head);
- mvwprintw(stdscr, LINES - 3, 0,
- "major_mode: %d input_mode: %d is_conclusion: %d "
- "st: %d j_idx: %d v_idx: %d ",
- state->major_mode, state->input_mode,
- state->slot->is_conclusion,
- state->slot->st,
- state->slot->judgment_idx,
- state->slot->vdecl_idx);
- wprintw(stdscr, "stack: ");
- l = state->slot->stack;
- if (!l)
- wprintw(stdscr, "NULL ");
- while (l) {
- wprintw(stdscr, "%d ", GPOINTER_TO_INT(l->data));
- l = l->next;
- }
- wprintw(stdscr, " inputstr: %s key: %d",
- state->input->str,
- kkey);
-
/* draw workspace rule */
- y = 0; x = 0;
p = create_point(FALSE,
state->rule->hypotheses ? slot_type_ctx_l :
slot_type_rule_dots, 0, 0, NULL);
caret_offset = point_distance(state->rule, p, state->slot);
free_point(p);
- draw_rule(state->workspace_w, &y, &x, caret_offset,
+ h = 0; w = 0;
+ draw_rule(state->workspace, &h, &w, caret_offset,
+ TRUE, state->input->str, state->rule, TRUE);
+ y = (LINES - 2 - h) / 2; x = (COLS - w) / 2;
+ draw_rule(state->workspace, &y, &x, caret_offset,
FALSE, state->input->str, state->rule, TRUE);
/* draw existing rules */
- i = 0;
- g_hash_table_iter_init(&iter, state->rules);
- while (g_hash_table_iter_next(&iter, &key, &value))
+ yoff = 0;
+ maxw = 0; maxn = 0;
+ l = state->ordered_rules;
+ while (l)
+ {
+ rule = g_hash_table_lookup(state->rules, l->data);
+ h1 = 0; w1 = 0;
+ draw_rule(state->workspace, &h1, &w1, -1,
+ TRUE, NULL, rule, FALSE);
+ if (yoff + h1 + 1 > LINES - 2)
+ break;
+ if (w1 > maxw)
+ maxw = w1;
+ if (maxn < (n = mbstowcs(NULL, rule->name, 0)))
+ maxn = n;
+ yoff += h1 + 1;
+ l = l->next;
+ }
+ yoff = 0;
+ l = state->ordered_rules;
+ while (l)
{
- rule = value;
- y = i; x = 0;
- draw_rule(state->support_w, &y, &x, -1,
+ rule = g_hash_table_lookup(state->rules, l->data);
+ h1 = 0; w1 = 0;
+ draw_rule(state->workspace, &h1, &w1, -1,
+ TRUE, NULL, rule, FALSE);
+ n = mbstowcs(NULL, rule->name, 0);
+ if (yoff + h1 + 1 > (LINES - 2 - h) / 2 &&
+ yoff < (LINES - 2 + h) / 2 &&
+ COLS - 1 - maxn - 1 - (w1 - n - 1) < (COLS + w) / 2)
+ yoff = (LINES - 2 + h) / 2 + 1;
+ if (yoff + h1 + 1 > LINES - 2)
+ break;
+ y = yoff; x = COLS - 1 - (maxn - n) - w1;
+ draw_rule(state->workspace, &y, &x, -1,
FALSE, NULL, rule, FALSE);
- i = y + 1;
+ yoff += h1 + 1;
+ l = l->next;
}
- /* /\* draw support rules *\/ */
- /* i = 0; */
- /* l = state->support; */
- /* while (l) */
- /* { */
- /* rule = l->data; */
- /* y = i; x = 0; */
- /* draw_rule(state->support_w, &y, &x, FALSE, FALSE, -1, NULL, rule); */
- /* i = y + 2; */
- /* l = l->next; */
- /* } */
-
- /* draw window names and boundaries */
- attron(COLOR_PAIR(PAIR_INVERSE));
- move(q, 0);
- printw("workspace%*s", COLS - NB_COLUMNS - 1 - 9, "");
- move(LINES - 2, 0);
- printw("support%*s", COLS - NB_COLUMNS - 1 - 7, "");
- move(LINES - 2, COLS - NB_COLUMNS);
- printw("rules%*s", NB_COLUMNS - 5, "");
- attroff(COLOR_PAIR(PAIR_INVERSE));
- for (i = 0 ; i < LINES - 1 ; i++)
- mvprintw(i, COLS - NB_COLUMNS - 1, "█");
+ /* status bar */
+ n = status_bar_str(buf, sizeof(buf),
+ state->major_mode, state->input_mode,
+ state->slot, state->input->str, kkey,
+ state->temporaries);
+ wattron(state->status_bar, COLOR_PAIR(PAIR_INVERSE));
+ mvwprintw(state->status_bar, 0, (COLS - n) / 2, buf);
+ wattroff(state->status_bar, COLOR_PAIR(PAIR_INVERSE));
- /* draw echo area */
+ /* echo area */
if (state->input_mode == ui_input_mode_command)
- echo_esc(state->echo_w, state->command->str);
+ echo_esc(state->echo_area, state->command->str);
else if (state->err) {
- echo_status(state->echo_w, state->err);
+ echo_status(state->echo_area, state->err);
state->err = 0;
}
else {
if (state->slot->st == slot_type_thesis) {
if (state->status == 0)
- mvwprintw(state->echo_w, 0, 0, str1);
+ mvwprintw(state->echo_area, 0, 0, str1);
else
- mvwprintw(state->echo_w, 0, 0, str2);
+ mvwprintw(state->echo_area, 0, 0, str2);
}
else if (state->input_mode == ui_input_mode_special_characters) {
- mvwprintw(state->echo_w, 0, 0, "\\");
- wprintw(state->echo_w, state->special->str);
+ mvwprintw(state->echo_area, 0, 0, "\\");
+ wprintw(state->echo_area, state->special->str);
}
}
if (g_hash_table_lookup(state->rules, state->input->str))
return 2;
rule->name = strdup(state->input->str);
- g_hash_table_insert(state->rules, state->rule->name, rule);
+ insert_rule(state, rule);
c = rule->conclusion;
switch (c->kind) {
case thesis_kind_type:
gpointer hkey, hvalue;
struct state state;
+ int n = 0;
+ char cmd[100];
+
setlocale(LC_ALL, "");
initscr();
start_color();
state.input_mode = ui_input_mode_default;
state.rule = create_rule();
state.slot = create_point(FALSE, slot_type_rule_dots, 0, 0, NULL);
- state.workspace_w = subwin(stdscr, q, COLS - NB_COLUMNS - 1, 0, 0);
- state.support_w = subwin(stdscr, LINES - 1, NB_COLUMNS, 0, COLS - NB_COLUMNS);
- state.echo_w = subwin(stdscr, 1, COLS, LINES - 1, 0);
+ state.workspace = subwin(stdscr , LINES - 2, COLS, 0 , 0);
+ state.status_bar = subwin(stdscr, 1 , COLS, LINES - 2, 0);
+ state.echo_area = subwin(stdscr , 1 , COLS, LINES - 1, 0);
state.rules = g_hash_table_new_full(g_str_hash, g_str_equal,
NULL, (GDestroyNotify)free_rule);
state.globals = g_hash_table_new_full(g_str_hash, g_str_equal,
str = strdup("Small");
small = create_name(scope_global, name_kind_vet, NULL, NULL, NULL, str);
g_hash_table_insert(state.globals, str, small);
+ state.temporaries = g_hash_table_new(g_str_hash, g_str_equal);
state.gctxs = g_hash_table_new(g_str_hash, g_str_equal);
state.gtheses = g_hash_table_new(g_str_hash, g_str_equal);
- state.temporaries = g_hash_table_new(g_str_hash, g_str_equal);
+ state.ordered_rules = NULL;
state.support = NULL;
state.input = g_string_new(NULL);
state.special = g_string_new(NULL);
default:
}
}
- delwin(state.workspace_w);
- delwin(state.support_w);
- delwin(state.echo_w);
+ delwin(state.workspace);
+ delwin(state.status_bar);
+ delwin(state.echo_area);
endwin();
g_hash_table_iter_init(&iter, special_character_map);
while (g_hash_table_iter_next(&iter, &hkey, &hvalue))
g_hash_table_destroy(state.gctxs);
g_hash_table_destroy(state.gtheses);
g_hash_table_destroy(state.temporaries);
+ g_slist_free(state.ordered_rules);
g_slist_free(state.support);
g_string_free(state.input, TRUE);
g_string_free(state.special, TRUE);
projects / vouivre.git / commitdiff