changeset 59706 | bf6ca55aae13 |
parent 59671 | 9715eb8e9408 |
child 59707 | 10effab11669 |
--- a/src/Pure/General/position.scala Sun Mar 15 20:35:47 2015 +0100 +++ b/src/Pure/General/position.scala Sun Mar 15 21:57:10 2015 +0100 @@ -21,6 +21,7 @@ val End_Offset = new Properties.Int(Markup.END_OFFSET) val File = new Properties.String(Markup.FILE) val Id = new Properties.Long(Markup.ID) + val Id_String = new Properties.String(Markup.ID) val Def_Line = new Properties.Int(Markup.DEF_LINE) val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)