1structure BoxTypes = 2struct 3 (* Data structures for boxes and their friends. *) 4 open BasicTypes; open FontTypes 5 datatype infOrder = normal | fil | fill | filll 6 datatype glueParam = natural 7 | stretching of (real * infOrder) 8 | shrinking of (real * infOrder) 9 10 type glueSpec = {size: dist, 11 stretch: dist * infOrder, 12 shrink: dist * infOrder} 13 type dim = {width: dist, depth: dist, height: dist} 14 datatype boxkind = HBox | VBox 15 16 datatype node = 17 Char of fontNr * charCode 18 | Box of dist * box (* dist = shift_amount *) 19 | Rule of dim (* no running dimensions! *) 20 | Glue of glueSpec 21 | Kern of dist 22 | Penalty of penalty 23 withtype box = 24 {kind: boxkind, 25 width: dist, 26 depth: dist, 27 height: dist, 28 content: node list, 29 glueParam: glueParam} 30 type hlist = node list 31 type vlist = node list 32 fun Box0 b = Box (0, b) (* creates node with zero shift *) 33 fun HL b = [Box0 b] (* creates horizontal list from box *) 34end (* structure BoxTypes *) 35