6

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?

Makarius
  • 2,165
  • 18
  • 20
Gergely
  • 6,879
  • 6
  • 25
  • 35

1 Answers1

9

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 *))
Mathieu
  • 726
  • 3
  • 11