39 else Markup.no_output; |
39 else Markup.no_output; |
40 val (bg2, en2) = |
40 val (bg2, en2) = |
41 if null ts then Markup.no_output |
41 if null ts then Markup.no_output |
42 else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") |
42 else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") |
43 else if name = Markup.sendbackN then (special "W", special "X") |
43 else if name = Markup.sendbackN then (special "W", special "X") |
44 else if name = Markup.bindingN then (special "F", special "A") |
44 else if name = Markup.bindingN then (special "B", special "A") |
45 else if name = Markup.hiliteN then (special "0", special "1") |
45 else if name = Markup.hiliteN then (special "0", special "1") |
46 else if name = Markup.tfreeN then (special "C", special "A") |
46 else if name = Markup.tfreeN then (special "C", special "A") |
47 else if name = Markup.tvarN then (special "D", special "A") |
47 else if name = Markup.tvarN then (special "D", special "A") |
48 else if name = Markup.freeN then (special "E", special "A") |
48 else if name = Markup.freeN then (special "E", special "A") |
49 else if name = Markup.boundN then (special "F", special "A") |
49 else if name = Markup.boundN then (special "F", special "A") |