Lines Matching refs:depth
625 pgrav lgrav rgrav depth apps =
631 depth
635 fun sysprint { gravs = (pg,lg,rg), binderp, depth} tm =
637 pg lg rg depth
643 depth tm
655 pgrav lgrav rgrav depth apps =
723 type_pp.pp_type_with_depth TyG backend (decdepth depth) ty
768 | RE TM => (pr_term (hd args) Top Top Top (decdepth depth) >>
772 pr_term (hd args) cprec lprec cprec (decdepth depth) >>
775 pr_term (hd args) cprec cprec rprec (decdepth depth) >>
791 fun lrecurse depth tm = let
798 if depth = 0 then add_string "..."
801 pr_term head Top Top Top (decdepth depth)
804 pr_term head Top Top Top (decdepth depth) >>
806 lrecurse (decdepth depth) tail
810 lrecurse depth t
833 (pr_t tm Top Top Top (decdepth depth))
845 pr_term Restrictor Top Top Top (decdepth depth) >>
911 pr_term restrictor Top Top Top (decdepth depth)
917 (pr_term body Top Top Top (decdepth depth)))
947 (pr_term b Top Top Top (decdepth depth)))
1047 pr_term t2 prec lprec prec (decdepth depth) >>
1119 fun print_update depth (fld, value, normal_upd) = let
1130 pr_term value upd_prec upd_prec Top (decdepth depth))
1133 fun recurse depth upds =
1134 if depth = 0 then add_string "..."
1138 | [u] => print_update (decdepth depth) u
1139 | u::us => (print_update (decdepth depth) u >>
1141 recurse (decdepth depth) us)
1146 recurse depth updates >>
1168 pr_term base with_grav lprec with_grav (decdepth depth) >>
1172 (if length updates = 1 then print_update depth (hd updates)
1246 prec lprec prec (decdepth depth) >>
1249 prec prec rprec (decdepth depth) >>
1491 if depth = 0 then add_string "..."
1761 pr_term oif pgrav lgrav rgrav depth
1843 pr_term l Top Top Top (decdepth depth) >>
1847 (pr_term r Top Top rprec (decdepth depth)))
1853 pr_term split_on Top Top Top (decdepth depth) >>