Окно РС-формы

Внешний вид окна просмотра и редактирования представлен на Рис. 1.

Рис. 1. Иллюстрация окна просмотра и редактирования документа РС-формы КС.

Из окна документа доступно редактирование полного и короткого имен, а также комментария РС-формы. Кнопка «Проверить КС» запускает проверку корректности выражения каждой конституенты и выводит сообщение со статистикой проверки.

Рядом с кнопкой располагается индикатор корректности РС-формы. Цвет индикатора отображает статус РС-формы КС. Также на индикаторе указаны количество некорректных конституент и общее количество конституент.

В окне документа располагается два вида (View) на документ: список конституент и дерево термов. Виды отделены специальным разделителем (сплиттером), положение которого можно регулировать путем перетаскивания курсором.

Список конституент отображает атрибуты каждой конституенты: имя, типизацию (вычисляется автоматически), формальное выражение, термин, интерпретацию и комментарий. Контекстное меню дублирует некоторые операции программного меню в части редактирования конституент (Рис. 2). Неактивные для данного контекста пункты меню закрашиваются серым цветом.

Рис. 2. Контекстное меню для конституенты из списка конституент

Дополнительно список конституент предоставляет следующий функционал.

Пользовательская настройка ширины каждого столбца для удобства отображения.
Отображение статусов конституент через изменение цвета текста и цвета фона.
Редактирование атрибутов конституент при двойном щелчке либо при нажатии клавиши Ввод (Enter).
Множественное выделение конституент для выполнения последующих операций. Для выделения более 1 конституенты необходимо зажимать клавишу Ctrl или Shift, после чего выделять необходимые конституенты левым кликом мыши.
Изменение порядка следования конституент путем перетаскивания. После начала процесса перетаскивания отображается всплывающая подсказка, содержащая информацию о диапазоне доступных положений для перетаскиваемых конституент (Рис. 3).

Рис. 3. Перетаскивание группы конституент.

Порядок конституент в списке ограничен следующими правилами.

Базисные множества расположены выше конституент других типов.
Константные множества расположены сразу за последним базисным множеством.
Родовые структуры расположены выше термов, аксиом и теорем.
Конституента расположена ниже любой из конституент, от которых она зависит (в смысле вхождений имен конституент в формальные выражения).

В окне дерева термов отображается граф связей конституент на основе анализе вхождений имен одних конституент в формальные выражения других. По двойному клику на узел дерева раскрывается следующий уровень вложенности. Активные конституенты в списке конституент и дереве термов синхронизируются.

В окне дерева термов присутствует кнопка экспорта связей в формате txt-файла (Рис. 1). В файл сохраняются дуги графа термов в виде пар имен зависимой и используемой конституент. После экспорта граф термов можно визуализировать с помощью сторонних программных средств, поддерживающих работу с графами, например, Graphviz.