Add warnings machinery

machinery for non-fatal errors that will be displayed in a separate
emacs window, but not interrupt typechecking.

Currently termination errors, unsolved metas and unsolved constraints
are non-fatal.

Developed together with Guillaume Allais.

doc/release-notes/2-5-2.txt

@@ -358,3 +358,11 @@ Emacs mode
 
     -- used to be:
     -- funField testFunRec x = {!!}
+
+* Non-fatal errors/warnings window.
+
+  Non-fatal errors and warnings are now displayed in their own emacs
+  window and does not interrupt the typechecking of the file.
+
+  Currently termination errors, unsolved metavariables and unsolved
+  constraints are non-fatal errors.

src/data/emacs-mode/agda2-mode.el

@@ -106,6 +106,13 @@ argument, and does not need to be listed here."
   "The name of the Agda toplevel module."
   :type 'string :group 'agda2)
 
+(defcustom agda2-warning-window-max-height
+  0.35
+  "The maximum height of the warning window.
+A multiple of the frame height."
+  :type 'number
+  :group 'agda2)
+
 (defcustom agda2-information-window-max-height
   0.35
   "The maximum height of the information window.
@@ -288,6 +295,9 @@ menus.")
 (defvar agda2-info-buffer nil
   "Agda information buffer.")
 
+(defvar agda2-warning-buffer nil
+  "Agda warnings buffer.")
+
 (defvar agda2-process-buffer nil
   "Agda subprocess buffer.
 Set in `agda2-restart'.")
@@ -891,6 +901,33 @@ Assumes that <clause> = {!<variables>!} is on one line."
 major mode)."
   (setq agda2-buffer-external-status status))
 
+(defun agda2-warning-buffer nil
+  "Creates the Agda warning buffer, if it does not already exist.
+The buffer is returned."
+  (unless (buffer-live-p agda2-warning-buffer)
+    (setq agda2-warning-buffer
+          (generate-new-buffer "*Agda warnings*"))
+
+    (with-current-buffer agda2-warning-buffer
+      (compilation-mode "AgdaInfo")
+      ;; Support for jumping to positions mentioned in the text.
+      (set (make-local-variable 'compilation-error-regexp-alist)
+           '(("\\([\\\\/][^[:space:]]*\\):\\([0-9]+\\),\\([0-9]+\\)-\\(\\([0-9]+\\),\\)?\\([0-9]+\\)"
+              1 (2 . 5) (3 . 6))))
+      ;; No support for recompilation. The key binding is removed, and
+      ;; attempts to run `recompile' will (hopefully) result in an
+      ;; error.
+      (let ((map (copy-keymap (current-local-map))))
+        (define-key map (kbd "g") 'undefined)
+        (use-local-map map))
+      (set (make-local-variable 'compile-command)
+           'agda2-does-not-support-compilation-via-the-compilation-mode)
+
+      (set-syntax-table agda2-mode-syntax-table)
+      (set-input-method "Agda")))
+
+  agda2-warning-buffer)
+
 (defun agda2-info-buffer nil
   "Creates the Agda info buffer, if it does not already exist.
 The buffer is returned."
@@ -996,6 +1033,90 @@ is inserted, and point is placed before this text."
               (goto-char (point-max))
             (goto-char (point-min))))))))
 
+(defun agda2-close-warning nil
+  (interactive)
+  (when (buffer-live-p agda2-warning-buffer)
+        (delete-windows-on agda2-warning-buffer))
+)
+
+(defun agda2-warning-action (name text &optional append)
+  "Insert TEXT into the Agda warning buffer and display it.
+NAME is displayed in the buffer's mode line.
+
+If APPEND is non-nil, then TEXT is appended at the end of the
+buffer, and point placed after this text.
+
+If APPEND is nil, then any previous text is removed before TEXT
+is inserted, and point is placed before this text."
+  (interactive)
+  (let ((buf (agda2-warning-buffer)))
+    (with-current-buffer buf
+      ;; In some cases the jump-to-position-mentioned-in-text
+      ;; functionality (see compilation-error-regexp-alist above)
+      ;; didn't work: Emacs jumped to the wrong position. However, it
+      ;; seems to work if compilation-forget-errors is used. This
+      ;; problem may be related to Emacs bug #9679
+      ;; (http://debbugs.gnu.org/cgi/bugreport.cgi?bug=9679). The idea
+      ;; to use compilation-forget-errors comes from a comment due to
+      ;; Oleksandr Manzyuk
+      ;; (https://github.com/haskell/haskell-mode/issues/67).
+      (compilation-forget-errors)
+      (unless append (erase-buffer))
+      (save-excursion
+        (goto-char (point-max))
+        (insert text))
+      (put-text-property 0 (length name) 'face '(:weight bold) name)
+      (setq mode-line-buffer-identification name)
+      (force-mode-line-update))
+    ;; If the current window displays the information buffer, then the
+    ;; window configuration is left untouched.
+    (unless (equal (window-buffer) buf)
+      (let ((agda-info
+              (and agda2-info-buffer
+                   (car-safe
+                     ;; All windows, including minibuffers, on any
+                     ;; frame on the current terminal, displaying the
+                     ;; present Agda file buffer.
+                    (get-buffer-window-list agda2-info-buffer t 0)))))
+        (save-selected-window
+          ;; Select a window displaying the Agda file buffer (if such
+          ;; a window exists). With certain configurations of
+          ;; display-buffer this should increase the likelihood that
+          ;; the info buffer will be displayed on the same frame.
+          (when agda-info
+            (select-window agda-info 'no-record))
+          (let* (;; The warnings window should be displayed below the
+                 ;; Agda info one
+                 (split-width-threshold nil)
+                 (split-height-threshold 1)
+                 (window
+                   (display-buffer
+                     buf
+                     ;; Under Emacs 23 the effect of the following
+                     ;; argument is only that the current window
+                     ;; should not be used.
+                     '((display-buffer-below-selected)
+                       .
+                       (;; Do not use the same window
+                        (inhibit-same-window . t)
+                        ;; Do not raise or select another frame.
+                        (inhibit-switch-frame . t))))))
+            (if window
+                (fit-window-to-buffer window
+                  (truncate
+                    (* (frame-height)
+                       agda2-warning-window-max-height))))))))
+    ;; Move point in every window displaying the information buffer.
+    ;; Exception: If we are appending, don't move point in selected
+    ;; windows.
+    (dolist (window (get-buffer-window-list buf 'no-minibuffer t))
+      (unless (and append
+                   (equal window (selected-window)))
+        (with-selected-window window
+          (if append
+              (goto-char (point-max))
+            (goto-char (point-min))))))))
+
 (defun agda2-info-action-and-copy (name text &optional append)
   "Same as agda2-info-action but also puts TEXT in the kill ring."
   (kill-new text)

src/full/Agda/Interaction/EmacsCommand.hs

@@ -8,7 +8,9 @@ module Agda.Interaction.EmacsCommand
   , response
   , putResponse
   , display_info'
+  , display_warning
   , clearRunningInfo
+  , clearWarning
   , displayRunningInfo
   ) where
 
@@ -59,19 +61,25 @@ response = (++ "\n") . map replaceNewLines . show . pretty
 putResponse :: Lisp String -> IO ()
 putResponse = putStr . response
 
--- | @display_info' append header content@ displays @content@ (with
--- header @header@) in some suitable way. If @append@ is @True@, then
--- the content is appended to previous content (if any), otherwise any
--- previous content is deleted.
+-- | @displayInBuffer buffername append header content@ displays @content@
+-- (with header @header@) in some suitable way in the buffer @buffername@.
+-- If @append@ is @True@, then the content is appended to previous content
+-- (if any), otherwise any previous content is deleted.
 
-display_info' :: Bool -> String -> String -> Lisp String
-display_info' append bufname content =
-    L [ A "agda2-info-action"
-      , A (quote bufname)
+displayInBuffer :: String -> Bool -> String -> String -> Lisp String
+displayInBuffer buffername append header content =
+    L [ A buffername
+      , A (quote header)
       , A (quote content)
       , A (if append then "t" else "nil")
       ]
 
+display_info' :: Bool -> String -> String -> Lisp String
+display_info' = displayInBuffer "agda2-info-action"
+
+display_warning :: String -> String -> Lisp String
+display_warning = displayInBuffer "agda2-warning-action" False
+
 ------------------------------------------------------------------------
 -- Running info
 
@@ -86,6 +94,10 @@ clearRunningInfo :: Lisp String
 clearRunningInfo =
     display_info' False runningInfoBufferName ""
 
+-- | Clear the warning buffer
+clearWarning :: Lisp String
+clearWarning = L [ A "agda2-close-warning" ]
+
 -- | Display running information about what the type-checker is up to.
 
 displayRunningInfo :: String -> Lisp String

src/full/Agda/Interaction/EmacsTop.hs

@@ -89,7 +89,8 @@ lispifyResponse (Resp_DisplayInfo info) = return $ case info of
     Info_Constraints s -> f s "*Constraints*"
     Info_AllGoals s -> f s "*All Goals*"
     Info_Auto s -> f s "*Auto*"
-    Info_Error s -> f s "*Error*"
+    Info_Error s -> clearWarning : f s "*Error*"
+    Info_Warning s -> [ display_warning "*Errors*" s ]
     Info_Time s -> f (render s) "*Time*"
     Info_NormalForm s -> f (render s) "*Normal Form*"   -- show?
     Info_InferredType s -> f (render s) "*Inferred Type*"
@@ -109,7 +110,7 @@ lispifyResponse (Resp_DisplayInfo info) = return $ case info of
     Info_Version -> f ("Agda version " ++ version) "*Agda Version*"
   where f content bufname = [ display_info' False bufname content ]
 lispifyResponse Resp_ClearHighlighting = return [ L [ A "agda2-highlight-clear" ] ]
-lispifyResponse Resp_ClearRunningInfo = return [ clearRunningInfo ]
+lispifyResponse Resp_ClearRunningInfo = return [ clearRunningInfo, clearWarning ]
 lispifyResponse (Resp_RunningInfo n s)
   | n <= 1    = return [ displayRunningInfo s ]
   | otherwise = return [ L [A "agda2-verbose", A (quote s)] ]

src/full/Agda/Interaction/Highlighting/Generate.hs

@@ -163,6 +163,8 @@ generateAndPrintSyntaxInfo decl hlLevel = do
       Full{} -> generateConstructorInfo modMap file kinds decl
       _      -> return mempty
 
+    warnInfo <- fmap Fold.fold $ fmap warningHighlighting <$> use stWarnings
+
     let (from, to) = case P.rangeToInterval (P.getRange decl) of
           Nothing -> __IMPOSSIBLE__
           Just i  -> ( fromIntegral $ P.posPos $ P.iStart i
@@ -179,6 +181,7 @@ generateAndPrintSyntaxInfo decl hlLevel = do
     let syntaxInfo = compress (mconcat [ constructorInfo
                                        , theRest modMap file
                                        , nameInfo
+                                       , warnInfo
                                        ])
                        `mappend`
                      curTokens
@@ -521,6 +524,14 @@ errorHighlighting e = do
                   }
   return $ mconcat [ erase, error ]
 
+-- | Generate syntax highlighting for warnings.
+
+warningHighlighting :: Warning -> File
+warningHighlighting w = case w of
+  TerminationIssue tcst terrs -> terminationErrorHighlighting $ clValue terrs
+  _ -> mempty
+
+
 -- | Generate syntax highlighting for termination errors.
 
 terminationErrorHighlighting :: [TerminationError] -> File

src/full/Agda/Interaction/Imports.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP           #-}
+{-# LANGUAGE DeriveFunctor #-}
 
 {-| This module deals with finding imported modules and loading their
     interface files.
@@ -144,11 +145,18 @@ scopeCheckImport x = do
     let s = iScope i
     return (iModuleName i `withRangesOfQ` mnameToConcrete x, s)
 
-data MaybeWarnings = NoWarnings | SomeWarnings Warnings
+data MaybeWarnings' a = NoWarnings | SomeWarnings a
+  deriving (Functor)
+type MaybeWarnings = MaybeWarnings' [Warning]
+
+instance Null a => Null (MaybeWarnings' a) where
+  empty = NoWarnings
+  null mws = case mws of
+    NoWarnings      -> True
+    SomeWarnings ws -> null ws
 
 hasWarnings :: MaybeWarnings -> Bool
-hasWarnings NoWarnings     = False
-hasWarnings SomeWarnings{} = True
+hasWarnings = not . null
 
 -- | If the module has already been visited (without warnings), then
 -- its interface is returned directly. Otherwise the computation is
@@ -378,7 +386,9 @@ getInterface' x isMain = do
           unless includeStateChanges cleanCachedLog
           let withMsgs = bracket_
                 (chaseMsg "Checking" $ Just $ filePath file)
-                (const $ chaseMsg "Finished" Nothing)
+                (const $ do
+                   ws <- getAllWarnings RespectFlags
+                   unless (hasWarnings ws) $ chaseMsg "Finished" Nothing)
 
           -- Do the type checking.
 
@@ -659,23 +669,19 @@ createInterface file mname =
     unless (null openMetas) $ do
       reportSLn "import.metas" 10 "We have unsolved metas."
       reportSLn "import.metas" 10 . unlines =<< showOpenMetas
-    unsolvedMetas       <- List.nub <$> mapM getMetaRange openMetas
-    unsolvedConstraints <- getAllConstraints
-    interactionPoints   <- getInteractionPoints
+    mallWarnings <- getAllWarnings IgnoreFlags
 
     ifTopLevelAndHighlightingLevelIs NonInteractive $
       printUnsolvedInfo
 
     reportSLn "import.iface.create" 7 $ "Starting writing to interface file."
-    warn <- if and [ null unsolvedMetas, null unsolvedConstraints, null interactionPoints ]
-     then Bench.billTo [Bench.Serialization] $ do
-      -- The file was successfully type-checked (and no warnings were
-      -- encountered), so the interface should be written out.
-      let ifile = filePath $ toIFile file
-      writeInterface ifile i
-      return NoWarnings
-     else do
-      return $ SomeWarnings $ Warnings unsolvedMetas unsolvedConstraints
+    case mallWarnings of
+      SomeWarnings allWarnings -> return ()
+      NoWarnings               -> Bench.billTo [Bench.Serialization] $ do
+        -- The file was successfully type-checked (and no warnings were
+        -- encountered), so the interface should be written out.
+        let ifile = filePath $ toIFile file
+        writeInterface ifile i
     reportSLn "import.iface.create" 7 $ "Finished writing to interface file."
 
     -- Profiling: Print statistics.
@@ -688,7 +694,34 @@ createInterface file mname =
     verboseS "profile" 1 $ do
       reportSLn "import.iface" 5 $ "Accumulated statistics."
 
-    return (constructIScope i, warn)
+    return $ first constructIScope (i, mallWarnings)
+
+-- | Collect all warnings that have accumulated in the state.
+-- Depending on the argument, we either respect the flags passed
+-- in by the user, or not (for instance when deciding if we are
+-- writing an interface file or not)
+
+getAllWarnings :: IgnoreFlags -> TCM MaybeWarnings
+getAllWarnings ifs = do
+  openMetas            <- getOpenMetas
+  interactionMetas     <- getInteractionMetas
+  unsolvedInteractions <- List.nub <$> mapM getMetaRange interactionMetas
+  unsolvedMetas        <- List.nub <$> mapM getMetaRange (openMetas List.\\ interactionMetas)
+  unsolvedConstraints  <- getAllConstraints
+  collectedWarnings    <- use stWarnings
+  interactionPoints    <- getInteractionPoints
+  tcst                 <- get
+
+  allWarnings <- applyFlagsToWarnings ifs $ reverse
+               $ UnsolvedInteractionMetas unsolvedInteractions
+               : UnsolvedMetaVariables    unsolvedMetas
+               : UnsolvedConstraints      tcst unsolvedConstraints
+               : collectedWarnings
+
+  return $ if and [ null allWarnings, null interactionPoints ]
+           then NoWarnings
+           else SomeWarnings allWarnings
+
 
 -- constructIScope :: ScopeInfo -> Map ModuleName Scope
 constructIScope :: Interface -> Interface