Merge pull request #646 from coq-community/reset-command

Plug reset command

client/goal-view-ui/src/App.tsx

@@ -34,6 +34,10 @@ const app = () => {
                 }
             );
             break;
+        case 'reset':
+            setMessages([]);
+            setGoals(null);
+            break;
     }
   }, []);
 

client/package.json

@@ -231,6 +231,11 @@
       }
     ],
     "commands": [
+      {
+        "command": "extension.coq.reset",
+        "category": "Coq",
+        "title": "Reset"
+      },
       {
         "command": "extension.coq.displayGoals",
         "category": "Coq",

client/src/extension.ts

@@ -11,7 +11,9 @@ import {workspace, window, commands, ExtensionContext,
 
 import {
   LanguageClientOptions,
+  RequestType,
   ServerOptions,
+  TextDocumentIdentifier,
 } from 'vscode-languageclient/node';
 
 import Client from './client';
@@ -23,6 +25,8 @@ import SearchViewProvider from './panels/SearchViewProvider';
 import {
     MoveCursorNotification, 
     ProofViewNotification, 
+    ResetCoqRequest, 
+    ResetCoqResponse, 
     SearchCoqResult
 } from './protocol/types';
 import { 
@@ -138,6 +142,21 @@ export function activate(context: ExtensionContext) {
             searchProvider.launchQuery(queryText, type);
         };
 
+        registerVscoqTextCommand('reset', (editor) => {
+            const uri = editor.document.uri;
+            const textDocument = TextDocumentIdentifier.create(uri.toString());
+            const params: ResetCoqRequest = {textDocument};
+            const req = new RequestType<ResetCoqRequest, ResetCoqResponse, void>("vscoq/resetCoq");
+            Client.writeToVscoq2Channel(uri.toString());
+            client.sendRequest(req, params).then(
+                (res) => {
+                    GoalPanel.resetGoalPanel();
+                }, 
+                (err) => {
+                    window.showErrorMessage(err);
+                }
+            );
+        });
         registerVscoqTextCommand('query.search', (editor) => launchQuery(editor, "search"));
         registerVscoqTextCommand('query.about', (editor) => launchQuery(editor, "about"));
         registerVscoqTextCommand('query.check', (editor) => launchQuery(editor, "check"));

client/src/panels/GoalPanel.ts

@@ -111,6 +111,19 @@ export default class GoalPanel {
     }
   }
 
+  // /////////////////////////////////////////////////////////////////////////////
+  // Change the display setting
+  //
+  // /////////////////////////////////////////////////////////////////////////////
+  public static resetGoalPanel() {
+
+    if(GoalPanel.currentPanel) {
+        Client.writeToVscoq2Channel("[GoalPanel] Resetting goal panel");
+        GoalPanel.currentPanel._reset();
+    }
+
+  }
+
   // /////////////////////////////////////////////////////////////////////////////
   // Create the goal panel if it doesn't exit and then 
   // handle a proofview notification
@@ -132,8 +145,12 @@ export default class GoalPanel {
 
   }
 
+  private _reset() {
+    this._panel.webview.postMessage({ "command": "reset"});
+  };
+
   private _handleProofViewResponseOrNotification(pv: ProofViewNotification) {
-    this._panel.webview.postMessage({ "command": "renderProofView", "proofView": pv });    
+    this._panel.webview.postMessage({ "command": "renderProofView", "proofView": pv });
   };
 
   /**

client/src/protocol/types.ts

@@ -126,3 +126,9 @@ export interface DocumentStateRequest {
 export interface DocumentStateResponse {
     document: string;
 }
+
+export interface ResetCoqRequest {
+    textDocument: TextDocumentIdentifier;
+}
+
+export interface ResetCoqResponse {};

language-server/dm/documentManager.ml

@@ -166,14 +166,6 @@ let get_messages st pos =
     | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback
     | None -> feedback
 
-let reset { uri; opts; init_vs; document; execution_state } =
-  let text = RawDocument.text @@ Document.raw_document document in
-  Vernacstate.unfreeze_full_state init_vs;
-  let document = Document.create_document init_vs.synterp text in
-  ExecutionManager.destroy execution_state;
-  let execution_state, feedback = ExecutionManager.init init_vs in
-  { uri; opts; init_vs; document; execution_state; observe_id = None }, [inject_em_event feedback]
-
 let interpret_to ~stateful ~background state id : (state * event Sel.Event.t list) =
   match Document.get_sentence state.document id with
   | None -> (state, []) (* TODO error? *)
@@ -253,6 +245,15 @@ let init init_vs ~opts uri ~text =
   let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in
   validate_document st, [inject_em_event feedback]
 
+let reset { uri; opts; init_vs; document; execution_state } =
+  let text = RawDocument.text @@ Document.raw_document document in
+  Vernacstate.unfreeze_full_state init_vs;
+  let document = Document.create_document init_vs.synterp text in
+  ExecutionManager.destroy execution_state;
+  let execution_state, feedback = ExecutionManager.init init_vs in
+  let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in
+  validate_document st, [inject_em_event feedback]
+
 let apply_text_edits state edits =
   let document = Document.apply_text_edits state.document edits in
   let shift_diagnostics_locs exec_st (range, new_text) =

language-server/protocol/extProtocol.ml

@@ -153,7 +153,7 @@ module Request = struct
   module ResetParams = struct
 
     type t = {
-      uri : DocumentUri.t;
+      textDocument : TextDocumentIdentifier.t;
     } [@@deriving yojson]
 
   end

language-server/vscoqtop/lspManager.ml

@@ -346,12 +346,18 @@ let textDocumentCompletion id params =
     Error(message), []
 
 let coqtopResetCoq id params =
-  let Request.Client.ResetParams.{ uri } = params in
+  let Request.Client.ResetParams.{ textDocument = { uri } } = params in
   let st = Hashtbl.find states (DocumentUri.to_path uri) in
   let st, events = Dm.DocumentManager.reset st in
+  let (st, events') =
+    if !check_mode = Settings.Mode.Continuous then
+      Dm.DocumentManager.interpret_in_background st
+    else
+      (st, [])
+  in
   Hashtbl.replace states (DocumentUri.to_path uri) st;
   update_view uri st;
-  Ok(()), (uri,events) |> inject_dm_events
+  Ok(()), (uri,events@events') |> inject_dm_events
 
 let coqtopInterpretToEnd params =
   let Notification.Client.InterpretToEndParams.{ textDocument = { uri } } = params in