[goals] Display position for goals, handle multiple goals better.

Still a long way to go, but this already looks much better.

Fixes #109

CHANGES.md

@@ -19,6 +19,8 @@
  - Show goals on click by default, allow users to configure the
    behavior to follow cursor in different ways (@ejgallego, #116,
    fixes #89)
+ - Show file position in goal buffer, use collapsible elements for
+   goal list (@ejgallego, #115, fixes #109)
 
 # coq-lsp 0.1.0: Memory
 -----------------------

controller/coq_lsp.ml

@@ -331,7 +331,16 @@ let do_goals ofmt ~id params =
   let uri, point = get_docTextPosition params in
   let doc = Hashtbl.find doc_table uri in
   let goals = Fleche.Info.LC.goals ~doc ~point goals_mode in
-  let result = `List (mk_goals goals) in
+  let result =
+    `Assoc
+      [ ( "textDocument"
+        , `Assoc [ ("uri", `String uri); ("version", `Int doc.version) ] )
+      ; ( "position"
+        , `Assoc [ ("line", `Int (fst point)); ("character", `Int (snd point)) ]
+        )
+      ; ("goals", `List (mk_goals goals))
+      ]
+  in
   let msg = LSP.mk_reply ~id ~result in
   LIO.send_json ofmt msg
 

editor/code/media/styles.css

@@ -1,6 +1,6 @@
 body {
-    font-size:medium;
-    /* font-size: var(--vscode-editor-font-size); */
+    font-size: var(--vscode-editor-font-size);
+    /* font-size: medium */
     font-family: var(--vscode-editor-font-family);
     /* font-family: 'Segoe UI', Tahoma, Geneva, Verdana, sans-serif; */
 }
@@ -23,4 +23,9 @@ body {
 
 .sep, hr {
     color : var(--vscode-editorRuler-foreground);
+}
+
+.goalDiv {
+    margin-left: 0.5ex;
+    margin-top: 0.5ex;
 }

editor/code/src/client.ts

@@ -50,7 +50,7 @@ export function panelFactory(context: ExtensionContext) {
 }
 
 export function activate(context: ExtensionContext): void {
-    window.showInformationMessage("Going to activate!");
+    window.showInformationMessage("Coq LSP Extension: Going to activate!");
 
     function coqCommand(command: string, fn: () => void) {
         let disposable = commands.registerCommand("coq-lsp." + command, fn);

editor/code/src/goals.ts

@@ -1,3 +1,4 @@
+import { basename } from "path";
 import { Webview, Position, Uri, WebviewPanel } from "vscode";
 import { RequestType, TextDocumentIdentifier, VersionedTextDocumentIdentifier } from "vscode-languageclient";
 import { LanguageClient } from "vscode-languageclient/node";
@@ -12,44 +13,47 @@ interface Goal {
 }
 
 interface GoalRequest {
-    textDocument: TextDocumentIdentifier,
-    position: Position
+    textDocument: TextDocumentIdentifier;
+    position: Position;
 }
 
-// returns the HTML code of goals environment
-function getGoalsEnvContent(goals: Goal[]) {
-    if (goals.length == 0) return "No goals";
+interface GoalAnswer {
+    textDocument: VersionedTextDocumentIdentifier;
+    position: Position;
+    goals : Goal[];
+}
 
-    return goals
-        .map((curGoal, itr) => {
-            return (
-                '<div class="hypothesis">' +
-                curGoal.hyps
-                    .map((hyp) => {
-                        return (
-                            `<label class="hname">${hyp.names}</label>` +
-                            `<label class="sep"> : </label>` +
-                            `<span class="htype">${hyp.ty}</span><br/>`
-                        );
-                    })
-                    .reduce((acc, cur) => acc + cur, "") +
-                "</div>" +
-                "<hr/>" +
-                `<div class="pp_goals">` +
-                `<label class="numGoal">${itr}</label>` +
-                `<label class="sep"> : </label>` +
-                `<span class="goal">${curGoal.ty}</span>` +
-                `<label class ="sep"></label><br/><br/>` +
-                `</div>`
-            );
-        })
-        .reduce((acc, cur) => acc + cur, "");
+function htmlOfHyp(hyp : Hyp) {
+    let hypBody = 
+        `<label class="hname">${hyp.names}</label>` +
+        `<label class="sep"> : </label>` +
+        `<span class="htype">${hyp.ty}</span><br/>`;
+
+    return `<div class="hypothesis"> ${hypBody} </div>`;
+}
+function htmlOfGoal(goal : Goal, idx : number) {
+    let hyps = goal.hyps.map(htmlOfHyp).join(' ');
+    let goalBody = `<div class="pp_goals"> <span class="goal">${goal.ty}</span><br/></div>`;
+    let summary = `<summary>Goal ${idx}</summary>`;
+    return `<details ${(idx == 0) ? "open" : "closed"}> ${summary}` +
+           `<div class="goalDiv">${hyps} <hr/> ${goalBody} </div>` +
+           `</details>`;
+}
+
+// returns the HTML code of goals environment
+function htmlOfGoals(goals: Goal[]) {
+    if (goals.length == 0)
+        return "No goals"
+    else
+        return goals.map(htmlOfGoal).join('<br/>');
 }
 
 // Returns the HTML code of the panel and the inset ccontent
-function buildGoalsContent(goals: Goal[], styleUri: Uri) {
+function buildGoalsContent(goals: GoalAnswer, styleUri: Uri) {
     // get the HTML code of goals environment
-    let codeEnvGoals: String = getGoalsEnvContent(goals);
+    let vsUri = Uri.parse(goals.textDocument.uri);
+    let uriBase = basename(vsUri.path);
+    let codeEnvGoals: String = htmlOfGoals(goals.goals);
 
     // Use #FA8072 color too?
     return `
@@ -62,9 +66,12 @@ function buildGoalsContent(goals: Goal[], styleUri: Uri) {
         <title>Goals</title>
     </head>
     <body>
-        <p class="goals_env">
-        ${codeEnvGoals}
-        </p>
+        <details open>
+            <summary>${uriBase}:${goals.position.line}:${goals.position.character}</summary>
+            <div class="goals_env" style="margin-left: 0.5ex;">
+                ${codeEnvGoals}
+            </div>
+        </details>
     </body>
     </html>`;
 }
@@ -84,15 +91,15 @@ class GoalView {
         this.sendGoalsRequest(uri, position);
     }
 
-    display(goals: Goal[]) {
+    display(goals: GoalAnswer) {
         this.view.html = buildGoalsContent(goals, this.styleUri);
     }
 
     // LSP Protocol extension for Goals
     sendGoalsRequest(uri: Uri, position: Position) {
         let doc = { uri: uri.toString() };
         let cursor : GoalRequest = { textDocument: doc, position: position };
-        const req = new RequestType<GoalRequest, Goal[], void>("proof/goals");
+        const req = new RequestType<GoalRequest, GoalAnswer, void>("proof/goals");
         this.client.sendRequest(req, cursor).then(
             (goals) => this.display(goals),
             () => {

etc/doc/PROTOCOL.md

@@ -59,8 +59,9 @@ that none of them are stable yet:
 
 In order to display proof goals, `coq-lsp` supports the `proof/goals` request, parameters are:
 ```typescript
-{ textDocument: uri
-, position: Position
+interface GoalRequest {
+    textDocument: VersionedTextDocumentIdentifier;
+    position: Position;
 }
 ```
 
@@ -70,12 +71,17 @@ interface Hyp {
     names: string;
     ty: string;
 }
+
 interface Goal {
     ty: string;
     hyps: Hyp[];
 }
 
-interface CoqFileProgressParams {
+interface GoalAnswer {
+    textDocument: VersionedTextDocumentIdentifier;
+    position: Position;
+    goals : Goal[];
+}
 
 ```