| changeset 55490 | 9b0fb0e2c9f5 |
| parent 55429 | 4a50f9e70dc1 |
| child 55555 | 9c16317c91d1 |
--- a/src/Pure/General/position.scala Fri Feb 14 14:44:43 2014 +0100 +++ b/src/Pure/General/position.scala Fri Feb 14 14:51:38 2014 +0100 @@ -14,6 +14,8 @@ { type T = Properties.T + val none: T = Nil + val Line = new Properties.Int(Markup.LINE) val Offset = new Properties.Int(Markup.OFFSET) val End_Offset = new Properties.Int(Markup.END_OFFSET)