Что означают цветовые коды в Isabelle/jEdit?

Question

Что означают цветовые коды в Изабель /jEdit? Я не смог найти их описание в руководстве к Isabelle/jEdit. Единственное, что он пишет, это

Обратная связь доказательств работает с помощью цветов, блоков, волнистого подчеркивания, гиперссылок, всплывающих окон, значков, интерактивного вывода - все это основано на семантической разметке, созданной Изабель в фоновом режиме.

Цвета используются в качестве фона сценария проверки и на вертикальной полосе рядом с полосой прокрутки.

Не могли бы вы указать на некоторую документацию или объяснить ее здесь?

Answer 1

Вы можете увидеть их имена и изменить их в "Параметры плагинов / плагинов", а затем "Изабель / Рендеринг". Имена дают относительно четкое объяснение, и вы можете ссылаться на руководства из терминов, используемых в именах.

Цветов много, поэтому я не буду их всех описывать. Для наиболее важных цветов по умолчанию:

Логика:

• синий: свободная переменная
• зеленый: связанная переменная
• оранжевый: постоянная сколема ("свободные" переменные экзистенциально "количественно")
• cyan: синтаксис (не переменная или константа, как case или же if)

Изар Ключевые слова:

• небесно-голубой: команды (как lemma, proof или же have)
• красный: команды в стиле тактики (например, apply, done или же prefer)
• бирюзовый: заявления (как where, fixes, shows или же and)

Подсветка сообщений в выводе:

• красный: ошибка
• желтый: предупреждение
• голубой: информация

Выделение в редакторе:

• красный: ошибка
• светло-желтый: текущая линия
• серый: цитируемый текст (логика и типы)
• светло-серый: комментарий и формальный текст text или же section)
• фиолетовый: выполнение процесса по команде (также показано справа)
• розовый: необработанная (устаревшая) команда (также показана справа)

Как правило, подчеркнутая команда отображает сообщение в выходных данных (возможно, связанных со значком и полем справа). Более конкретно:

Иконки, [поля] и {в тексте}:

• красный восклицательный знак [красная рамка] {волнистое красное подчеркивание}: ошибка
• оранжевый восклицательный знак [оранжевая рамка] {волнистое оранжевое подчеркивание}: предупреждение
• синий я {волнистое синее подчеркивание}: информация (часто предоставляемая автоматическими инструментами)
• {волнистое серое подчеркивание}: команда показывает сообщение в выводе
• {красный текст}: комментарий (как (* This is a comment *))