[ui] Support Markdown preview and live editor hot-swap

backend/common/jscoq_interp.ml

@@ -100,13 +100,21 @@ let mk_vo_path l = Jslib.paths_to_coqpath ~implicit:!opts.implicit_libs l
 let cur_workspace = ref None
 let root_state = ref (Coq.State.of_coq (Vernacstate.freeze_interp_state ~marshallable:false))
 
+let lvl_to_fb = function
+  | 0 -> Feedback.Error
+  | 1 -> Feedback.Warning
+  | 2 -> Feedback.Notice
+  | 3 -> Feedback.Info
+  | 4 -> Feedback.Debug
+  | _ -> Feedback.Debug
+
 let lsp_cb =
   let out_fn = post_answer in
   Fleche.Io.CallBack.
     { trace = (fun cat ?extra:_ msg -> Format.eprintf "[%s] %s@\n%!" cat msg)
-    ; message = (fun ~lvl:_ ~message:_ -> ())
-    ; diagnostics = (fun ~uri:_ ~version diags ->
-          out_fn (Notification (diags,version)))
+    ; message = (fun ~lvl ~message -> out_fn (Log (lvl_to_fb lvl, Pp.str message)))
+    ; diagnostics = (fun ~uri ~version diagnostic ->
+          out_fn (Notification { uri; version; diagnostic }))
     ; fileProgress = (fun ~uri:_ ~version:_ _progress -> ())
     }
 
@@ -180,16 +188,16 @@ let jscoq_execute =
     try_check ();
     ()
 
-  | Request { uri; method_ } ->
-    let { Request.id; loc = _; v = _ } = method_ in
+  | Request { id; method_ } ->
+    let { Request.uri; loc = _; v = _ } = method_ in
     (* XXX Fix to use position *)
     let r = Fleche.Theory.Request.{ id; request = FullDoc { uri } } in
     (* XXX Fix to postpone requests *)
     let () = match Fleche.Theory.Request.add r with
       | Now doc ->
-        let f = Request_interp.do_request ~doc in
+        let f _uri = Request_interp.do_request ~doc in
         let res = Request.process ~f method_ in
-        out_fn (Response res)
+        out_fn (Response { id; res })
       | Postpone -> ()
       | Cancel -> () in
     try_check ()

backend/common/jscoq_proto.ml

@@ -163,24 +163,24 @@ let opaque_of_yojson _x = Result.Error "opaque value"
 module Request = struct
 
   type 'a t =
-    { id : int
+    { uri : Lang.LUri.File.t
     ; loc : int
     (* In fact, we should use Lsp.Base.point instead of int for
        location, however ProseMirror and CM6 use offsets *)
     ; v : 'a
     }
   [@@deriving yojson]
 
-  let make ~id ~loc v = { id; loc; v }
+  let make ~uri ~loc v = { uri; loc; v }
 
   type 'a answer =
     { id : int
     ; res : 'a
     }
   [@@deriving yojson]
 
-  let process { id; loc; v } ~f =
-    { id; res = f loc v }
+  let process { uri; loc; v } ~f =
+    f uri loc v
 
 end
 
@@ -190,7 +190,7 @@ type jscoq_cmd =
   | NewDoc  of { uri : Lang.LUri.File.t; version : int; raw : string }
   | Update  of { uri : Lang.LUri.File.t; version : int; raw : string }
 
-  | Request of { uri : Lang.LUri.File.t; method_ : Method.t Request.t [@key "method"]}
+  | Request of { id: int; method_ : Method.t Request.t [@key "method"] }
 
   | InfoPkg of string * string list
   | LoadPkg of string * string
@@ -204,7 +204,8 @@ type jscoq_cmd =
 type jscoq_answer =
   | CoqInfo   of string
   | Ready     of unit
-  | Notification of Lang.Diagnostic.t list * int
+  | Notification of { uri: Lang.LUri.File.t; version: int; diagnostic: Lang.Diagnostic.t list }
+  (** LSP-compatible payload for diagnostics *)
   | Response  of Answer.t Request.answer
   | Log       of Feedback.level * Pp.t
   | JsonExn   of string

backend/coq-worker.ts

@@ -26,6 +26,12 @@ export interface Diagnostic {
     extra?: any[]
 }
 
+export interface PublishDiagnosticParams {
+    uri: string,
+    version: number,
+    diagnostic: Diagnostic[]
+}
+
 export interface CoqInitOptions {
   implicit_libs?: boolean,
   coq_options?: [string[], any[]][],
@@ -243,7 +249,7 @@ export class CoqWorker {
     sendRequest(uri: string, loc: number, req: object) {
         let id = this.request_nextid++,
             fut = this.request_pending[id] = new Future;
-        this.sendCommand(["Request", { uri, method: {id, loc, v: req} }]);
+        this.sendCommand(["Request", { id, method: {uri, loc, v: req} }]);
         /** @todo would be desirable to interrupt a previously started document re-check. */
         /**   unfortunately this interrupts the new request as well! so yeah, */
         /**   this woudl involve some backend work  */

frontend/classic/css/coq-base.css

@@ -515,6 +515,9 @@ body.jscoq-main .CodeMirror-linenumber {
 #buttons button[name=reset] {
   background-image: url(../images/reset.png);
 }
+#buttons button[name=editor] {
+  background-image: url(../images/editor.png);
+}
 
 
 /* Proper  */

frontend/classic/js/cm-provider-container.ts

@@ -1,3 +1,4 @@
+import CodeMirror from "codemirror";
 import { Future } from "../../../backend/future";
 import { CmCoqProvider } from './cm-provider';
 import { CoqManager, ManagerOptions } from "./coq-manager";
@@ -23,12 +24,11 @@ export class ProviderContainer {
     onAction : (evt : any ) => void;
     wait_for : Future<void>;
     currentFocus : CmCoqProvider;
-    manager : any;
 
     /**
      * Creates an instance of ProviderContainer.
      */
-    constructor(elementRefs : (string | HTMLElement)[], options : ManagerOptions, manager : CoqManager) {
+    constructor(elementRefs : (string | HTMLElement)[], options : ManagerOptions) {
 
         this.options = options;
 
@@ -81,15 +81,14 @@ export class ProviderContainer {
                     element = Deprettify.trim(element);
 
                 // Init.
-                let cm = new CmCoqProvider(element, this.options.editor, this.options.replace, idx, manager);
+                let cm = new CmCoqProvider(element, this.options.editor, this.options.replace, idx);
 
                 this.snippets.push(cm);
 
                 // Track focus XXX (make generic)
                 cm.editor.on('focus', ev => { this.currentFocus = cm; });
 
                 // Track invalidate
-                cm.onChange     = (cm, evt) => { this.onChangeAny(cm, evt); };
                 cm.onInvalidate = (stm)     => { this.onInvalidate(stm); };
                 cm.onMouseEnter = (stm, ev) => { this.onMouseEnter(stm, ev); };
                 cm.onMouseLeave = (stm, ev) => { this.onMouseLeave(stm, ev); };
@@ -98,7 +97,7 @@ export class ProviderContainer {
                 cm.onTipOut   = (cm)            => { this.onTipOut(cm); }
 
                 cm.onAction = (action) => { this.onAction({...action, snippet: cm}); };
-                cm.onChange = (cm, evt) => { this.onChangeAny(cm,evt); };
+                cm.onChange = (cm, evt) => { this.onChangeAny(cm, evt); };
                 cm.onCursorUpdate = (cm) => { this.onCursorUpdate(cm); };
                 // Running line numbers
                 if (this.options.line_numbers === 'continue') {
@@ -159,6 +158,15 @@ export class ProviderContainer {
             snippet.configure(options);
     }
 
+    destroy() {
+        for (let snippet of this.snippets) {
+            snippet.editor.setOption("mode", "text/x-csrc");
+            snippet.editor.getWrapperElement().parentNode.
+                removeChild(snippet.editor.getWrapperElement());
+            snippet.editor = null;
+        }
+    }
+
     retract() {
         for (let sp of this.snippets) sp.retract();
     }

frontend/classic/js/cm-provider.ts

@@ -140,11 +140,14 @@ export class CmCoqProvider {
      * @param {number} idx index of this snippet within a ProviderContainer
      * @memberof CmCoqProvider
      */
-    constructor(element: HTMLElement, options : CM5Options, replace : boolean, idx: number, manager: CoqManager) {
+// <<<<<<< HEAD
+/*    constructor(element: HTMLElement, options : CM5Options, replace : boolean, idx: number, manager: CoqManager) {
 
         this.options = options;
         this.idx = idx;
         this.manager = manager;
+*/
+    constructor(element, options : CM5Options, replace : boolean, idx : number) {
 
         CmCoqProvider._config();
 
@@ -164,6 +167,8 @@ export class CmCoqProvider {
 
         copyOptions(options, cmOpts);
 
+        // We test for :hidden custom attribute, as to assume less shared attribute
+        // state, this is useful when replacing editors.
         var makeHidden = $(element).is(':hidden') ||
             /* corner case: a div with a single hidden child is considered hidden */
             element.children.length == 1 && $(element.children[0]).is(':hidden');
@@ -172,6 +177,7 @@ export class CmCoqProvider {
             assert(element instanceof HTMLTextAreaElement);
             /* workaround: `value` sometimes gets messed up after forward/backwarn nav in Chrome */
             element.value ||= element.textContent;
+            /** @todo desirable, but causes a lot of errors: @ type {CodeMirror.Editor} */
             this.editor = CodeMirror.fromTextArea(element, cmOpts);
             replace = true;
         } else {
@@ -198,6 +204,7 @@ export class CmCoqProvider {
 
         this.editor.on('beforeChange', (cm, evt) => this.onCMChange(cm, evt) );
         this.editor.on('change', (cm, evt) => this.onChange(cm, evt));
+
         this.editor.on('cursorActivity', (cm) => {
             this.onCursorUpdate(cm);
             cm.operation(() => this._adjustWidgetsInSelection())
@@ -209,7 +216,9 @@ export class CmCoqProvider {
         var editor_element = $(this.editor.getWrapperElement());
         editor_element.on('mousemove', ev => this.onCMMouseMove(ev));
         editor_element.on('mouseleave', ev => this.onCMMouseLeave(ev));
-        if (makeHidden && !editor_element.is(':hidden'))
+
+        // EJGA: Don't make hidden editors for now
+        if (false && makeHidden && !editor_element.is(':hidden'))
             editor_element.css({display: "none"});
 
         // Some hack to prevent CodeMirror from consuming PageUp/PageDn

frontend/classic/js/coq-editor-cm5.ts

@@ -4,7 +4,7 @@
 // CodeMirror implementation
 import { Diagnostic } from '../../../backend';
 import { ProviderContainer } from './cm-provider-container';
-import { CoqManager, ManagerOptions } from './coq-manager';
+import { CoqDocument, ManagerOptions } from './coq-manager';
 import { ICoqEditor } from './coq-editor';
 
 interface CM5Options {
@@ -17,16 +17,16 @@ interface CM5Options {
 /** Interface for CM5 */
 export class CoqCodeMirror5 extends ProviderContainer implements ICoqEditor {
 
-    constructor(eIds: (string | HTMLElement)[], options : ManagerOptions, onChange, onCursorUpdate, manager : CoqManager) {
+    constructor(doc: CoqDocument, options : ManagerOptions) {
 
-        super(eIds, options, manager);
+        super([doc.area], options);
 
         this.onChangeAny = () => {
             let txt = this.getValue();
-            onChange(txt);
+            doc.change(txt);
         };
         this.onCursorUpdate = (cm) => {
-            onCursorUpdate(this.getCursorOffset());
+            doc.updateCursor(this.getCursorOffset());
         }
         // if (this.options.mode && this.options.mode['company-coq']) {
         //     this.company_coq = new CompanyCoq(this.manager);

frontend/classic/js/coq-editor-cm6.ts

@@ -3,6 +3,7 @@ import { EditorState, RangeSet, Facet, StateEffect, StateField } from "@codemirr
 import { EditorView, lineNumbers, Decoration, ViewPlugin } from "@codemirror/view";
 import { Diagnostic } from "../../../backend/coq-worker";
 import { ICoqEditor, editorAppend } from "./coq-editor";
+import { CoqDocument } from "./coq-manager";
 
 // import './mode/coq-mode.js';
 
@@ -39,32 +40,29 @@ export class CoqCodeMirror6 implements ICoqEditor {
     private view : EditorView;
 
     // element e
-    constructor(eIds : string[], options, onChange, onCursorUpdated, manager) {
-        if (eIds.length != 1)
-            throw new Error('not implemented: `cm6` frontend requires a single element')
-
-        let { container, area }  = editorAppend(eIds[0]);
+    constructor(doc: CoqDocument, options) {
 
         var extensions =
-            [ diagField,
-              lineNumbers(),
-              EditorView.updateListener.of(v => {
-                  if(v.selectionSet) {
-                    onCursorUpdated(v.state.selection.main.head);
-                  }
-                  if (v.docChanged) {
-                      // Document changed
-                      var newText = v.state.doc.toString();
-                      area.value = newText;
-                      onChange(newText);
-                  }})
+            [diagField,
+                lineNumbers(),
+                EditorView.updateListener.of(v => {
+                    if (v.docChanged) {
+                        // Document changed
+                        var newText = v.state.doc.toString();
+                        doc.change(newText);
+                    }
+                    // Careful to run this _after_ doc is changed in the model
+                    if (v.selectionSet) {
+                        doc.updateCursor(v.state.selection.main.head);
+                    }
+                })
             ];
 
-        var state = EditorState.create( { doc: area.value, extensions } );
+        var state = EditorState.create( { doc: doc.getValue(), extensions } );
 
         this.view = new EditorView(
             { state,
-              parent: container,
+              parent: doc.container,
               extensions
             });
     }
@@ -102,6 +100,9 @@ export class CoqCodeMirror6 implements ICoqEditor {
         return this.view.state.selection.main.head;
     }
 
+    destroy() {
+        this.view.destroy();
+    }
     configure() {}
     openFile() {}
     focus() {}

frontend/classic/js/coq-editor-pm.ts

@@ -12,7 +12,7 @@ import 'prosemirror-menu/style/menu.css';
 import 'prosemirror-example-setup/style/style.css';
 import { Diagnostic } from '../../../backend';
 import { ICoqEditor, editorAppend } from './coq-editor';
-import { CoqManager, ManagerOptions } from './coq-manager';
+import { CoqDocument, ManagerOptions } from './coq-manager';
 
 function diagNew(d : Diagnostic) {
     var mark_class = (d.severity === 1) ? 'coq-eval-failed' : 'coq-eval-ok';
@@ -63,31 +63,28 @@ export class CoqProseMirror implements ICoqEditor {
     view : EditorView;
 
     // eId must be a textarea
-    constructor(eIds, options: ManagerOptions, onChange, onCursorUpdated, manager: CoqManager) {
+    constructor(doc : CoqDocument, options: ManagerOptions) {
 
-        let { container, area } = editorAppend(eIds[0]);
-
-        var doc = defaultMarkdownParser.parse(area.value);
+        var text = defaultMarkdownParser.parse(doc.getValue());
 
         this.view =
-            new EditorView(container, {
+            new EditorView(doc.container, {
                 state: EditorState.create({
-                    doc: doc || undefined,
+                    doc: text || undefined,
                     plugins: [...exampleSetup({schema: schema}), coqDiags]
                 }),
                 // We update the text area
                 dispatchTransaction(tr) {
                     // Update textarea only if content has changed
                     if (tr.docChanged) {
                         let newDoc = CoqProseMirror.serializeDoc(tr.doc);
-                        onChange(newDoc);
                         var newMarkdown = defaultMarkdownSerializer.serialize(tr.doc);
-                        area.value = newMarkdown;
+                        doc.changeSpecial(newDoc, newMarkdown);
                     }
                     const { state } = this.state.applyTransaction(tr);
 
                     if(tr.selectionSet) {
-                        onCursorUpdated(state.selection.head);
+                        doc.updateCursor(state.selection.head);
                     }
 
                     this.updateState(state);
@@ -129,6 +126,10 @@ export class CoqProseMirror implements ICoqEditor {
         return this.view.state.selection.head;
     }
 
+    destroy() {
+        this.view.destroy();
+    }
+
     configure() {}
     openFile() {}
     focus() {}