equal
deleted
inserted
replaced
10 object Position |
10 object Position |
11 { |
11 { |
12 type T = List[(String, String)] |
12 type T = List[(String, String)] |
13 |
13 |
14 val Line = new Markup.Int_Property(Markup.LINE) |
14 val Line = new Markup.Int_Property(Markup.LINE) |
15 val End_Line = new Markup.Int_Property(Markup.END_LINE) |
|
16 val Offset = new Markup.Int_Property(Markup.OFFSET) |
15 val Offset = new Markup.Int_Property(Markup.OFFSET) |
17 val End_Offset = new Markup.Int_Property(Markup.END_OFFSET) |
16 val End_Offset = new Markup.Int_Property(Markup.END_OFFSET) |
18 val File = new Markup.Property(Markup.FILE) |
17 val File = new Markup.Property(Markup.FILE) |
19 val Id = new Markup.Long_Property(Markup.ID) |
18 val Id = new Markup.Long_Property(Markup.ID) |
20 |
19 |