From faf1a62ed5b12d132a090129af9dd9448723584c Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 12 Nov 2025 19:38:14 +0100
Subject: [PATCH 01/14] Implement sub-diagnostics

---
 .../tools/dotc/reporting/Diagnostic.scala     | 20 +++++++-
 .../dotc/reporting/MessageRendering.scala     | 50 +++++++++++++------
 2 files changed, 54 insertions(+), 16 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
index a4c30b4658e9..90b841a1adcb 100644
--- a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
@@ -11,6 +11,8 @@ import dotty.tools.dotc.util.chaining.*
 import java.util.{Collections, Optional, List => JList}
 import core.Decorators.toMessage
 
+import collection.mutable.ArrayBuffer
+
 object Diagnostic:
 
   def shouldExplain(dia: Diagnostic)(using Context): Boolean =
@@ -117,6 +119,22 @@ class Diagnostic(
     msg.message.replaceAll("\u001B\\[[;\\d]*m", "")
   override def diagnosticRelatedInformation: JList[interfaces.DiagnosticRelatedInformation] =
     Collections.emptyList()
-
   override def toString: String = s"$getClass at $pos L${pos.line+1}: $message"
+
+  private val subdiags: ArrayBuffer[Subdiagnostic] = ArrayBuffer.empty
+
+  def addSubdiag(diag: Subdiagnostic): Unit =
+    subdiags += diag
+
+  def addSubdiag(msg: Message, pos: SourcePosition): Unit =
+    addSubdiag(Subdiagnostic(msg, pos))
+
+  def withSubdiags(diags: List[Subdiagnostic]): this.type =
+    diags.foreach(addSubdiag)
+    this
+
+  def getSubdiags: List[Subdiagnostic] = subdiags.toList
 end Diagnostic
+
+class Subdiagnostic(val msg: Message, val pos: SourcePosition)
+
diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
index 9366050a5a17..68b4b74089f2 100644
--- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
@@ -77,10 +77,11 @@ trait MessageRendering {
    *  -- Error: source.scala ---------------------
    *  ```
    */
-  private def boxTitle(title: String)(using Context, Level, Offset): String =
+  private def boxTitle(title: String, isSubtitle: Boolean = false)(using Context, Level, Offset): String =
     val pageWidth = ctx.settings.pageWidth.value
     val line = "-" * (pageWidth - title.length - 4)
-    hl(s"-- $title $line")
+    val starter = if isSubtitle then ".." else "--"
+    hl(s"$starter $title $line")
 
   /** The position markers aligned under the error
    *
@@ -169,7 +170,8 @@ trait MessageRendering {
   private def posStr(
     pos: SourcePosition,
     message: Message,
-    diagnosticString: String
+    diagnosticString: String,
+    isSubdiag: Boolean = false
   )(using Context, Level, Offset): String =
     assert(
       message.errorId.isActive,
@@ -191,7 +193,7 @@ trait MessageRendering {
         val title =
           if fileAndPos.isEmpty then s"$errId$kind:" // this happens in dotty.tools.repl.ScriptedTests // TODO add name of source or remove `:` (and update test files)
           else s"$errId$kind: $fileAndPos"
-        boxTitle(title)
+        boxTitle(title, isSubtitle = isSubdiag)
       })
     else ""
   end posStr
@@ -232,6 +234,18 @@ trait MessageRendering {
     if origin.nonEmpty then
       addHelp("origin=")(origin)
 
+  // adjust a pos at EOF if preceded by newline
+  private def adjust(pos: SourcePosition): SourcePosition =
+    if pos.span.isSynthetic
+    && pos.span.isZeroExtent
+    && pos.span.exists
+    && pos.span.start == pos.source.length
+    && pos.source(pos.span.start - 1) == '\n'
+    then
+    pos.withSpan(pos.span.shift(-1))
+    else
+    pos
+
   /** The whole message rendered from `dia.msg`.
    *
    *  For a position in an inline expansion, choose `pos1`
@@ -252,17 +266,6 @@ trait MessageRendering {
    *
    */
   def messageAndPos(dia: Diagnostic)(using Context): String =
-    // adjust a pos at EOF if preceded by newline
-    def adjust(pos: SourcePosition): SourcePosition =
-      if pos.span.isSynthetic
-      && pos.span.isZeroExtent
-      && pos.span.exists
-      && pos.span.start == pos.source.length
-      && pos.source(pos.span.start - 1) == '\n'
-      then
-        pos.withSpan(pos.span.shift(-1))
-      else
-        pos
     val msg = dia.msg
     val pos = dia.pos
     val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos
@@ -296,6 +299,9 @@ trait MessageRendering {
         sb.append(EOL).append(endBox)
       end if
     else sb.append(msg.message)
+
+    dia.getSubdiags.foreach(addSubdiagnostic(sb, _))
+
     if dia.isVerbose then
       appendFilterHelp(dia, sb)
 
@@ -313,6 +319,20 @@ trait MessageRendering {
     sb.toString
   end messageAndPos
 
+  private def addSubdiagnostic(sb: StringBuilder, subdiag: Subdiagnostic)(using Context, Level, Offset): Unit =
+    val pos1 = adjust(subdiag.pos)
+    val msg = subdiag.msg
+    assert(pos1.exists && pos1.source.file.exists)
+
+    val posString = posStr(pos1, msg, "Note", isSubdiag = true)
+    val (srcBefore, srcAfter, offset) = sourceLines(pos1)
+    val marker = positionMarker(pos1)
+    val err = errorMsg(pos1, msg.message)
+
+    val diagText = (posString :: srcBefore ::: marker :: err :: srcAfter).mkString(EOL)
+    sb.append(EOL)
+    sb.append(diagText)
+
   private def hl(str: String)(using Context, Level): String =
     summon[Level].value match
       case interfaces.Diagnostic.ERROR   => Red(str).show

From 0f7f56fab75c6513ec4da06c1defaca4920b98d2 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Wed, 12 Nov 2025 19:38:25 +0100
Subject: [PATCH 02/14] Use sub-diagnostics for consume error

---
 compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 7442b44cf07f..888def8ddc77 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -454,6 +454,14 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             |No clashing definitions were found. This might point to an internal error.""",
         tree.srcPos)
 
+  class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Diagnostic.Error(
+    em"""Separation failure: Illegal access to $ref, which was consumed
+        |and therefore is no longer available.""",
+    useLoc.sourcePos
+  ):
+      addSubdiag(em"""$ref was passed to a consume parameter or
+                     |was used as a prefix of a consume method here.""", consumedLoc.sourcePos)
+
   /** Report a failure where a previously consumed capability is used again,
    *  @param ref     the capability that is used after being consumed
    *  @param loc     the position where the capability was consumed
@@ -465,6 +473,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       em"""Separation failure: Illegal access to $ref, which was ${role.howConsumed}
           |on line ${locPos.line + 1} and therefore is no longer available.""",
       pos)
+  // def consumeError(ref: Capability, loc: SrcPos, pos: SrcPos)(using Context): Unit =
+  //   ctx.reporter.report(UseAfterConsume(ref, loc, pos))
 
   /** Report a failure where a capability is consumed in a loop.
    *  @param ref     the capability

From f15a919b2810abdfdc56db7ef70a15e84d704e76 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 13 Nov 2025 13:57:08 +0100
Subject: [PATCH 03/14] Tweak the error message

---
 compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 888def8ddc77..1258061aea65 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -455,12 +455,12 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         tree.srcPos)
 
   class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Diagnostic.Error(
-    em"""Separation failure: Illegal access to $ref, which was consumed
+    em"""Separation failure: Illegal access to $ref, which was passed to a
+        |consume parameter or was used as a prefix to a consume method
         |and therefore is no longer available.""",
     useLoc.sourcePos
   ):
-      addSubdiag(em"""$ref was passed to a consume parameter or
-                     |was used as a prefix of a consume method here.""", consumedLoc.sourcePos)
+      addSubdiag(em"... $ref was consumed here.", consumedLoc.sourcePos)
 
   /** Report a failure where a previously consumed capability is used again,
    *  @param ref     the capability that is used after being consumed

From 7a51cca32e1537db71ecf4bb115d0e63a480082d Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 20 Nov 2025 00:40:26 +0100
Subject: [PATCH 04/14] First prototype of all-in-one multi-span rendering

---
 .../dotc/reporting/MessageRendering.scala     | 207 ++++++++++++++----
 1 file changed, 165 insertions(+), 42 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
index 68b4b74089f2..af6b9e0e5718 100644
--- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
@@ -246,65 +246,113 @@ trait MessageRendering {
     else
     pos
 
-  /** The whole message rendered from `dia.msg`.
-   *
-   *  For a position in an inline expansion, choose `pos1`
-   *  which is the most specific position in the call written
-   *  by the user. For a diagnostic at EOF, where the last char
-   *  of source text is a newline, adjust the position to render
-   *  before the newline, at the end of the last line of text.
-   *
-   *  The rendering begins with a label and position (`posString`).
-   *  Then `sourceLines` with embedded caret `positionMarker`
-   *  and rendered message.
-   *
-   *  Then an `Inline stack trace` showing context for inlined code.
-   *  Inlined positions are taken which don't contain `pos1`.
-   *  (That should probably be positions not contained by outermost.)
-   *  Note that position equality includes `outer` position;
-   *  usually we intend to test `contains` or `coincidesWith`.
-   *
-   */
-  def messageAndPos(dia: Diagnostic)(using Context): String =
+  /** Render diagnostics with positions in different files separately */
+  private def renderSeparateSpans(dia: Diagnostic)(using Context): String =
     val msg = dia.msg
     val pos = dia.pos
-    val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos
-    val outermost = pos.outermost // call.pos
-    val inlineStack = pos.inlinePosStack.filterNot(outermost.contains(_))
+    val pos1 = adjust(pos.nonInlined)
     given Level = Level(dia.level)
     given Offset =
-      val maxLineNumber =
-        if pos.exists then (pos1 :: inlineStack).map(_.endLine).max + 1
-        else 0
+      val maxLineNumber = if pos.exists then pos1.endLine + 1 else 0
       Offset(maxLineNumber.toString.length + 2)
+
     val sb = StringBuilder()
     val posString = posStr(pos1, msg, diagnosticLevel(dia))
     if posString.nonEmpty then sb.append(posString).append(EOL)
+
     if pos.exists && pos1.exists && pos1.source.file.exists then
       val (srcBefore, srcAfter, offset) = sourceLines(pos1)
       val marker = positionMarker(pos1)
       val err = errorMsg(pos1, msg.message)
       sb.append((srcBefore ::: marker :: err :: srcAfter).mkString(EOL))
-
-      if inlineStack.nonEmpty then
-        sb.append(EOL).append(newBox())
-        sb.append(EOL).append(offsetBox).append(i"Inline stack trace")
-        for inlinedPos <- inlineStack do
-          sb.append(EOL).append(newBox(soft = true))
-          sb.append(EOL).append(offsetBox).append(i"This location contains code that was inlined from $pos")
-          if inlinedPos.source.file.exists then
-            val (srcBefore, srcAfter, _) = sourceLines(inlinedPos)
-            val marker = positionMarker(inlinedPos)
-            sb.append(EOL).append((srcBefore ::: marker :: srcAfter).mkString(EOL))
-        sb.append(EOL).append(endBox)
-      end if
-    else sb.append(msg.message)
+    else
+      sb.append(msg.message)
 
     dia.getSubdiags.foreach(addSubdiagnostic(sb, _))
+    sb.toString
+
+  def messageAndPosMultiSpan(dia: Diagnostic)(using Context): String =
+    val msg = dia.msg
+    val pos = dia.pos
+    val pos1 = adjust(pos.nonInlined)
+    val subdiags = dia.getSubdiags
+
+    // Collect all positions with their associated messages
+    case class PosAndMsg(pos: SourcePosition, msg: Message, isPrimary: Boolean)
+    val allPosAndMsg = PosAndMsg(pos1, msg, true) :: subdiags.map(s => PosAndMsg(adjust(s.pos), s.msg, false))
+    val validPosAndMsg = allPosAndMsg.filter(_.pos.exists)
+
+    if validPosAndMsg.isEmpty then
+      return msg.message
+
+    // Check all positions are in the same source file
+    val source = validPosAndMsg.head.pos.source
+    if !validPosAndMsg.forall(_.pos.source == source) || !source.file.exists then
+      // Cannot render multi-span if positions are in different files
+      // Fall back to showing them separately
+      return renderSeparateSpans(dia)
+
+    // Find the line range covering all positions
+    val minLine = validPosAndMsg.map(_.pos.startLine).min
+    val maxLine = validPosAndMsg.map(_.pos.endLine).max
+    val maxLineNumber = maxLine + 1
+
+    given Level = Level(dia.level)
+    given Offset = Offset(maxLineNumber.toString.length + 2)
+
+    val sb = StringBuilder()
+
+    // Title using the primary position
+    val posString = posStr(pos1, msg, diagnosticLevel(dia))
+    if posString.nonEmpty then sb.append(posString).append(EOL)
+
+    // Render the unified code snippet
+    // Get syntax-highlighted content for the entire range
+    val startOffset = source.lineToOffset(minLine)
+    val endOffset = source.nextLine(source.lineToOffset(maxLine))
+    val content = source.content.slice(startOffset, endOffset)
+    val syntax =
+      if (summon[Context].settings.color.value != "never" && !summon[Context].isJava)
+        SyntaxHighlighting.highlight(new String(content)).toCharArray
+      else content
+
+    // Split syntax-highlighted content into lines
+    def linesFrom(arr: Array[Char]): List[String] = {
+      def pred(c: Char) = (c: @switch) match {
+        case LF | CR | FF | SU => true
+        case _ => false
+      }
+      val (line, rest0) = arr.span(!pred(_))
+      val (_, rest) = rest0.span(pred)
+      new String(line) :: { if (rest.isEmpty) Nil else linesFrom(rest) }
+    }
 
-    if dia.isVerbose then
-      appendFilterHelp(dia, sb)
+    val lines = linesFrom(syntax)
+    val lineNumberWidth = maxLineNumber.toString.length
+
+    // Render each line with its markers and messages
+    for (lineNum <- minLine to maxLine) {
+      val lineIdx = lineNum - minLine
+      if lineIdx < lines.length then
+        val lineContent = lines(lineIdx)
+        val lineNbr = (lineNum + 1).toString
+        val linePrefix = String.format(s"%${lineNumberWidth}s |", lineNbr)
+        val lnum = hl(" " * math.max(0, offset - linePrefix.length - 1) + linePrefix)
+        sb.append(lnum).append(lineContent.stripLineEnd).append(EOL)
+
+        // Find all positions that should show markers after this line
+        // A position shows its marker after its start line
+        val positionsOnLine = validPosAndMsg.filter(_.pos.startLine == lineNum)
+          .sortBy(pm => (pm.pos.startColumn, !pm.isPrimary)) // Primary positions first if same column
+
+        for posAndMsg <- positionsOnLine do
+          val marker = positionMarker(posAndMsg.pos)
+          val err = errorMsg(posAndMsg.pos, posAndMsg.msg.message)
+          sb.append(marker).append(EOL)
+          sb.append(err).append(EOL)
+    }
 
+    // Add explanation if needed
     if Diagnostic.shouldExplain(dia) then
       sb.append(EOL).append(newBox())
       sb.append(EOL).append(offsetBox).append(" Explanation (enabled by `-explain`)")
@@ -317,6 +365,81 @@ trait MessageRendering {
       sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`")
 
     sb.toString
+  end messageAndPosMultiSpan
+
+  /** The whole message rendered from `dia.msg`.
+   *
+   *  For a position in an inline expansion, choose `pos1`
+   *  which is the most specific position in the call written
+   *  by the user. For a diagnostic at EOF, where the last char
+   *  of source text is a newline, adjust the position to render
+   *  before the newline, at the end of the last line of text.
+   *
+   *  The rendering begins with a label and position (`posString`).
+   *  Then `sourceLines` with embedded caret `positionMarker`
+   *  and rendered message.
+   *
+   *  Then an `Inline stack trace` showing context for inlined code.
+   *  Inlined positions are taken which don't contain `pos1`.
+   *  (That should probably be positions not contained by outermost.)
+   *  Note that position equality includes `outer` position;
+   *  usually we intend to test `contains` or `coincidesWith`.
+   *
+   */
+  def messageAndPos(dia: Diagnostic)(using Context): String =
+    if dia.getSubdiags.nonEmpty then messageAndPosMultiSpan(dia)
+    else
+      val msg = dia.msg
+      val pos = dia.pos
+      val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos
+      val outermost = pos.outermost // call.pos
+      val inlineStack = pos.inlinePosStack.filterNot(outermost.contains(_))
+      given Level = Level(dia.level)
+      given Offset =
+        val maxLineNumber =
+          if pos.exists then (pos1 :: inlineStack).map(_.endLine).max + 1
+          else 0
+        Offset(maxLineNumber.toString.length + 2)
+      val sb = StringBuilder()
+      val posString = posStr(pos1, msg, diagnosticLevel(dia))
+      if posString.nonEmpty then sb.append(posString).append(EOL)
+      if pos.exists && pos1.exists && pos1.source.file.exists then
+        val (srcBefore, srcAfter, offset) = sourceLines(pos1)
+        val marker = positionMarker(pos1)
+        val err = errorMsg(pos1, msg.message)
+        sb.append((srcBefore ::: marker :: err :: srcAfter).mkString(EOL))
+
+        if inlineStack.nonEmpty then
+          sb.append(EOL).append(newBox())
+          sb.append(EOL).append(offsetBox).append(i"Inline stack trace")
+          for inlinedPos <- inlineStack do
+            sb.append(EOL).append(newBox(soft = true))
+            sb.append(EOL).append(offsetBox).append(i"This location contains code that was inlined from $pos")
+            if inlinedPos.source.file.exists then
+              val (srcBefore, srcAfter, _) = sourceLines(inlinedPos)
+              val marker = positionMarker(inlinedPos)
+              sb.append(EOL).append((srcBefore ::: marker :: srcAfter).mkString(EOL))
+          sb.append(EOL).append(endBox)
+        end if
+      else sb.append(msg.message)
+
+      dia.getSubdiags.foreach(addSubdiagnostic(sb, _))
+
+      if dia.isVerbose then
+        appendFilterHelp(dia, sb)
+
+      if Diagnostic.shouldExplain(dia) then
+        sb.append(EOL).append(newBox())
+        sb.append(EOL).append(offsetBox).append(" Explanation (enabled by `-explain`)")
+        sb.append(EOL).append(newBox(soft = true))
+        dia.msg.explanation.split(raw"\R").foreach: line =>
+          sb.append(EOL).append(offsetBox).append(if line.isEmpty then "" else " ").append(line)
+        sb.append(EOL).append(endBox)
+      else if dia.msg.canExplain then
+        sb.append(EOL).append(offsetBox)
+        sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`")
+
+      sb.toString
   end messageAndPos
 
   private def addSubdiagnostic(sb: StringBuilder, subdiag: Subdiagnostic)(using Context, Level, Offset): Unit =

From 90f03eb91ce83a462325f793ecdbbc66a620e5db Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 20 Nov 2025 00:43:55 +0100
Subject: [PATCH 05/14] Use `---` for secondary messages

---
 .../dotc/reporting/MessageRendering.scala     | 23 +++++++++++++------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
index af6b9e0e5718..4a78f6b41403 100644
--- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
@@ -88,14 +88,21 @@ trait MessageRendering {
    *  ```
    *    |         ^^^^^
    *  ```
+   *  or for sub-diagnostics:
+   *  ```
+   *    |         -----
+   *  ```
+   *
+   *  @param pos the source position to mark
+   *  @param markerChar the character to use for marking ('^' for primary errors, '-' for notes)
    */
-  private def positionMarker(pos: SourcePosition)(using Context, Level, Offset): String = {
+  private def positionMarker(pos: SourcePosition, markerChar: Char = '^')(using Context, Level, Offset): String = {
     val padding = pos.startColumnPadding
-    val carets =
+    val markers =
       if (pos.startLine == pos.endLine)
-        "^" * math.max(1, pos.endColumn - pos.startColumn)
-      else "^"
-    hl(s"$offsetBox$padding$carets")
+        markerChar.toString * math.max(1, pos.endColumn - pos.startColumn)
+      else markerChar.toString
+    hl(s"$offsetBox$padding$markers")
   }
 
   /** The horizontal line with the given offset
@@ -346,7 +353,9 @@ trait MessageRendering {
           .sortBy(pm => (pm.pos.startColumn, !pm.isPrimary)) // Primary positions first if same column
 
         for posAndMsg <- positionsOnLine do
-          val marker = positionMarker(posAndMsg.pos)
+          // Use '^' for primary error, '-' for sub-diagnostics
+          val markerChar = if posAndMsg.isPrimary then '^' else '-'
+          val marker = positionMarker(posAndMsg.pos, markerChar)
           val err = errorMsg(posAndMsg.pos, posAndMsg.msg.message)
           sb.append(marker).append(EOL)
           sb.append(err).append(EOL)
@@ -449,7 +458,7 @@ trait MessageRendering {
 
     val posString = posStr(pos1, msg, "Note", isSubdiag = true)
     val (srcBefore, srcAfter, offset) = sourceLines(pos1)
-    val marker = positionMarker(pos1)
+    val marker = positionMarker(pos1, '-')  // Use '-' for sub-diagnostics
     val err = errorMsg(pos1, msg.message)
 
     val diagText = (posString :: srcBefore ::: marker :: err :: srcAfter).mkString(EOL)

From 3e3421296b6231a01d15836157401208078d6b75 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 20 Nov 2025 00:52:11 +0100
Subject: [PATCH 06/14] Display primary error message before multi-span error

---
 .../src/dotty/tools/dotc/reporting/MessageRendering.scala     | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
index 4a78f6b41403..b907cbf24ac1 100644
--- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
@@ -313,6 +313,10 @@ trait MessageRendering {
     val posString = posStr(pos1, msg, diagnosticLevel(dia))
     if posString.nonEmpty then sb.append(posString).append(EOL)
 
+    // Display primary error message before code snippet
+    sb.append(msg.message)
+    if !msg.message.endsWith(EOL) then sb.append(EOL)
+
     // Render the unified code snippet
     // Get syntax-highlighted content for the entire range
     val startOffset = source.lineToOffset(minLine)

From b2addc6ba0ac42a3dc269a67c63e9e9622ef137a Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 20 Nov 2025 01:05:37 +0100
Subject: [PATCH 07/14] Multi-span error reporting for consume errors

---
 compiler/src/dotty/tools/dotc/cc/SepCheck.scala       |  3 ++-
 .../src/dotty/tools/dotc/reporting/Diagnostic.scala   |  9 +++++++++
 .../dotty/tools/dotc/reporting/MessageRendering.scala | 11 +++++++----
 3 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 1258061aea65..9a5bfaccc5cc 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -460,7 +460,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         |and therefore is no longer available.""",
     useLoc.sourcePos
   ):
-      addSubdiag(em"... $ref was consumed here.", consumedLoc.sourcePos)
+      addSubdiag(em"$ref was consumed here.", consumedLoc.sourcePos)
+      addPrimaryNote(em"... and it was used here")
 
   /** Report a failure where a previously consumed capability is used again,
    *  @param ref     the capability that is used after being consumed
diff --git a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
index 90b841a1adcb..dc635c01015a 100644
--- a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
@@ -123,9 +123,18 @@ class Diagnostic(
 
   private val subdiags: ArrayBuffer[Subdiagnostic] = ArrayBuffer.empty
 
+  private var primaryNote: Message | Null = null
+
   def addSubdiag(diag: Subdiagnostic): Unit =
     subdiags += diag
 
+  def addPrimaryNote(msg: Message): Unit =
+    assert(primaryNote eq null)
+    primaryNote = msg
+
+  def getPrimaryNote: Option[Message] =
+    if primaryNote eq null then None else Some(primaryNote.nn)
+
   def addSubdiag(msg: Message, pos: SourcePosition): Unit =
     addSubdiag(Subdiagnostic(msg, pos))
 
diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
index b907cbf24ac1..838ad358f4ca 100644
--- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
@@ -313,7 +313,7 @@ trait MessageRendering {
     val posString = posStr(pos1, msg, diagnosticLevel(dia))
     if posString.nonEmpty then sb.append(posString).append(EOL)
 
-    // Display primary error message before code snippet
+    // Always display primary error message before code snippet
     sb.append(msg.message)
     if !msg.message.endsWith(EOL) then sb.append(EOL)
 
@@ -342,7 +342,7 @@ trait MessageRendering {
     val lineNumberWidth = maxLineNumber.toString.length
 
     // Render each line with its markers and messages
-    for (lineNum <- minLine to maxLine) {
+    for (lineNum <- minLine to maxLine) do
       val lineIdx = lineNum - minLine
       if lineIdx < lines.length then
         val lineContent = lines(lineIdx)
@@ -360,10 +360,13 @@ trait MessageRendering {
           // Use '^' for primary error, '-' for sub-diagnostics
           val markerChar = if posAndMsg.isPrimary then '^' else '-'
           val marker = positionMarker(posAndMsg.pos, markerChar)
-          val err = errorMsg(posAndMsg.pos, posAndMsg.msg.message)
+          // For primary position: use PrimaryNote if available, otherwise use primary message
+          val messageToShow =
+            if posAndMsg.isPrimary then dia.getPrimaryNote.map(_.message).getOrElse(posAndMsg.msg.message)
+            else posAndMsg.msg.message
+          val err = errorMsg(posAndMsg.pos, messageToShow)
           sb.append(marker).append(EOL)
           sb.append(err).append(EOL)
-    }
 
     // Add explanation if needed
     if Diagnostic.shouldExplain(dia) then

From 909e7851eac4b24dc8c7fcef2252daad52a32c92 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Thu, 20 Nov 2025 01:07:30 +0100
Subject: [PATCH 08/14] Tweak the error message

---
 compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 9a5bfaccc5cc..47cedc8a946b 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -460,8 +460,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         |and therefore is no longer available.""",
     useLoc.sourcePos
   ):
-      addSubdiag(em"$ref was consumed here.", consumedLoc.sourcePos)
-      addPrimaryNote(em"... and it was used here")
+      addSubdiag(em"The capability was consumed here.", consumedLoc.sourcePos)
+      addPrimaryNote(em"Then, it was used here")
 
   /** Report a failure where a previously consumed capability is used again,
    *  @param ref     the capability that is used after being consumed

From d45911f3592abbc3d10add00c7a945871c3fa78b Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Fri, 21 Nov 2025 17:25:03 +0100
Subject: [PATCH 09/14] Refactor: move multi-span handling logic to Message

---
 .../src/dotty/tools/dotc/cc/SepCheck.scala    |  35 ++++--
 .../tools/dotc/reporting/Diagnostic.scala     |  27 -----
 .../dotty/tools/dotc/reporting/Message.scala  |  18 +++
 .../dotc/reporting/MessageRendering.scala     | 107 ++++++------------
 4 files changed, 75 insertions(+), 112 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 47cedc8a946b..c4da2298a7b8 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -454,14 +454,31 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             |No clashing definitions were found. This might point to an internal error.""",
         tree.srcPos)
 
-  class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Diagnostic.Error(
-    em"""Separation failure: Illegal access to $ref, which was passed to a
-        |consume parameter or was used as a prefix to a consume method
-        |and therefore is no longer available.""",
-    useLoc.sourcePos
-  ):
-      addSubdiag(em"The capability was consumed here.", consumedLoc.sourcePos)
-      addPrimaryNote(em"Then, it was used here")
+  class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Message(reporting.ErrorMessageID.NoExplanationID):
+    def kind = reporting.MessageKind.NoKind
+
+    protected def msg(using Context): String = ""
+
+    protected def explain(using Context): String = ""
+
+    override def leading(using Context): Option[String] = Some(
+      em"""Separation failure: Illegal access to $ref, which was passed to a
+          |consume parameter or was used as a prefix to a consume method
+          |and therefore is no longer available.""".message
+    )
+
+    override def parts(using Context): List[reporting.Message.MessagePart] = List(
+      reporting.Message.MessagePart(
+        "The capability was consumed here.",
+        consumedLoc.sourcePos,
+        isPrimary = false
+      ),
+      reporting.Message.MessagePart(
+        "Then, it was used here",
+        useLoc.sourcePos,
+        isPrimary = true
+      )
+    )
 
   /** Report a failure where a previously consumed capability is used again,
    *  @param ref     the capability that is used after being consumed
@@ -474,8 +491,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       em"""Separation failure: Illegal access to $ref, which was ${role.howConsumed}
           |on line ${locPos.line + 1} and therefore is no longer available.""",
       pos)
-  // def consumeError(ref: Capability, loc: SrcPos, pos: SrcPos)(using Context): Unit =
-  //   ctx.reporter.report(UseAfterConsume(ref, loc, pos))
 
   /** Report a failure where a capability is consumed in a loop.
    *  @param ref     the capability
diff --git a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
index dc635c01015a..807185106d01 100644
--- a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
@@ -11,8 +11,6 @@ import dotty.tools.dotc.util.chaining.*
 import java.util.{Collections, Optional, List => JList}
 import core.Decorators.toMessage
 
-import collection.mutable.ArrayBuffer
-
 object Diagnostic:
 
   def shouldExplain(dia: Diagnostic)(using Context): Boolean =
@@ -120,30 +118,5 @@ class Diagnostic(
   override def diagnosticRelatedInformation: JList[interfaces.DiagnosticRelatedInformation] =
     Collections.emptyList()
   override def toString: String = s"$getClass at $pos L${pos.line+1}: $message"
-
-  private val subdiags: ArrayBuffer[Subdiagnostic] = ArrayBuffer.empty
-
-  private var primaryNote: Message | Null = null
-
-  def addSubdiag(diag: Subdiagnostic): Unit =
-    subdiags += diag
-
-  def addPrimaryNote(msg: Message): Unit =
-    assert(primaryNote eq null)
-    primaryNote = msg
-
-  def getPrimaryNote: Option[Message] =
-    if primaryNote eq null then None else Some(primaryNote.nn)
-
-  def addSubdiag(msg: Message, pos: SourcePosition): Unit =
-    addSubdiag(Subdiagnostic(msg, pos))
-
-  def withSubdiags(diags: List[Subdiagnostic]): this.type =
-    diags.foreach(addSubdiag)
-    this
-
-  def getSubdiags: List[Subdiagnostic] = subdiags.toList
 end Diagnostic
 
-class Subdiagnostic(val msg: Message, val pos: SourcePosition)
-
diff --git a/compiler/src/dotty/tools/dotc/reporting/Message.scala b/compiler/src/dotty/tools/dotc/reporting/Message.scala
index f0bb57652fd9..2d1a3217b801 100644
--- a/compiler/src/dotty/tools/dotc/reporting/Message.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/Message.scala
@@ -300,6 +300,13 @@ object Message:
       super.toText(sym)
   end Printer
 
+  /** A part of a multi-span message, associating text with a source position.
+   *  @param text       the message text for this part
+   *  @param srcPos     the source position where this part applies
+   *  @param isPrimary  whether this is the primary message (true) or a secondary note (false)
+   */
+  case class MessagePart(text: String, srcPos: util.SourcePosition, isPrimary: Boolean)
+
 end Message
 
 /** A `Message` contains all semantic information necessary to easily
@@ -370,6 +377,17 @@ abstract class Message(val errorId: ErrorMessageID)(using Context) { self =>
     */
   protected def explain(using Context): String
 
+  /** Optional leading text to be displayed before the source snippet.
+    * If present along with parts, triggers multi-span rendering.
+    */
+  def leading(using Context): Option[String] = None
+
+  /** Optional list of message parts for multi-span error messages.
+    * Each part associates text with a source position and indicates
+    * whether it's a primary message or a secondary note.
+    */
+  def parts(using Context): List[MessagePart] = Nil
+
   /** What gets printed after the message proper */
   protected def msgPostscript(using Context): String =
     if ctx eq NoContext then ""
diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
index 838ad358f4ca..4b94a605f49b 100644
--- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
@@ -253,55 +253,31 @@ trait MessageRendering {
     else
     pos
 
-  /** Render diagnostics with positions in different files separately */
-  private def renderSeparateSpans(dia: Diagnostic)(using Context): String =
+  /** Render a message using multi-span information from Message.parts. */
+  def messageAndPosFromParts(dia: Diagnostic)(using Context): String =
     val msg = dia.msg
     val pos = dia.pos
     val pos1 = adjust(pos.nonInlined)
-    given Level = Level(dia.level)
-    given Offset =
-      val maxLineNumber = if pos.exists then pos1.endLine + 1 else 0
-      Offset(maxLineNumber.toString.length + 2)
-
-    val sb = StringBuilder()
-    val posString = posStr(pos1, msg, diagnosticLevel(dia))
-    if posString.nonEmpty then sb.append(posString).append(EOL)
+    val msgParts = msg.parts
 
-    if pos.exists && pos1.exists && pos1.source.file.exists then
-      val (srcBefore, srcAfter, offset) = sourceLines(pos1)
-      val marker = positionMarker(pos1)
-      val err = errorMsg(pos1, msg.message)
-      sb.append((srcBefore ::: marker :: err :: srcAfter).mkString(EOL))
-    else
-      sb.append(msg.message)
+    if msgParts.isEmpty then
+      return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message
 
-    dia.getSubdiags.foreach(addSubdiagnostic(sb, _))
-    sb.toString
+    // Collect all positions from message parts
+    val validParts = msgParts.filter(_.srcPos.exists)
 
-  def messageAndPosMultiSpan(dia: Diagnostic)(using Context): String =
-    val msg = dia.msg
-    val pos = dia.pos
-    val pos1 = adjust(pos.nonInlined)
-    val subdiags = dia.getSubdiags
-
-    // Collect all positions with their associated messages
-    case class PosAndMsg(pos: SourcePosition, msg: Message, isPrimary: Boolean)
-    val allPosAndMsg = PosAndMsg(pos1, msg, true) :: subdiags.map(s => PosAndMsg(adjust(s.pos), s.msg, false))
-    val validPosAndMsg = allPosAndMsg.filter(_.pos.exists)
-
-    if validPosAndMsg.isEmpty then
-      return msg.message
+    if validParts.isEmpty then
+      return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message
 
     // Check all positions are in the same source file
-    val source = validPosAndMsg.head.pos.source
-    if !validPosAndMsg.forall(_.pos.source == source) || !source.file.exists then
-      // Cannot render multi-span if positions are in different files
-      // Fall back to showing them separately
-      return renderSeparateSpans(dia)
+    val source = validParts.head.srcPos.source
+    if !validParts.forall(_.srcPos.source == source) || !source.file.exists then
+      // TODO: support rendering source positions across multiple files
+      return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message
 
     // Find the line range covering all positions
-    val minLine = validPosAndMsg.map(_.pos.startLine).min
-    val maxLine = validPosAndMsg.map(_.pos.endLine).max
+    val minLine = validParts.map(_.srcPos.startLine).min
+    val maxLine = validParts.map(_.srcPos.endLine).max
     val maxLineNumber = maxLine + 1
 
     given Level = Level(dia.level)
@@ -313,12 +289,13 @@ trait MessageRendering {
     val posString = posStr(pos1, msg, diagnosticLevel(dia))
     if posString.nonEmpty then sb.append(posString).append(EOL)
 
-    // Always display primary error message before code snippet
-    sb.append(msg.message)
-    if !msg.message.endsWith(EOL) then sb.append(EOL)
+    // Display leading text if present
+    msg.leading.foreach { leadingText =>
+      sb.append(leadingText)
+      if !leadingText.endsWith(EOL) then sb.append(EOL)
+    }
 
     // Render the unified code snippet
-    // Get syntax-highlighted content for the entire range
     val startOffset = source.lineToOffset(minLine)
     val endOffset = source.nextLine(source.lineToOffset(maxLine))
     val content = source.content.slice(startOffset, endOffset)
@@ -352,19 +329,13 @@ trait MessageRendering {
         sb.append(lnum).append(lineContent.stripLineEnd).append(EOL)
 
         // Find all positions that should show markers after this line
-        // A position shows its marker after its start line
-        val positionsOnLine = validPosAndMsg.filter(_.pos.startLine == lineNum)
-          .sortBy(pm => (pm.pos.startColumn, !pm.isPrimary)) // Primary positions first if same column
-
-        for posAndMsg <- positionsOnLine do
-          // Use '^' for primary error, '-' for sub-diagnostics
-          val markerChar = if posAndMsg.isPrimary then '^' else '-'
-          val marker = positionMarker(posAndMsg.pos, markerChar)
-          // For primary position: use PrimaryNote if available, otherwise use primary message
-          val messageToShow =
-            if posAndMsg.isPrimary then dia.getPrimaryNote.map(_.message).getOrElse(posAndMsg.msg.message)
-            else posAndMsg.msg.message
-          val err = errorMsg(posAndMsg.pos, messageToShow)
+        val partsOnLine = validParts.filter(_.srcPos.startLine == lineNum)
+          .sortBy(p => (p.srcPos.startColumn, !p.isPrimary))
+
+        for part <- partsOnLine do
+          val markerChar = if part.isPrimary then '^' else '-'
+          val marker = positionMarker(part.srcPos, markerChar)
+          val err = errorMsg(part.srcPos, part.text)
           sb.append(marker).append(EOL)
           sb.append(err).append(EOL)
 
@@ -381,7 +352,7 @@ trait MessageRendering {
       sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`")
 
     sb.toString
-  end messageAndPosMultiSpan
+  end messageAndPosFromParts
 
   /** The whole message rendered from `dia.msg`.
    *
@@ -403,9 +374,11 @@ trait MessageRendering {
    *
    */
   def messageAndPos(dia: Diagnostic)(using Context): String =
-    if dia.getSubdiags.nonEmpty then messageAndPosMultiSpan(dia)
+    val msg = dia.msg
+    // Check if message provides its own multi-span structure
+    if msg.leading.isDefined || msg.parts.nonEmpty then
+      messageAndPosFromParts(dia)
     else
-      val msg = dia.msg
       val pos = dia.pos
       val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos
       val outermost = pos.outermost // call.pos
@@ -439,8 +412,6 @@ trait MessageRendering {
         end if
       else sb.append(msg.message)
 
-      dia.getSubdiags.foreach(addSubdiagnostic(sb, _))
-
       if dia.isVerbose then
         appendFilterHelp(dia, sb)
 
@@ -458,20 +429,6 @@ trait MessageRendering {
       sb.toString
   end messageAndPos
 
-  private def addSubdiagnostic(sb: StringBuilder, subdiag: Subdiagnostic)(using Context, Level, Offset): Unit =
-    val pos1 = adjust(subdiag.pos)
-    val msg = subdiag.msg
-    assert(pos1.exists && pos1.source.file.exists)
-
-    val posString = posStr(pos1, msg, "Note", isSubdiag = true)
-    val (srcBefore, srcAfter, offset) = sourceLines(pos1)
-    val marker = positionMarker(pos1, '-')  // Use '-' for sub-diagnostics
-    val err = errorMsg(pos1, msg.message)
-
-    val diagText = (posString :: srcBefore ::: marker :: err :: srcAfter).mkString(EOL)
-    sb.append(EOL)
-    sb.append(diagText)
-
   private def hl(str: String)(using Context, Level): String =
     summon[Level].value match
       case interfaces.Diagnostic.ERROR   => Red(str).show

From 9053eee1471977182eaa2e043b65e08d91d26515 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Fri, 21 Nov 2025 17:39:43 +0100
Subject: [PATCH 10/14] Move UseAfterConsume to messages.scala

---
 .../src/dotty/tools/dotc/cc/SepCheck.scala    | 26 -------------------
 .../dotty/tools/dotc/reporting/messages.scala | 24 +++++++++++++++++
 2 files changed, 24 insertions(+), 26 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index c4da2298a7b8..7442b44cf07f 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -454,32 +454,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             |No clashing definitions were found. This might point to an internal error.""",
         tree.srcPos)
 
-  class UseAfterConsume(ref: Capability, consumedLoc: SrcPos, useLoc: SrcPos)(using Context) extends reporting.Message(reporting.ErrorMessageID.NoExplanationID):
-    def kind = reporting.MessageKind.NoKind
-
-    protected def msg(using Context): String = ""
-
-    protected def explain(using Context): String = ""
-
-    override def leading(using Context): Option[String] = Some(
-      em"""Separation failure: Illegal access to $ref, which was passed to a
-          |consume parameter or was used as a prefix to a consume method
-          |and therefore is no longer available.""".message
-    )
-
-    override def parts(using Context): List[reporting.Message.MessagePart] = List(
-      reporting.Message.MessagePart(
-        "The capability was consumed here.",
-        consumedLoc.sourcePos,
-        isPrimary = false
-      ),
-      reporting.Message.MessagePart(
-        "Then, it was used here",
-        useLoc.sourcePos,
-        isPrimary = true
-      )
-    )
-
   /** Report a failure where a previously consumed capability is used again,
    *  @param ref     the capability that is used after being consumed
    *  @param loc     the position where the capability was consumed
diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index a2afaab0ecce..6dbdd95f5b77 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -3741,3 +3741,27 @@ final class EncodedPackageName(name: Name)(using Context) extends SyntaxMsg(Enco
        |or `myfile-test.scala` can produce encoded names for the generated package objects.
        |
        |In this case, the name `$name` is encoded as `${name.encode}`."""
+
+class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition)(using Context)
+extends TypeMsg(NoExplanationID):
+  protected def msg(using Context): String =
+    i"""Separation failure: Illegal access to $ref, which was passed to a
+       |consume parameter or was used as a prefix to a consume method
+       |and therefore is no longer available."""
+
+  protected def explain(using Context): String = ""
+
+  override def leading(using Context): Option[String] = Some(message)
+
+  override def parts(using Context): List[Message.MessagePart] = List(
+    Message.MessagePart(
+      "The capability was consumed here.",
+      consumedLoc,
+      isPrimary = false
+    ),
+    Message.MessagePart(
+      "Then, it was used here",
+      useLoc,
+      isPrimary = true
+    )
+  )

From aee8019f8b8dc188b723433d356cd8bf937bb727 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sat, 22 Nov 2025 00:08:47 +0100
Subject: [PATCH 11/14] Add test for consume error

---
 tests/neg-custom-args/captures/consume-twice.check | 13 +++++++++++++
 tests/neg-custom-args/captures/consume-twice.scala |  6 ++++++
 2 files changed, 19 insertions(+)
 create mode 100644 tests/neg-custom-args/captures/consume-twice.check
 create mode 100644 tests/neg-custom-args/captures/consume-twice.scala

diff --git a/tests/neg-custom-args/captures/consume-twice.check b/tests/neg-custom-args/captures/consume-twice.check
new file mode 100644
index 000000000000..073a1459c9a4
--- /dev/null
+++ b/tests/neg-custom-args/captures/consume-twice.check
@@ -0,0 +1,13 @@
+-- Type Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 --------------------------------------------------
+Separation failure: Illegal access to (x : Object^), which was passed to a
+consume parameter or was used as a prefix to a consume method
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+5 |  send(x)
+  |       -
+  |       The capability was consumed here.
+6 |  send(x)  // error
+  |       ^
+  |       Then, it was used here
+
diff --git a/tests/neg-custom-args/captures/consume-twice.scala b/tests/neg-custom-args/captures/consume-twice.scala
new file mode 100644
index 000000000000..b0f955e9dbf7
--- /dev/null
+++ b/tests/neg-custom-args/captures/consume-twice.scala
@@ -0,0 +1,6 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+def send(consume x: Object^): Unit = ()
+def consumeTwice(consume x: Object^): Unit =
+  send(x)
+  send(x)  // error

From f02de951fa4c5e794e581963f33162712d482d4e Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sat, 22 Nov 2025 00:22:18 +0100
Subject: [PATCH 12/14] Support multi-parts on the same line

---
 .../dotc/reporting/MessageRendering.scala     | 46 ++++++++++++++++++-
 .../captures/consume-twice-same-line.check    | 33 +++++++++++++
 .../captures/consume-twice-same-line.scala    |  8 ++++
 3 files changed, 86 insertions(+), 1 deletion(-)
 create mode 100644 tests/neg-custom-args/captures/consume-twice-same-line.check
 create mode 100644 tests/neg-custom-args/captures/consume-twice-same-line.scala

diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
index 4b94a605f49b..d59af43691fa 100644
--- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
@@ -332,12 +332,56 @@ trait MessageRendering {
         val partsOnLine = validParts.filter(_.srcPos.startLine == lineNum)
           .sortBy(p => (p.srcPos.startColumn, !p.isPrimary))
 
-        for part <- partsOnLine do
+        if partsOnLine.size == 1 then
+          // Single marker on this line
+          val part = partsOnLine.head
           val markerChar = if part.isPrimary then '^' else '-'
           val marker = positionMarker(part.srcPos, markerChar)
           val err = errorMsg(part.srcPos, part.text)
           sb.append(marker).append(EOL)
           sb.append(err).append(EOL)
+        else if partsOnLine.size > 1 then
+          // Multiple markers on same line
+          val markerLine = StringBuilder()
+          markerLine.append(offsetBox)
+
+          var currentCol = 0
+          for part <- partsOnLine do
+            val markerChar = if part.isPrimary then '^' else '-'
+            val targetCol = part.srcPos.startColumn
+            val padding = " " * (targetCol - currentCol)
+            markerLine.append(padding).append(markerChar)
+            currentCol = targetCol + 1
+
+          sb.append(markerLine).append(EOL)
+
+          // Render messages from right to left with connector bars
+          val sortedByColumn = partsOnLine.reverse // rightmost first
+          for (part, idx) <- sortedByColumn.zipWithIndex do
+            val remainingParts = sortedByColumn.drop(idx + 1) // parts still waiting for messages
+
+            // Build connector line with vertical bars for remaining parts
+            val connectorLine = StringBuilder()
+            connectorLine.append(offsetBox)
+
+            var col = 0
+            // First, add vertical bars for all remaining (not-yet-shown) parts
+            for p <- partsOnLine do
+              if remainingParts.contains(p) then
+                val targetCol = p.srcPos.startColumn
+                val padding = " " * (targetCol - col)
+                connectorLine.append(padding).append("|")
+                col = targetCol + 1
+
+            // Then add the message for the current part, aligned to its column
+            val msgText = part.text
+            val msgCol = part.srcPos.startColumn
+            // If we've added bars, col is position after last bar; if not, col is 0
+            // We want the message to start at msgCol, with at least one space separation
+            val msgPadding = if col == 0 then " " * msgCol else " " * Math.max(1, msgCol - col)
+            connectorLine.append(msgPadding).append(msgText)
+
+            sb.append(connectorLine).append(EOL)
 
     // Add explanation if needed
     if Diagnostic.shouldExplain(dia) then
diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.check b/tests/neg-custom-args/captures/consume-twice-same-line.check
new file mode 100644
index 000000000000..24a8a4734042
--- /dev/null
+++ b/tests/neg-custom-args/captures/consume-twice-same-line.check
@@ -0,0 +1,33 @@
+-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 ---------------------------------------
+Separation failure: Illegal access to (x : Object^), which was passed to a
+consume parameter or was used as a prefix to a consume method
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+5 |  send(x); send(x)  // error
+  |       -        ^
+  |       |        Then, it was used here
+  |       The capability was consumed here.
+
+-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 ---------------------------------------
+Separation failure: Illegal access to (x : Object^), which was passed to a
+consume parameter or was used as a prefix to a consume method
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+8 |  send(x); send(x); send(x)  // error // error
+  |       -        ^
+  |       |        Then, it was used here
+  |       The capability was consumed here.
+
+-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 ---------------------------------------
+Separation failure: Illegal access to (x : Object^), which was passed to a
+consume parameter or was used as a prefix to a consume method
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+8 |  send(x); send(x); send(x)  // error // error
+  |       -                 ^
+  |       |                 Then, it was used here
+  |       The capability was consumed here.
+
diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.scala b/tests/neg-custom-args/captures/consume-twice-same-line.scala
new file mode 100644
index 000000000000..858786419e16
--- /dev/null
+++ b/tests/neg-custom-args/captures/consume-twice-same-line.scala
@@ -0,0 +1,8 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+def send(consume x: Object^): Unit = ()
+def consumeTwice(consume x: Object^): Unit =
+  send(x); send(x)  // error
+
+def consumeThrice(consume x: Object^): Unit =
+  send(x); send(x); send(x)  // error // error

From 7089e839c539d41017f233c59fd1278e40d190dd Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sat, 22 Nov 2025 00:32:47 +0100
Subject: [PATCH 13/14] Use precise consume reason

---
 compiler/src/dotty/tools/dotc/cc/SepCheck.scala          | 5 +----
 compiler/src/dotty/tools/dotc/reporting/messages.scala   | 5 ++---
 .../captures/consume-twice-same-line.check               | 9 +++------
 tests/neg-custom-args/captures/consume-twice.check       | 3 +--
 4 files changed, 7 insertions(+), 15 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 7442b44cf07f..d482734b4cc9 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -461,10 +461,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
    */
   def consumeError(ref: Capability, loc: (SrcPos, TypeRole), pos: SrcPos)(using Context): Unit =
     val (locPos, role) = loc
-    report.error(
-      em"""Separation failure: Illegal access to $ref, which was ${role.howConsumed}
-          |on line ${locPos.line + 1} and therefore is no longer available.""",
-      pos)
+    report.error(reporting.UseAfterConsume(ref, locPos.sourcePos, pos.sourcePos, role.howConsumed), pos)
 
   /** Report a failure where a capability is consumed in a loop.
    *  @param ref     the capability
diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index 6dbdd95f5b77..35d6d42f6a16 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -3742,11 +3742,10 @@ final class EncodedPackageName(name: Name)(using Context) extends SyntaxMsg(Enco
        |
        |In this case, the name `$name` is encoded as `${name.encode}`."""
 
-class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition)(using Context)
+class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context)
 extends TypeMsg(NoExplanationID):
   protected def msg(using Context): String =
-    i"""Separation failure: Illegal access to $ref, which was passed to a
-       |consume parameter or was used as a prefix to a consume method
+    i"""Separation failure: Illegal access to $ref, which was $howConsumed
        |and therefore is no longer available."""
 
   protected def explain(using Context): String = ""
diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.check b/tests/neg-custom-args/captures/consume-twice-same-line.check
index 24a8a4734042..d549f450be1d 100644
--- a/tests/neg-custom-args/captures/consume-twice-same-line.check
+++ b/tests/neg-custom-args/captures/consume-twice-same-line.check
@@ -1,6 +1,5 @@
 -- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 ---------------------------------------
-Separation failure: Illegal access to (x : Object^), which was passed to a
-consume parameter or was used as a prefix to a consume method
+Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
 and therefore is no longer available.
 
 where:    ^ refers to a fresh root capability in the type of parameter x
@@ -10,8 +9,7 @@ where:    ^ refers to a fresh root capability in the type of parameter x
   |       The capability was consumed here.
 
 -- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 ---------------------------------------
-Separation failure: Illegal access to (x : Object^), which was passed to a
-consume parameter or was used as a prefix to a consume method
+Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
 and therefore is no longer available.
 
 where:    ^ refers to a fresh root capability in the type of parameter x
@@ -21,8 +19,7 @@ where:    ^ refers to a fresh root capability in the type of parameter x
   |       The capability was consumed here.
 
 -- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 ---------------------------------------
-Separation failure: Illegal access to (x : Object^), which was passed to a
-consume parameter or was used as a prefix to a consume method
+Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
 and therefore is no longer available.
 
 where:    ^ refers to a fresh root capability in the type of parameter x
diff --git a/tests/neg-custom-args/captures/consume-twice.check b/tests/neg-custom-args/captures/consume-twice.check
index 073a1459c9a4..6f88f54a1d4d 100644
--- a/tests/neg-custom-args/captures/consume-twice.check
+++ b/tests/neg-custom-args/captures/consume-twice.check
@@ -1,6 +1,5 @@
 -- Type Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 --------------------------------------------------
-Separation failure: Illegal access to (x : Object^), which was passed to a
-consume parameter or was used as a prefix to a consume method
+Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
 and therefore is no longer available.
 
 where:    ^ refers to a fresh root capability in the type of parameter x

From 2ee70f26049517d2e54ba33489c299688f3ab678 Mon Sep 17 00:00:00 2001
From: Yichen Xu <yichen.x@outlook.com>
Date: Sat, 22 Nov 2025 14:32:52 +0100
Subject: [PATCH 14/14] Update checkfiles

---
 .../dotty/tools/dotc/reporting/messages.scala |  5 +-
 .../captures/linear-buffer-2.check            | 60 +++++++++++-----
 .../captures/linear-buffer.check              | 71 ++++++++++++++-----
 .../captures/sep-consume.check                | 28 +++++---
 4 files changed, 120 insertions(+), 44 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index 35d6d42f6a16..bfdd402b448e 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -3742,8 +3742,9 @@ final class EncodedPackageName(name: Name)(using Context) extends SyntaxMsg(Enco
        |
        |In this case, the name `$name` is encoded as `${name.encode}`."""
 
-class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context)
-extends TypeMsg(NoExplanationID):
+class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context) extends Message(NoExplanationID):
+  def kind = MessageKind.NoKind
+
   protected def msg(using Context): String =
     i"""Separation failure: Illegal access to $ref, which was $howConsumed
        |and therefore is no longer available."""
diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check
index ae70cb3aa249..47445ff8e6b9 100644
--- a/tests/neg-custom-args/captures/linear-buffer-2.check
+++ b/tests/neg-custom-args/captures/linear-buffer-2.check
@@ -1,31 +1,59 @@
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 ---------------------------------------------------
+Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter buf
+11 |  val buf1: Buffer[Int]^ = buf.append(1)
+   |                           ---
+   |                           The capability was consumed here.
+12 |  val buf2 = buf1.append(2) // OK
 13 |  val buf3 = buf.append(3) // error
    |             ^^^
-   | Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append
-   | on line 11 and therefore is no longer available.
-   |
-   | where:    ^ refers to a fresh root capability in the type of parameter buf
+   |             Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 ---------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value buf1
+18 |    if ??? then buf1.append(2) // OK
+   |                ----
+   |                The capability was consumed here.
+19 |    else buf1.append(3) // OK
 20 |  val buf3 = buf1.append(4) // error
    |             ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
-   |on line 18 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability in the type of value buf1
+   |             Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 ---------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value buf1
+25 |    case 1 => buf1.append(2) // OK
+   |              ----
+   |              The capability was consumed here.
+26 |    case 2 => buf1.append(2)
+27 |    case _ => buf1.append(3)
 28 |  val buf3 = buf1.append(4) // error
    |             ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
-   |on line 25 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability in the type of value buf1
+   |             Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 ---------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value buf1
+33 |    case 1 => buf1.append(2) // OK
+   |              ----
+   |              The capability was consumed here.
+34 |    case 2 => buf1.append(2)
+35 |    case 3 => buf1.append(3)
+36 |    case 4 => buf1.append(4)
+37 |    case 5 => buf1.append(5)
 38 |  val buf3 = buf1.append(4) // error
    |             ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
-   |on line 33 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability in the type of value buf1
+   |             Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ----------------------------------------------------
 42 |    buf.append(1)  // error
    |    ^^^
diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check
index 97d0409e55ed..b545a6456ef3 100644
--- a/tests/neg-custom-args/captures/linear-buffer.check
+++ b/tests/neg-custom-args/captures/linear-buffer.check
@@ -34,33 +34,61 @@
    |       Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
    |       The access must be in a consume method to allow this.
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:23:17 -----------------------------------------------------
+Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter buf
+21 |  val buf1: Buffer[Int]^ = app(buf, 1)
+   |                               ---
+   |                               The capability was consumed here.
+22 |  val buf2 = app(buf1, 2) // OK
 23 |  val buf3 = app(buf, 3) // error
    |                 ^^^
-   |Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app
-   |on line 21 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability in the type of parameter buf
+   |                 Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:30:17 -----------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value buf1
+28 |    if ??? then app(buf1, 2) // OK
+   |                    ----
+   |                    The capability was consumed here.
+29 |    else app(buf1, 3) // OK
 30 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
-   |on line 28 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability in the type of value buf1
+   |                 Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 -----------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value buf1
+35 |    case 1 => app(buf1, 2) // OK
+   |                  ----
+   |                  The capability was consumed here.
+36 |    case 2 => app(buf1, 2)
+37 |    case _ => app(buf1, 3)
 38 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
-   |on line 35 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability in the type of value buf1
+   |                 Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:17 -----------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value buf1
+43 |    case 1 => app(buf1, 2) // OK
+   |                  ----
+   |                  The capability was consumed here.
+44 |    case 2 => app(buf1, 2)
+45 |    case 3 => app(buf1, 3)
+46 |    case 4 => app(buf1, 4)
+47 |    case 5 => app(buf1, 5)
 48 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
-   |on line 43 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability in the type of value buf1
+   |                 Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:52:8 ------------------------------------------------------
 52 |    app(buf, 1)  // error
    |        ^^^
@@ -69,7 +97,14 @@
    |
    |        where:    ^ refers to a fresh root capability in the type of parameter buf
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:62:20 -----------------------------------------------------
+Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app
+and therefore is no longer available.
+59 |  val buf1 = app(buf, "hi") // buf unavailable from here
+   |                 ---
+   |                 The capability was consumed here.
+60 |  val c1 = contents(buf1)         // only buf.rd is consumed
+61 |  val c2 = contents(buf1)         // buf.rd can be consumed repeatedly
 62 |  val c3 = contents(buf)  // error
    |                    ^^^
-   |             Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app
-   |             on line 59 and therefore is no longer available.
+   |                    Then, it was used here
+
diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check
index 5854c52cd84b..e6e8dedb31d9 100644
--- a/tests/neg-custom-args/captures/sep-consume.check
+++ b/tests/neg-custom-args/captures/sep-consume.check
@@ -1,17 +1,29 @@
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:19:2 --------------------------------------------------------
+Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+18 |  val rx: () => Unit = bad(f)  // hides x.rd in the resulting `cap`
+   |                           -
+   |                           The capability was consumed here.
 19 |  x.put(42)  // error
    |  ^
-   |  Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
-   |  on line 18 and therefore is no longer available.
-   |
-   |  where:    ^ refers to a fresh root capability in the type of parameter x
+   |  Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 -------------------------------------------------------
+Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+18 |  val rx: () => Unit = bad(f)  // hides x.rd in the resulting `cap`
+   |                           -
+   |                           The capability was consumed here.
+19 |  x.put(42)  // error
+20 |  x.get      // ok rd/rd
 21 |  par(rx, () => x.put(42))  // error
    |                ^
-   |         Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
-   |         on line 18 and therefore is no longer available.
-   |
-   |         where:    ^ refers to a fresh root capability in the type of parameter x
+   |                Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 -------------------------------------------------------
 26 |  def foo = bad(f) // error
    |                ^