equal
deleted
inserted
replaced
79 } |
79 } |
80 new_styles |
80 new_styles |
81 } |
81 } |
82 } |
82 } |
83 |
83 |
84 object Extender extends SyntaxUtilities.StyleExtender |
84 object Main_Extender extends SyntaxUtilities.StyleExtender |
85 { |
85 { |
86 val max_user_fonts = 2 |
86 val max_user_fonts = 2 |
87 if (Symbol.font_names.length > max_user_fonts) |
87 if (Symbol.font_names.length > max_user_fonts) |
88 error("Too many user symbol fonts (" + max_user_fonts + " permitted): " + |
88 error("Too many user symbol fonts (" + max_user_fonts + " permitted): " + |
89 Symbol.font_names.mkString(", ")) |
89 Symbol.font_names.mkString(", ")) |