1signature MATH_GLUE = 2sig 3 val noSkip : MathTypes.mathSpace option 4 val thinSkip : MathTypes.mathSpace option 5 val medSkip : MathTypes.mathSpace option 6 val thickSkip : MathTypes.mathSpace option 7 val thinSkip' : MathTypes.mathSpace option 8 val medSkip' : MathTypes.mathSpace option 9 val thickSkip' : MathTypes.mathSpace option 10end (* signature MATH_GLUE *) 11(*----------*) 12 13structure MathGlue: MATH_GLUE = 14struct 15 open BoxTypes; open MathTypes 16 17 val zeropair = (0, normal) 18 19 val thinGlue = {size = 3, stretch = zeropair, shrink = zeropair} 20 val medGlue = {size = 4, stretch = (2, normal), shrink = (4, normal)} 21 val thickGlue = {size = 5, stretch = (5, normal), shrink = zeropair} 22 23 fun space always g = SOME {isMu = true, always = always, entry = SGlue g} 24 val allstyles = space true 25 val nonscript = space false 26 27 val noSkip = NONE 28 val thinSkip = allstyles thinGlue 29 val medSkip = allstyles medGlue 30 val thickSkip = allstyles thickGlue 31 val thinSkip' = nonscript thinGlue 32 val medSkip' = nonscript medGlue 33 val thickSkip' = nonscript thickGlue 34 35end (* structure MathGlue *) 36