79 private def bold_style(style: SyntaxStyle): SyntaxStyle = |
79 private def bold_style(style: SyntaxStyle): SyntaxStyle = |
80 font_style(style, _.deriveFont(Font.BOLD)) |
80 font_style(style, _.deriveFont(Font.BOLD)) |
81 |
81 |
82 class Style_Extender extends SyntaxUtilities.StyleExtender |
82 class Style_Extender extends SyntaxUtilities.StyleExtender |
83 { |
83 { |
84 val symbols = Isabelle_System.symbols |
84 if (Symbol.font_names.length > 2) |
85 if (symbols.font_names.length > 2) |
85 error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", ")) |
86 error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", ")) |
|
87 |
86 |
88 override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = |
87 override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = |
89 { |
88 { |
90 val new_styles = new Array[SyntaxStyle](full_range) |
89 val new_styles = new Array[SyntaxStyle](full_range) |
91 for (i <- 0 until plain_range) { |
90 for (i <- 0 until plain_range) { |
92 val style = styles(i) |
91 val style = styles(i) |
93 new_styles(i) = style |
92 new_styles(i) = style |
94 new_styles(subscript(i.toByte)) = script_style(style, -1) |
93 new_styles(subscript(i.toByte)) = script_style(style, -1) |
95 new_styles(superscript(i.toByte)) = script_style(style, 1) |
94 new_styles(superscript(i.toByte)) = script_style(style, 1) |
96 new_styles(bold(i.toByte)) = bold_style(style) |
95 new_styles(bold(i.toByte)) = bold_style(style) |
97 for ((family, idx) <- symbols.font_index) |
96 for ((family, idx) <- Symbol.font_index) |
98 new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _)) |
97 new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _)) |
99 } |
98 } |
100 new_styles(hidden) = |
99 new_styles(hidden) = |
101 new SyntaxStyle(Color.white, null, |
100 new SyntaxStyle(Color.white, null, |
102 { val font = styles(0).getFont |
101 { val font = styles(0).getFont |
106 } |
105 } |
107 } |
106 } |
108 |
107 |
109 def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] = |
108 def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] = |
110 { |
109 { |
111 val symbols = Isabelle_System.symbols |
110 // FIXME Symbol.is_bsub_decoded etc. |
112 |
|
113 // FIXME symbols.bsub_decoded etc. |
|
114 def ctrl_style(sym: String): Option[Byte => Byte] = |
111 def ctrl_style(sym: String): Option[Byte => Byte] = |
115 if (symbols.is_subscript_decoded(sym)) Some(subscript(_)) |
112 if (Symbol.is_subscript_decoded(sym)) Some(subscript(_)) |
116 else if (symbols.is_superscript_decoded(sym)) Some(superscript(_)) |
113 else if (Symbol.is_superscript_decoded(sym)) Some(superscript(_)) |
117 else if (sym == symbols.bold_decoded) Some(bold(_)) |
114 else if (Symbol.is_bold_decoded(sym)) Some(bold(_)) |
118 else None |
115 else None |
119 |
116 |
120 var result = Map[Text.Offset, Byte => Byte]() |
117 var result = Map[Text.Offset, Byte => Byte]() |
121 def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte) |
118 def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte) |
122 { |
119 { |
125 var offset = 0 |
122 var offset = 0 |
126 var ctrl = "" |
123 var ctrl = "" |
127 for (sym <- Symbol.iterator(text)) { |
124 for (sym <- Symbol.iterator(text)) { |
128 if (ctrl_style(sym).isDefined) ctrl = sym |
125 if (ctrl_style(sym).isDefined) ctrl = sym |
129 else if (ctrl != "") { |
126 else if (ctrl != "") { |
130 if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) { |
127 if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) { |
131 mark(offset - ctrl.length, offset, _ => hidden) |
128 mark(offset - ctrl.length, offset, _ => hidden) |
132 mark(offset, offset + sym.length, ctrl_style(ctrl).get) |
129 mark(offset, offset + sym.length, ctrl_style(ctrl).get) |
133 } |
130 } |
134 ctrl = "" |
131 ctrl = "" |
135 } |
132 } |
136 symbols.lookup_font(sym) match { |
133 Symbol.lookup_font(sym) match { |
137 case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _)) |
134 case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _)) |
138 case _ => |
135 case _ => |
139 } |
136 } |
140 offset += sym.length |
137 offset += sym.length |
141 } |
138 } |