Search code examples
isabellejedit

What do colour codes mean in Isabelle/jEdit?

What do the colour codes mean in Isabelle/jEdit? I could not find their description in the Isabelle/jEdit manual. The only thing it writes is

Prover feedback works via colors, boxes, squiggly underline, hyper- links, popup windows, icons, clickable output — all based on semantic markup produced by Isabelle in the background.

Colours are used as proof script background and on a vertical bar beside the scrollbar.

Could you point to some documentation or explain it here?

Solution

  • You can see their names and change them in "Plugins/Plugin Options" and then "Isabelle/Rendering". The names give a relatively clear explanation, and you can refer to the manuals from the terms used in the names.

    There is a lot of colors so I won't describe them all. For the most important default colors:

    Logic:

    • blue : free variable
    • green : bound variable
    • orange : skolem constant ("free" variables existentially "quantified")
    • cyan : syntax (not a variable or a constant, like case or if)

    Isar Keywords:

    • sky blue : commands (like lemma, proof or have)
    • red : tactic-style commands (like apply, done or prefer)
    • turquoise : statements (like where, fixes, shows or and)

    Messages highlighting in output:

    • red : error
    • yellow : warning
    • light blue : info

    Highlighting in editor:

    • red : error
    • light yellow : current line
    • gray : quoted text (logic and types)
    • light gray : comment and formal text (introduced with text or section)
    • purple : running process on the command (also shown on the right)
    • pink : unprocessed (outdated) command (also shown on the right)

    In general, an underlined command displays a message in the output (possibly associated with an icon and a box on the right). More specifically:

    Icons, [boxes] and {in text}:

    • red exclamation mark [red box] {squiggly red underline} : error
    • orange exclamation mark [orange box] {squiggly orange underline} : warning
    • blue i {squiggly blue underline}: information (often provided by automatic tools)
    • {squiggly gray underline} : the command shows a message in the output
    • {red text} : comment (like (* This is a comment *))