Skip to content

Commit

Permalink
feat: Improve display of help
Browse files Browse the repository at this point in the history
  • Loading branch information
famoser committed Feb 19, 2024
1 parent 76fa9ae commit 55f0e2f
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 18 deletions.
40 changes: 26 additions & 14 deletions server/src/hover.ts
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import {
Hover, LocationLink,
Hover, LocationLink, MarkupContent, MarkupKind,
ParameterInformation,
Position,
SignatureHelp,
Expand Down Expand Up @@ -30,43 +30,55 @@ export const getHover = async (identifier: TextDocumentIdentifier, position: Pos

const constructHover = (definitionSymbol: ProverifSymbol, source: ParseTree): Hover | undefined => {
const range = getRange(source);
const contents = getFullName(definitionSymbol);
const fullName = getFullName(definitionSymbol);
const contents = createProverifMarkupContent(fullName);

return {range, contents};
};

const createProverifMarkupContent = (proverifCode: string): MarkupContent => {
return {
kind: MarkupKind.Markdown,
value: [
'```pv',
proverifCode,
'```'
].join('\n')
};
};

const getFullName = (definitionSymbol: ProverifSymbol): string => {
const declarationPrefix = getDeclarationPrefix(definitionSymbol.declaration)
const name = definitionSymbol.node.text
const parametersString = getParametersString(definitionSymbol.parameters)
const typeSuffix = getTypeSuffix(definitionSymbol.type)
const declarationPrefix = getDeclarationPrefix(definitionSymbol.declaration);
const name = definitionSymbol.node.text;
const parametersString = getParametersString(definitionSymbol.parameters);
const typeSuffix = getTypeSuffix(definitionSymbol.type);

return declarationPrefix + name + parametersString + typeSuffix
return declarationPrefix + name + parametersString + typeSuffix;
};

const getDeclarationPrefix = (declarationType: DeclarationType): string => {
switch (declarationType) {
case DeclarationType.Parameter:
case DeclarationType.DefineParameter:
case DeclarationType.ExpandParameter:
return "";
return "(parameter) ";
default:
return `${declarationType} `;
}
};

const getParametersString = (parameters?: (ProverifSymbolParameter|undefined)[]): string => {
const getParametersString = (parameters?: (ProverifSymbolParameter | undefined)[]): string => {
if (!parameters) {
return "";
}

const parameterListString = parameters
.map(parameter => parameter ? parameter.node.text + getTypeSuffix(parameter.type) : "")
.join(", ")
.join(", ");

return `(${parameterListString})`
}
return `(${parameterListString})`;
};

const getTypeSuffix = (type?: ParseTree) => {
return type ? ": " + type.text : ""
}
return type ? ": " + type.text : "";
};
8 changes: 4 additions & 4 deletions server/src/server.ts
Original file line number Diff line number Diff line change
Expand Up @@ -89,13 +89,13 @@ connection.onDefinition(async (params) => {
});

connection.onHover(async (params) => {
const hover = await getHover(params.textDocument, params.position, documentManager)
const hover = await getHover(params.textDocument, params.position, documentManager);
if (!hover) {
return undefined
return undefined;
}

return hover
})
return hover;
});

connection.onDocumentLinks(async params => {
const parseResult = await documentManager.getParseResult(params.textDocument);
Expand Down

0 comments on commit 55f0e2f

Please sign in to comment.