src/Pure/General/markup.scala
changeset 43710 7270ae921cf2
parent 43673 29eb1cd29961
child 43721 fad8634cee62
equal deleted inserted replaced
43709:717e96cf9527 43710:7270ae921cf2
   112 
   112 
   113 
   113 
   114   /* position */
   114   /* position */
   115 
   115 
   116   val LINE = "line"
   116   val LINE = "line"
   117   val COLUMN = "column"
       
   118   val OFFSET = "offset"
   117   val OFFSET = "offset"
   119   val END_OFFSET = "end_offset"
   118   val END_OFFSET = "end_offset"
   120   val FILE = "file"
   119   val FILE = "file"
   121   val ID = "id"
   120   val ID = "id"
   122 
   121 
   123   val DEF_LINE = "def_line"
   122   val DEF_LINE = "def_line"
   124   val DEF_COLUMN = "def_column"
       
   125   val DEF_OFFSET = "def_offset"
   123   val DEF_OFFSET = "def_offset"
   126   val DEF_END_OFFSET = "def_end_offset"
   124   val DEF_END_OFFSET = "def_end_offset"
   127   val DEF_FILE = "def_file"
   125   val DEF_FILE = "def_file"
   128   val DEF_ID = "def_id"
   126   val DEF_ID = "def_id"
   129 
   127 
   130   val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
   128   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   131   val POSITION = "position"
   129   val POSITION = "position"
   132 
   130 
   133 
   131 
   134   /* path */
   132   /* path */
   135 
   133