Take advantage of text formatting messages in IDE protocol

[ohad]

The IDE protocol has a few messages for formatting text.

• [x] We should refactor the pretty printer so that it's easy to also send the docstring formatting in semantic highlighting.
• [ ] It's not quite clear how we should use link-href messages in their full generality: usually we want to hyperlink to the hyperlink that appears in the text itself.

(This is a stub to be expanded later.)

[gallais]

I guess the second goal is dependent on us starting to parse docstrings to make sense of them

[gallais]

TIL the ide-mode has way more font faces by default:

Show Idris2 Active Term Face:[sample]
   The face to highlight active terms

Show Idris2 Antiquotation Face:[sample]
   The face to be used to highlight antiquotations in Idris2 source code

Show Idris2 Char Face:[sample]
   The face used to highlight character literals in Idris2

Show Idris2 Colon Face:[sample]
   The face to highlight ’:’ in type annotations with.

Show Idris2 Definition Face:[sample]
   The face to highlight things being defined in.

Show Idris2 Directive Argument Face:[sample]
   The face to highlight arguments to Idris2 directives.

Show Idris2 Directive Face:[sample]
   The face to highlight Idris2 compiler directives.

Show Idris2 Equals Face:[sample]
   The face to highlight ’=’ in definitions with.

Show Idris2 Hole Face:[sample]
   The face to highlight Idris2 holes with.

Show Idris2 Identifier Face:[sample]
   The face to highlight Idris2 identifiers with.

Show Idris2 Info Title Face:[sample]
   Face for Idris2 headers and titles.

Show Idris2 Inline Doc Face:[sample]
   The face shown for Idris2Doc while editing Idris2 files.

Show Idris2 Ipkg Keyword Face:[sample]
   The face to highlight Idris2 package keywords

Show Idris2 Ipkg Package Name Face:[sample]
   The face to highlight the name of the package

Show Idris2 Keyword Face:[sample]
   The face to highlight Idris2 keywords with.

Show Idris2 Link Face:[sample]
   The face shown for Web links in Idris2 documentation.

Show Idris2 Loaded Region Face:[sample]
   The face to use for the currently-loaded region of a More

Show Idris2 Log Level 1 Face:[sample]
   The face used for log level 1 in the Idris2 log

Show Idris2 Log Level 2 Face:[sample]
   The face used for log level 2 in the Idris2 log

Show Idris2 Log Level 3 Face:[sample]
   The face used for log level 3 in the Idris2 log

Show Idris2 Log Level 4 Face:[sample]
   The face used for log level 4 in the Idris2 log

Show Idris2 Log Level 5 Face:[sample]
   The face used for log level 5 in the Idris2 log

Show Idris2 Log Level Face:[sample]
   General properties for displaying Idris2 log levels

Show Idris2 Log Level Higher Face:[sample]
   The face used for log levels over 5 in the Idris2 log

Show Idris2 Log Timestamp Face:[sample]
   The face used for timestamps in the Idris2 log

Show Idris2 Module Face:[sample]
   The face to highlight Idris2 module names with.

Show Idris2 Operator Face:[sample]
   The face to highlight operators with.

Show Idris2 Parameter Face:[sample]
   The face to highlight formal parameters to function definitions with.

Show Idris2 Prover Processed Face:[sample]
   Face for Idris2 proof script which is already processed.

Show Idris2 Prover Processing Face:[sample]
   Face for Idris2 proof script which is currently processing.

Show Idris2 Quasiquotation Face:[sample]
   The face to be used to highlight quasiquotations in Idris2 source code

Show Idris2 Semantic Bound Face:[sample]
   The face to be used to highlight bound variables

Show Idris2 Semantic Data Face:[sample]
   The face to be used to highlight data and constructors

Show Idris2 Semantic Function Face:[sample]
   The face to be used to highlight defined functions

Show Idris2 Semantic Implicit Face:[sample]
   The face to be used to highlight implicit arguments

Show Idris2 Semantic Module Face:[sample]
   The face to be used to highlight namespace declarations

Show Idris2 Semantic Namespace Face:[sample]
   The face to be used to highlight namespace declarations

Show Idris2 Semantic Postulate Face:[sample]
   The face to be used to highlight postulated values

Show Idris2 Semantic Type Face:[sample]
   The face to be used to highlight types

Show Idris2 Unsafe Face:[sample]
   The face used to highlight unsafe Idris2 features, such as %assert_total

Show Idris2 Warning Face:[sample]
   Face for warnings from the compiler.