Lines Matching refs:timestamp
360 | update_b_tstamp t (BinderString {tok,term_name,timestamp}) =
361 BinderString {tok = tok, term_name =term_name, timestamp = t}
364 block_style, timestamp} =
366 block_style = block_style, timestamp = t}
421 timestamp = 0,
429 timestamp = 0,
435 timestamp = 0,
441 timestamp = 0,
450 timestamp = 0,
457 timestamp = 0,
473 timestamp = 0,
542 (* ignore timestamp field *)
750 (#timestamp rr,
789 | BinderString {tok,term_name,timestamp} :: rest =>
792 ((timestamp, GRULE (binder_grule {term_name=term_name,tok=tok})) ::
825 val rr = {term_name = s, elements = pp_elements, timestamp = new_tstamp,
837 timestamp=new_tstamp}]))
848 timestamp = gnext_timestamp G0 }
1503 fun rrule_encode {term_name,elements,timestamp,block_style,paren_style} =
1505 IntData.encode timestamp ::
1510 fun f ((((term_name, timestamp), block_style), paren_style), elements) =
1511 {term_name = term_name, timestamp = timestamp,
1523 | BinderString{tok,term_name,timestamp} =>
1525 IntData.encode timestamp
1527 fun f ((tok,term_name),timestamp) =
1529 timestamp = timestamp}