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