Errors with multiple location markers are not displayed correctly

[nickbattle]

Most error messages simply have some text followed by the location of the error in the code, and the error parser uses the location of the error to highlight the location in the editor.

But some (albeit few) errors have multiple locations reported - usually duplication or hiding errors, and the following one about compose types:

Mismatched compose definitions for R.
R: in 'DEFAULT' (C:\Cygwin\home\OvertureWorkspace2\TestSL\TestSL.vdmsl) at line 2:21
R: in 'DEFAULT' (C:\Cygwin\home\OvertureWorkspace2\TestSL\TestSL.vdmsl) at line 3:2

This error only highlights one location in the editor (the second). It would be better if it could highlight both to make the mismatch clearer - though double clicking can obviously only go to one of them. The spec to produce the error is:

types
    A = seq of compose R of nat end;
    R :: a : bool;

[peterwvj]

For your example only a single error is reported.

TypeChecker.report(3325, "Mismatched compose definitions for " + composeType.getName(), composeType.getLocation());

[Error 3325: Mismatched compose definitions for R in 'DEFAULT' (/home/peter/dev/rt-ovt-ws/A/A.vdmsl) at line 2:24]

Afterwards details about the error message are appended to the last error message

TypeChecker.detail2(composeType.getName().getName(), composeType.getLocation(), existing.getName().getName(), existing.getLocation());

[Error 3325: Mismatched compose definitions for R in 'DEFAULT' (/home/peter/dev/rt-ovt-ws/A/A.vdmsl) at line 2:24
R: in 'DEFAULT' (/home/peter/dev/rt-ovt-ws/A/A.vdmsl) at line 2:24
R: in 'DEFAULT' (/home/peter/dev/rt-ovt-ws/A/A.vdmsl) at line 3:5]

Since the detailed location information is appended as a string (see detail method below) the location information is not easily available in the UI code. In order to fix this we probably need to store error details in a different way.

public static void detail(String tag, Object obj)
{
    if (lastMessage != null)
    {
       lastMessage.add(tag + ": " + obj);
    }
}