odd character

[lovettchris]

This "outputs" block in Functions and Definitions has an odd character prefix "🛈 "

outputs
🛈 "Hello Lean"

I believe it's coming from this CSS, but none of the other outputs listed have this prefix:

code.info::before {
    content: "🛈 ";
    font-style: normal;
}

[david-christiansen]

In the yet-unwritten "Typographical conventions" section of the introduction, it will distinguish between three types of literal block: those that contain code submitted to Lean, those that contain informative replies from Lean (e.g. the result of #check or #eval), and those that contain error messages. The former is unmarked and will eventually get highlighting, while the latter two are marked. Right now, it happens with little "info" and "error sign" characters combined with some font changes.

How are you seeing this? On my computer, the issue looks like this:

If common computer setups don't have this character in their font, then I definitely need to do something else (e.g. a little image, or a different background).

[lovettchris]

I see, thanks for the explanation. I see the "i" with a circle around it, so yes it is coming through, font substitution in web browsers works pretty well these days. If you are unsure it works on all devices, you could instead use a symbol from https://fontawesome.com/v4/icons/ and explicitly include this font in your website ... it has a nice info circle - I also think playing with the fontsize a bit would help distinguish it from the rest of the text. Perhaps even figuring out how to make it float off the left margin or something would make it clear this is just a separate indicator and not part of the "expected output text".

[david-christiansen]

This is great feedback. I'll look into some options for a more clear presentation - this one was quick to implement, but as you can see, it needs replacing with something better now.

Thanks!

[lovettchris]

This seems to work:

custom.css:

code.info:before {
  content: "\f05a";
  font-family: "FontAwesome";
  font-style: normal;
  font-size: 12pt;
  margin-left: -30px;
  display: block;
  position: absolute;
  color: #718c00
}

code.info {
  font-style: italic;
}


code.error:before {
  content: "\f071";
  font-family: "FontAwesome";
  font-style: normal;
  font-size: 12pt;
  margin-left: -30px;
  display: block;
  position: absolute;
  color: #ff0000;
}

code.error {
  color: #ff0000;
}

Which appears like this: