src/Pure/General/markup.ML
changeset 44581 7270ae921cf2
parent 44563 85388f5570c4
child 44624 c70bd78ec83c
equal deleted inserted replaced
44580:717e96cf9527 44581:7270ae921cf2
    19   val entityN: string val entity: string -> string -> T
    19   val entityN: string val entity: string -> string -> T
    20   val get_entity_kind: T -> string option
    20   val get_entity_kind: T -> string option
    21   val defN: string
    21   val defN: string
    22   val refN: string
    22   val refN: string
    23   val lineN: string
    23   val lineN: string
    24   val columnN: string
       
    25   val offsetN: string
    24   val offsetN: string
    26   val end_offsetN: string
    25   val end_offsetN: string
    27   val fileN: string
    26   val fileN: string
    28   val idN: string
    27   val idN: string
    29   val position_properties': string list
    28   val position_properties': string list
   184 
   183 
   185 
   184 
   186 (* position *)
   185 (* position *)
   187 
   186 
   188 val lineN = "line";
   187 val lineN = "line";
   189 val columnN = "column";
       
   190 val offsetN = "offset";
   188 val offsetN = "offset";
   191 val end_offsetN = "end_offset";
   189 val end_offsetN = "end_offset";
   192 val fileN = "file";
   190 val fileN = "file";
   193 val idN = "id";
   191 val idN = "id";
   194 
   192 
   195 val position_properties' = [fileN, idN];
   193 val position_properties' = [fileN, idN];
   196 val position_properties = [lineN, columnN, offsetN, end_offsetN] @ position_properties';
   194 val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
   197 
   195 
   198 val (positionN, position) = markup_elem "position";
   196 val (positionN, position) = markup_elem "position";
   199 
   197 
   200 
   198 
   201 (* path *)
   199 (* path *)