Skip to content

View option 'hide package prefix' doesn't work #3683

@FliegendeWurst

Description

@FliegendeWurst

Description

The view option "Hide Package Prefix" doesn't seem to actually hide package prefixes on the sequent.

Reproducible

always

Steps to reproduce

Load the file below.

package very.large.path.with.lots.of.members;

class LongMethodName {
    /*@ public normal_behaviour
      @ ensures \result == 100;
      @*/
    public int doIt(LongMethodName a, LongMethodName b, LongMethodName c) {
        return 100;
    }
}

Expected behaviour: package name in very.large.path.with.lots.of.members.LongMethodName::exactInstance(self) = TRUE is abbreviated
Actual behaviour: it is not

The same applies to lots of other places where full class names are displayed (e.g. casts).

Additional information


Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions