src/Pure/General/position.ML
changeset 67280 dfc5a1503916
parent 64556 851ae0e7b09c
child 68172 0f14cf9c632f
equal deleted inserted replaced
67279:d327c11c9f3e 67280:dfc5a1503916
    22   val file_only: string -> T
    22   val file_only: string -> T
    23   val file: string -> T
    23   val file: string -> T
    24   val line_file_only: int -> string -> T
    24   val line_file_only: int -> string -> T
    25   val line_file: int -> string -> T
    25   val line_file: int -> string -> T
    26   val line: int -> T
    26   val line: int -> T
       
    27   val get_props: T -> Properties.T
    27   val id: string -> T
    28   val id: string -> T
    28   val id_only: string -> T
    29   val id_only: string -> T
    29   val get_id: T -> string option
    30   val get_id: T -> string option
    30   val put_id: string -> T -> T
    31   val put_id: string -> T -> T
    31   val parse_id: T -> int option
    32   val parse_id: T -> int option
   129 
   130 
   130 fun line_file_only i name = Pos ((i, 0, 0), file_name name);
   131 fun line_file_only i name = Pos ((i, 0, 0), file_name name);
   131 fun line_file i name = Pos ((i, 1, 0), file_name name);
   132 fun line_file i name = Pos ((i, 1, 0), file_name name);
   132 fun line i = line_file i "";
   133 fun line i = line_file i "";
   133 
   134 
       
   135 fun get_props (Pos (_, props)) = props;
       
   136 
   134 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
   137 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
   135 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
   138 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
   136 
   139 
   137 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
   140 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
   138 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
   141 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));