equal
deleted
inserted
replaced
108 drawBox(box, g) |
108 drawBox(box, g) |
109 |
109 |
110 } |
110 } |
111 case None => { |
111 case None => { |
112 // Ident |
112 // Ident |
113 val font_var = new Font("CMMI12", Font.PLAIN, CalcUtil.fontsizeOf(box.level)) |
113 if (box.name.forall(c => EditingUtil.isNumber(c) || EditingUtil.isIdentifier(c)) ) { |
114 g.setFont(font_var) |
114 val font_var = new Font("CMMI12", Font.PLAIN, CalcUtil.fontsizeOf(box.level)) |
|
115 g.setFont(font_var) |
|
116 |
|
117 }else { |
|
118 val font_var = new Font("CMCSC8", Font.PLAIN, CalcUtil.fontsizeOf(box.level)) |
|
119 g.setFont(font_var) |
|
120 } |
115 |
121 |
116 g.drawString(box.name, box.x0, box.y0) |
122 g.drawString(box.name, box.x0, box.y0) |
117 drawBox(box, g) |
123 drawBox(box, g) |
118 } |
124 } |
119 } |
125 } |