What do colour codes mean in Isabelle/jEdit?

Question

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?

Answer 1

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 *))