Error highlighting

bin/narya.ml

@@ -163,16 +163,31 @@ let interact () =
           let* () = LTerm_history.save history history_file in
           Lwt.fail exn)
 
+let rec print_error_locs (d : Reporter.Code.t Asai.Diagnostic.t) =
+  match d.message with
+  | Accumulated (_name, msgs) -> Mbwd.miter (fun [ e ] -> print_error_locs e) [ msgs ]
+  | _ -> (
+      match d.explanation.loc with
+      | Some loc -> (
+          match Asai.Range.view loc with
+          | `Range (s, e) -> Format.printf "%d %d\n" s.offset e.offset
+          | `End_of_file p -> Format.printf "%d\n" p.offset)
+      | None -> ())
+
 (* In ProofGeneral interaction mode, the prompt is delimited by formfeeds, and commands are ended by a formfeed on a line by itself.  This prevents any possibility of collision with other input or output.  This doesn't require initialization. *)
 let rec interact_pg () : unit =
   Format.printf "\x0C[narya]\x0C\n%!";
   try
     let buf = Buffer.create 20 in
+    let atstart = ref true in
     let str = ref "" in
     while !str <> "\x0C\n" do
       Buffer.add_string buf !str;
       let line = read_line () in
-      str := if String.length line > 0 then line ^ "\n" else ""
+      (* Sometimes the command we get has a blank line at the beginning and sometimes it doesn't.  I don't understand why. *)
+      if (not !atstart) || line <> "" then (
+        str := line ^ "\n";
+        atstart := false)
     done;
     let cmd = Buffer.contents buf in
     let holes = ref Emp in
@@ -184,7 +199,10 @@ let rec interact_pg () : unit =
           match d.message with
           | Hole _ -> holes := Snoc (!holes, d.message)
           | _ -> Reporter.display ~use_ansi:true ~output:stdout d)
-        ~fatal:(fun d -> Reporter.display ~use_ansi:true ~output:stdout d)
+        ~fatal:(fun d ->
+          Reporter.display ~use_ansi:true ~output:stdout d;
+          Format.printf "\x0C[errors]\x0C\n%!";
+          print_error_locs d)
         (fun () ->
           try
             match Command.parse_single cmd with

proofgeneral/narya.el

@@ -177,7 +177,40 @@ Some code copied from Coq."
               (with-selected-window goal-win
                 (goto-char (point-max))
                 (recenter (- 1)))))))))
+
+(defface narya-error-face
+  '((t (:background "red1" :foreground "white" :weight bold)))
+  "Face used to highlight script errors in Narya."
+  :group 'narya)
+
+(defvar narya-error-overlays nil
+  "List of overlays for error highlighting.")
+
+(defun narya-highlight-error-range (start-byte end-byte)
+  "Highlight the byte range START-BYTE to END-BYTE in the script buffer."
+  (let ((start (byte-to-position start-byte))
+        (end (byte-to-position end-byte)))
+    (when (and start end)
+      (let ((ovl (make-overlay start end)))
+        (overlay-put ovl 'face 'narya-error-face)
+        (push ovl narya-error-overlays)))))
+
+(defun narya-clear-error-highlights ()
+  "Remove all current error overlays."
+  (mapc #'delete-overlay narya-error-overlays)
+  (setq narya-error-overlays nil))
 
+(add-hook 'proof-shell-pre-send-hook 'narya-clear-error-highlights)
+
+(defun narya-clear-error-highlights-on-edit (start end length)
+  "Remove all error overlays when the buffer is edited."
+  (narya-clear-error-highlights))  
+
+(add-hook 'after-change-functions 'narya-clear-error-highlights-on-edit)
+
+(defvar narya-last-successful-span nil
+  "Stores the last successful span.")
+
 (defun narya-handle-output (cmd string)
   "Parse and handle Narya's output.
 If called with an invisible command (such as 'solve'), store hole data
@@ -197,10 +230,28 @@ handling in Proof General."
         (parsed-hole-data nil)
         (error-found nil)
         (reformatted nil))
+    (when (and span (overlay-buffer span))
+    ;; Store the span
+    (setq narya-last-successful-span span))
     ;; Check for errors in the output first.
-    (when (string-match proof-shell-error-regexp string)
-      (setq error-found t
-            proof-shell-last-output-kind 'error))
+    (when (and (string-match proof-shell-error-regexp string))
+        (setq error-found t
+              proof-shell-last-output-kind 'error)
+        (setq span narya-last-successful-span)
+        (proof-with-script-buffer
+   	;; Start parsing the error numbers after the initial "^L[errors]^L" part
+        (let ((error-start (string-match "\f\\[errors\\]\f\n" string)))
+           ;; Parse all the error pairs (start-byte, end-byte)
+           (while (string-match "\\([0-9]+\\) \\([0-9]+\\)" string)
+              (let ((start-byte (string-to-number (match-string 1 string)))
+                    (end-byte (string-to-number (match-string 2 string))))
+              ;; Highlight the positions on the current line
+              (if (and span (overlay-buffer span) (overlay-end span)) 
+                  (narya-highlight-error-range (+ (overlay-end span) 1 start-byte) 
+                                               (+ (overlay-end span) 1 end-byte))
+                  (narya-highlight-error-range (+ 1 start-byte) (+ 1 end-byte)))
+              ;; Move forward in the string to look for the next error pair
+              (setq string (substring string (match-end 0))))))))
     ;; If no errors, proceed with normal processing.
     (unless error-found
       ;; Check for the goals marker in the output, setting positions to slice