started mini notation highlighting

currently deactivated by addMiniLocations flag
This commit is contained in:
Felix Roos 2022-02-20 23:46:45 +01:00
parent 358ba0101e
commit acd07c31ff
5 changed files with 75 additions and 2 deletions

View file

@ -24,6 +24,7 @@
this.type_ = "element";
this.source_ = source;
this.options_ = options;
this.location_ = location();
}
var CommandStub = function(name, options)