message: hover: Show docs when available
diff: @@ -14,12 +14,20 @@ export class LeanHoverProvider implements HoverProvider {
  public provideHover(document : TextDocument, position : Position, CancellationToken) : Thenable<Hover> {
  return this.server.info(document.fileName, position.line + 1, position.character).then((response) => {
  // Maybe use more sohpisticated typing here?
  - if (response.record && response.record['full-id']) {
  + let marked = [];
  + if (response.record) {
  + if (response.record['full-id']) {
  let msg = response.record['full-id'] + ' : ' + response.record['type'];
  - let marked = { language: 'lean', value: msg };
  - return new Hover(marked, new vscode.Range(position.line - 1, position.character, position.line - 1, position.character));
  - } else if (response.record && response.record.state) {
  - let marked = { language: 'lean', value: response.record.state };
  + marked.push({ language: 'lean', value: msg });
  + }
  + if (response.record.doc) {
  + marked.push(response.record.doc);
  + }
  + if (response.record.state && !marked) {
  + marked.push({ language: 'lean', value: response.record.state });
  + }
  + }
  + if (marked) {
  return new Hover(marked, new vscode.Range(position.line - 1, position.character, position.line - 1, position.character));
  } else {
  return null;
  