Update Diagnostic Structure

Author: rcosta358

diagnostics/structure.md diagnostics/diagnostic-structure.mddiagnostics/structure.md renamed to diagnostics/diagnostic-structure.md

@@ -24,6 +24,8 @@ Each part gives a different piece of information:
 | `result must be positive` | The custom error message from the annotation's `msg` parameter |
 | `Counterexample: x == 1 && #ret² == 0` | A concrete model showing why the check fails. Here we can see the failure arises because if `x == 1`, then `x / 2 == 0` |
 
+The error message also includes the absolute path of the file and line where the error was reported, which can be clicked to jump the source code location in the editor.
+
 ## Understanding the Counterexample
 
 The counterexample is a concrete assignment of values that makes the verification fail.

diagnostics/index.md

@@ -13,7 +13,7 @@ cards:
     url: /diagnostics/warnings/
     description: Learn about the different verification warnings LiquidJava can report and what each one means.
   - title: Structure
-    url: /diagnostics/structure/
+    url: /diagnostics/diagnostic-structure/
     description: Learn how to understand a diagnostic message.
   - title: Custom Messages
     url: /diagnostics/custom-messages/