[VsCoq1] Added a rudimentary message panel

client/src/CoqDocument.ts

@@ -176,33 +176,17 @@ export class CoqDocument implements vscode.Disposable {
   // }
 
   private onCoqMessage(params: proto.NotifyMessageParams) {
-    if (params.routeId == this.queryRouteId) {
-      this.project.queryOut.show(true);
-      this.project.queryOut.appendLine(psm.prettyTextToString(params.message));
-    } else if (params.routeId == this.hoverQueryRouteId) {
+    /* 
+      originally, all messages will be output to their corresponding channels
+      now with the message panel, they will be output on the message panel, 
+        EXCEPT those which should be displayed as hovering text
+    */
+    if (params.routeId == this.hoverQueryRouteId) {
       const hoverText = psm.prettyTextToString(params.message);
       if (this.hoverListener)
         this.hoverListener(hoverText);
-    }
-    else {
-      switch (params.level) {
-        case 'warning':
-          this.project.infoOut.show(true);
-          this.project.infoOut.appendLine(psm.prettyTextToString(params.message));
-          return;
-        case 'info':
-          this.project.infoOut.appendLine(psm.prettyTextToString(params.message));
-          return;
-        case 'notice':
-          this.project.noticeOut.show(true);
-          this.project.noticeOut.append(psm.prettyTextToString(params.message));
-          this.project.noticeOut.append("\n");
-          return;
-        case 'debug':
-          this.project.debugOut.show(true);
-          this.project.debugOut.appendLine(psm.prettyTextToString(params.message));
-          return;
-      }
+    } else {
+      this.view.update({ innertext: params.message, type: "message-query" });
     }
   }
 
@@ -366,7 +350,7 @@ export class CoqDocument implements vscode.Disposable {
       }
     } else if(value.type === 'interrupted')
       this.statusBar.setStateComputing(proto.ComputingStatus.Interrupted)
-    else
+    else if (value.type !== 'message-query' && value.type !== 'message-ready-clear')
       this.updateFocus(value.focus, this.project.settings.moveCursorToFocus);
 
     return true;
@@ -423,6 +407,7 @@ export class CoqDocument implements vscode.Disposable {
     try {
       this.makePreviewOpenedFilePermanent(editor);
       this.rememberCursors();
+      this.view.update({ type:"message-ready-clear" });
       const value = await this.langServer.stepForward();
       this.updateView(value, true);
       this.handleResult(value);
@@ -449,6 +434,7 @@ export class CoqDocument implements vscode.Disposable {
   public async finishComputations(editor: TextEditor) {
     this.statusBar.setStateWorking('Finishing computations');
     try {
+      this.view.update({ type:"message-ready-clear" });
       await this.langServer.finishComputations();
       this.statusBar.setStateReady();
     } catch (err) {
@@ -461,6 +447,7 @@ export class CoqDocument implements vscode.Disposable {
       if(!editor || editor.document.uri.toString() !== this.documentUri)
        return;
       this.makePreviewOpenedFilePermanent(editor);
+      this.view.update({ type:"message-ready-clear" });
       const value = await this.langServer.interpretToPoint(editor.selection.active, synchronous);
       this.updateView(value, true);
       this.handleResult(value);
@@ -476,6 +463,7 @@ export class CoqDocument implements vscode.Disposable {
     this.statusBar.setStateWorking('Interpreting to end');
     try {
       this.makePreviewOpenedFilePermanent(editor);
+      this.view.update({ type:"message-ready-clear" });
       const value = await this.langServer.interpretToEnd(synchronous);
       this.updateView(value, true);
       this.handleResult(value);
@@ -486,8 +474,9 @@ export class CoqDocument implements vscode.Disposable {
   public async query(query: proto.QueryFunction, term: string | undefined) {
     try {
       if (term) {
-        this.project.queryOut.clear();
-        this.project.queryOut.show(true);
+        // this.project.queryOut.clear();
+        this.view.update({ type:"message-ready-clear" });
+        // this.project.queryOut.show(true);
         this.langServer.query(query, term, this.queryRouteId);
       }
     } catch (err) {

client/src/CoqProject.ts

@@ -26,10 +26,12 @@ export class CoqProject implements vscode.Disposable {
   private subscriptions : vscode.Disposable[] = [];
 
   // lazily created output windows
+  /*
   private infoOutput: vscode.OutputChannel = vscode.window.createOutputChannel('Info');
   private queryOutput: vscode.OutputChannel = vscode.window.createOutputChannel('Queries');
   private noticeOutput: vscode.OutputChannel = vscode.window.createOutputChannel('Notices');
   private debugOutput: vscode.OutputChannel = vscode.window.createOutputChannel('Debug');
+  */
 
   private constructor(context: vscode.ExtensionContext) {
     this.langServer = CoqLanguageServer.create(context);
@@ -70,6 +72,7 @@ export class CoqProject implements vscode.Disposable {
     return CoqProject.instance;
   }
 
+  /*
   public get infoOut(): vscode.OutputChannel {
     return this.infoOutput;
   }
@@ -82,11 +85,14 @@ export class CoqProject implements vscode.Disposable {
   public get debugOut(): vscode.OutputChannel {
     return this.debugOutput;
   }
+  */
 
   dispose() {
+    /*
     this.infoOutput.dispose();
     this.queryOutput.dispose();
     this.noticeOutput.dispose();
+    */
     this.documents.forEach((doc) => doc.dispose());
     this.subscriptions.forEach((s) => s.dispose());
     this.langServer.dispose();

client/src/HtmlCoqView.ts

@@ -41,7 +41,12 @@ interface SettingsState {
   proofViewDiff?: ProofViewDiffSettings;
 }
 
-type ProofViewProtocol = GoalUpdate | SettingsUpdate;
+interface QueryMessageUpdate {
+  command: "message-query";
+  msg: string
+}
+
+type ProofViewProtocol = GoalUpdate | SettingsUpdate | QueryMessageUpdate;
 
 const VIEW_PATH = "html_views";
 
@@ -146,6 +151,7 @@ export class HtmlCoqView implements view.CoqView {
         },
         {
           enableScripts: true,
+          enableFindWidget: true
         }
       );
 

client/src/protocol.ts

@@ -166,20 +166,30 @@ export interface CommandInterrupted {
   range: vscode.Range
 }
 
+export interface QueryMessageWrapper {
+  innertext: AnnotatedText
+}
+
 export type FocusPosition = {focus: vscode.Position}
 export type NotRunningTag = {type: 'not-running'}
 export type NoProofTag = {type: 'no-proof'}
 export type FailureTag = {type: 'failure'}
 export type ProofViewTag = {type: 'proof-view'}
 export type InterruptedTag = {type: 'interrupted'}
 export type BusyTag = {type: 'busy'}
+export type QueryMessageTag = {type: 'message-query'}
+export type ReadyClearMessageTag = {type: 'message-ready-clear'}
 export type NotRunningResult = NotRunningTag & {reason: "not-started"|"spawn-failed", coqtop?: string}
 export type BusyResult = BusyTag
 export type NoProofResult = NoProofTag
 export type FailureResult = FailValue & FailureTag
 export type ProofViewResult = ProofView & ProofViewTag
 export type InterruptedResult = CommandInterrupted & InterruptedTag
+export type QueryMessageResult = QueryMessageWrapper & QueryMessageTag
+export type ReadyClearMessageResult = ReadyClearMessageTag
 export type CommandResult =
+  QueryMessageResult |
+  ReadyClearMessageResult |
   NotRunningResult |
   (BusyResult & FocusPosition) |
   (FailureResult & FocusPosition) |

html_views/src/goals/display-proof-state.ts

@@ -232,20 +232,63 @@ export const ProofState = () => {
   return { element, updateState, unmount };
 };
 
+export const OtherInfoView = () => {
+  const messageView = h("vscode-panel-view");
+  const element = h("vscode-panels.panels", [
+    h("vscode-panel-tab", "MESSAGE"),
+    messageView
+  ]);
+
+  let messageViewInnerDiv = h("pre");
+  messageView.appendChild(messageViewInnerDiv);
+
+  /* 
+    clear-on-demand: 
+    if this flag is set, the message panel will be reset on receiving the next incoming message
+    and this flag will be unset immediately after that
+  */
+  let ready : boolean = true;
+
+  const readyForMessageReset = () => {
+    ready = true;
+  };
+
+  const updateInnerMessage = (s : AnnotatedText) => {
+    if (ready){
+      messageViewInnerDiv.innerHTML = "";
+      ready = false;
+    }
+    messageViewInnerDiv.appendChild(h("span", [...createAnnotatedText(s), "\n"]));
+  };
+
+  return { element, updateInnerMessage, readyForMessageReset };
+};
+
 export const Infoview = () => {
   const element = h("div");
 
   let proofStateInstance: ReturnType<typeof ProofState> | undefined = undefined;
+  let otherViewInstance = OtherInfoView();
+  let divider = h("vscode-divider");
 
   const updateState = (state: CommandResult) => {
     if (state.type === "proof-view") {
       if (proofStateInstance === undefined) {
         element.innerHTML = "";
         proofStateInstance = ProofState();
         element.appendChild(proofStateInstance.element);
+        element.appendChild(divider);
+        element.appendChild(otherViewInstance.element);
       }
 
       proofStateInstance.updateState(state);
+    } else if (state.type === "message-query") {
+      // if (state.innertext)
+      otherViewInstance.updateInnerMessage(state.innertext);
+      // else
+      //   otherViewInstance.updateInnerMessage("nothing. why?");
+    } else if (state.type === "message-ready-clear") {
+      otherViewInstance.readyForMessageReset();
     } else {
       if (proofStateInstance !== undefined) {
         proofStateInstance.unmount();
@@ -257,6 +300,8 @@ export const Infoview = () => {
       element.innerHTML = "";
       const formatted = h("div.message", message);
       element.appendChild(formatted);
+      element.appendChild(divider);
+      element.appendChild(otherViewInstance.element);
     };
 
     const setErrorMessage = (message: HTMLElement) => {
@@ -266,6 +311,8 @@ export const Infoview = () => {
         h("code", message),
       ]);
       element.appendChild(formatted);
+      element.appendChild(divider);
+      element.appendChild(otherViewInstance.element);
     };
 
     if (state.type === "not-running") {