src/Pure/General/position.ML
changeset 62940 a03592aafadf
parent 62929 b92565f98206
child 63806 c54a53ef1873
equal deleted inserted replaced
62939:ef8d840f39fb 62940:a03592aafadf
     5 *)
     5 *)
     6 
     6 
     7 signature POSITION =
     7 signature POSITION =
     8 sig
     8 sig
     9   eqtype T
     9   eqtype T
    10   val make: {line: int, offset: int, end_offset: int, props: Properties.T} -> T
    10   val make: Thread_Position.T -> T
    11   val dest: T -> {line: int, offset: int, end_offset: int, props: Properties.T}
    11   val dest: T -> Thread_Position.T
    12   val line_of: T -> int option
    12   val line_of: T -> int option
    13   val offset_of: T -> int option
    13   val offset_of: T -> int option
    14   val end_offset_of: T -> int option
    14   val end_offset_of: T -> int option
    15   val file_of: T -> string option
    15   val file_of: T -> string option
    16   val advance: Symbol.symbol -> T -> T
    16   val advance: Symbol.symbol -> T -> T
   241   properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
   241   properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
   242 
   242 
   243 
   243 
   244 (* thread data *)
   244 (* thread data *)
   245 
   245 
   246 val thread_data = of_properties o Thread_Position.get;
   246 val thread_data = make o Thread_Position.get;
   247 fun setmp_thread_data pos = Thread_Position.setmp (properties_of pos);
   247 fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
   248 
   248 
   249 fun default pos =
   249 fun default pos =
   250   if pos = none then (false, thread_data ())
   250   if pos = none then (false, thread_data ())
   251   else (true, pos);
   251   else (true, pos);
   252 
   252