Merge pull request #177 from corwin-of-amber/v8.11+error-focus

More accurate location of error indicator

CHANGES.md

@@ -21,6 +21,7 @@
  - Accept dropped `.coq-pkg` files as packages to add to the current
    session (@corwin-of-amber)
  - Allow multiple directories for package files (@corwin-of-amber)
+ - More accurate error location marker (@corwin-of-amber)
 
 # JsCoq 0.10 "((())((()()(()))((()()))))"
 -----------------------------------------

ui-css/coq-base.css

@@ -105,6 +105,12 @@ body.jscoq-main .CodeMirror-linenumber {
   box-sizing: content-box;  /* need to override `jscoq-main > *` */
 }
 
+.coq-squiggle {
+  background-image: url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAQAAAACCAYAAAB/qH1jAAAABmJLR0QA/wD/AP+gvaeTAAAACXBIWXMAAAsTAAALEwEAmpwYAAAAB3RJTUUH3QUXCToH00Y1UgAAACFJREFUCNdjPMDBUc/AwNDAAAFMTAwMDA0OP34wQgX/AQBYgwYEx4f9lQAAAABJRU5ErkJggg==);
+  background-repeat: repeat-x;
+  background-position: bottom;
+}
+
 /*
  * This is here for the time interval between document load and creation of
  * the CodeMirror editors from textareas.

ui-css/coq-dark.css

@@ -84,15 +84,15 @@
 }
 
 .cm-s-blackboard .coq-eval-ok {
-  background: #483D8B;
+  background-color: #483D8B;
 }
 
 .cm-s-blackboard .coq-eval-pending {
-  background: #94763a;
+  background-color: #94763a;
 }
 
 .cm-s-blackboard .coq-eval-failed {
-  background: #aa0000;
+  background-color: #aa0000;
 }
 
 /* Gallina keywords */

ui-css/coq-light.css

@@ -52,29 +52,29 @@ body.jscoq-main #document {
 /* Coq settings */
 
 .coq-eval-ok {
-  background: #ddd;
+  background-color: #ddd;
 }
 
 .coq-eval-ok.coq-highlight {
-  background: #ebeebd;
+  background-color: #ebeebd;
 }
   
 .coq-eval-pending {
-    background: #fc6;
+  background-color: #fc6;
 }
 
 .coq-eval-failed {
-    background: rgba(255, 00, 50, 0.4);
+  background-color: rgba(255, 00, 50, 0.2);
 }
 
 .coq-eval-ok.CodeMirror-selectedtext,
 .coq-eval-pending.CodeMirror-selectedtext,
 .coq-eval-failed.CodeMirror-selectedtext {
-    background: none;
+  background-color: none;
 }
 
 .coq-eval-ok.coq-highlight.CodeMirror-selectedtext {
-    background: #bbe; 
+  background-color: #bbe; 
 }
 
 

ui-js/cm-provider.js

@@ -164,7 +164,7 @@ class CmCoqProvider {
     }
 
     // Mark a sentence with {clear, processing, error, ok}
-    mark(stm, mark_type) {
+    mark(stm, mark_type, loc_focus) {
 
         if (stm.mark) {
             let b = stm.mark.find();
@@ -184,14 +184,16 @@ class CmCoqProvider {
             break;
         case "error":
             this.markWithClass(stm, 'coq-eval-failed');
-            // XXX: Check this is the right place.
+            if (loc_focus) {
+                let foc = this.squiggle(stm, loc_focus, 'coq-squiggle');
+                this.editor.setCursor(foc.find().to);
+            }
+            else {
                 this.editor.setCursor(stm.end);
+            }
             break;
         case "ok":
             this.markWithClass(stm, 'coq-eval-ok');
-            // XXX: Check this is the right place.
-            // This interferes with the go to target.
-            // doc.setCursor(stm.end);
             break;
         }
     }
@@ -211,6 +213,10 @@ class CmCoqProvider {
         }
     }
 
+    squiggle(stm, loc, className) {
+        return this.markSubordinate(stm, this._subregion(stm, loc), className);
+    }
+
     /**
      * Removes all sentence marks
      */
@@ -223,18 +229,40 @@ class CmCoqProvider {
     }
 
     markWithClass(stm, className) {
-        var doc = this.editor.getDoc();
+        var doc = this.editor.getDoc(),
+            {start, end} = stm;
 
         var mark = 
-            doc.markText(stm.start, stm.end, {className: className,
+            doc.markText(start, end, {className: className,
                 attributes: {'data-coq-sid': stm.coq_sid}});
 
-        this._markWidgetsAsWell(stm.start, stm.end, mark);
+        this._markWidgetsAsWell(start, end, mark);
 
         mark.stm = stm;
         stm.mark = mark;
     }
 
+    markSubordinate(stm, pos, className) {
+        var doc = this.editor.getDoc(),
+            {start, end} = pos;
+
+        var mark = 
+            doc.markText(start, end, {className: className});
+
+        this._markWidgetsAsWell(start, end, mark);
+
+        stm.mark.on('clear', () => mark.clear());
+        return mark;
+    }
+
+    _subregion(stm, loc) {
+        var doc = this.editor.getDoc(),
+            idx = doc.indexFromPos(stm.start);
+
+        return {start: doc.posFromIndex(idx + loc.bp),
+                end:   doc.posFromIndex(idx + loc.ep)}
+    }
+
     /**
      * Hack to apply MarkedSpan CSS class formatting and attributes to widgets
      * within mark boundaries as well. 

ui-js/coq-manager.js

@@ -162,8 +162,8 @@ class ProviderContainer {
         }
     }
 
-    mark(stm, mark) {
-        stm.sp.mark(stm, mark);
+    mark(stm, mark, loc_focus) {
+        stm.sp.mark(stm, mark, loc_focus);
     }
 
     highlight(stm, flag) {
@@ -626,18 +626,19 @@ class CoqManager {
 
     coqLog(level, msg) {
 
-        let rmsg = this.pprint.pp2HTML(msg);
+        let fmsg = this.pprint.pp2DOM(msg);
 
         level = level[0];
 
         if (this.options.debug) {
             if (level === 'Debug')
-                console.debug(rmsg, level)
+                console.debug(fmsg, level)
             else
-                console.log(rmsg, level);
+                console.log(fmsg, level);
         }
 
-        this.layout.log(rmsg, level);
+        var item = this.layout.log(fmsg, level);
+        this.pprint.adjustBreaks(item);
     }
 
     coqLibInfo(bname, bi) {
@@ -663,8 +664,10 @@ class CoqManager {
         if (this.error.some(stm => stm.feedback.some(x => x.msg.equals(msg))))
             return;
 
-        var rmsg = this.pprint.pp2HTML(msg);
-        this.layout.log(rmsg, 'Error');
+        var fmsg = this.pprint.pp2DOM(msg);
+
+        var item = this.layout.log(fmsg, 'Error', {'data-coq-sid': sids[0]});
+        this.pprint.adjustBreaks(item);
     }
 
     coqJsonExn(msg) {
@@ -918,7 +921,7 @@ class CoqManager {
         err_stm.phase = Phases.ERROR;
         this.error.push(err_stm);
 
-        this.provider.mark(err_stm, 'error');
+        this.provider.mark(err_stm, 'error', loc);
 
         this.truncate(err_stm);
         this.coq.cancel(sid);