159 class Marker extends TokenMarker |
159 class Marker extends TokenMarker |
160 { |
160 { |
161 override def markTokens(context: TokenMarker.LineContext, |
161 override def markTokens(context: TokenMarker.LineContext, |
162 handler: TokenHandler, line: Segment): TokenMarker.LineContext = |
162 handler: TokenHandler, line: Segment): TokenMarker.LineContext = |
163 { |
163 { |
164 val symbols = Isabelle.system.symbols |
164 val context1 = |
165 val syntax = Isabelle.session.current_syntax() |
165 if (Isabelle.session.is_ready) { |
166 |
166 val symbols = Isabelle.system.symbols |
167 val ctxt = |
167 val syntax = Isabelle.session.current_syntax() |
168 context match { |
168 |
169 case c: Line_Context => c.context |
169 val ctxt = |
170 case _ => Scan.Finished |
170 context match { |
|
171 case c: Line_Context => c.context |
|
172 case _ => Scan.Finished |
|
173 } |
|
174 val (tokens, ctxt1) = syntax.scan_context(line, ctxt) |
|
175 val context1 = new Line_Context(ctxt1) |
|
176 |
|
177 val extended = extended_styles(symbols, line) |
|
178 |
|
179 var offset = 0 |
|
180 for (token <- tokens) { |
|
181 val style = Isabelle_Markup.token_markup(syntax, token) |
|
182 val length = token.source.length |
|
183 val end_offset = offset + length |
|
184 if ((offset until end_offset) exists extended.isDefinedAt) { |
|
185 for (i <- offset until end_offset) { |
|
186 val style1 = |
|
187 extended.get(i) match { |
|
188 case None => style |
|
189 case Some(ext) => ext(style) |
|
190 } |
|
191 handler.handleToken(line, style1, i, 1, context1) |
|
192 } |
|
193 } |
|
194 else handler.handleToken(line, style, offset, length, context1) |
|
195 offset += length |
|
196 } |
|
197 handler.handleToken(line, JEditToken.END, line.count, 0, context1) |
|
198 context1 |
171 } |
199 } |
172 val (tokens, ctxt1) = syntax.scan_context(line, ctxt) |
200 else { |
173 val context1 = new Line_Context(ctxt1) |
201 val context1 = new Line_Context(Scan.Finished) |
174 |
202 handler.handleToken(line, JEditToken.NULL, 0, line.count, context1) |
175 val extended = extended_styles(symbols, line) |
203 handler.handleToken(line, JEditToken.END, line.count, 0, context1) |
176 |
204 context1 |
177 var offset = 0 |
|
178 for (token <- tokens) { |
|
179 val style = Isabelle_Markup.token_markup(syntax, token) |
|
180 val length = token.source.length |
|
181 val end_offset = offset + length |
|
182 if ((offset until end_offset) exists extended.isDefinedAt) { |
|
183 for (i <- offset until end_offset) { |
|
184 val style1 = |
|
185 extended.get(i) match { |
|
186 case None => style |
|
187 case Some(ext) => ext(style) |
|
188 } |
|
189 handler.handleToken(line, style1, i, 1, context1) |
|
190 } |
|
191 } |
205 } |
192 else handler.handleToken(line, style, offset, length, context1) |
|
193 offset += length |
|
194 } |
|
195 handler.handleToken(line, JEditToken.END, line.count, 0, context1) |
|
196 |
|
197 val context2 = context1.intern |
206 val context2 = context1.intern |
198 handler.setLineContext(context2) |
207 handler.setLineContext(context2) |
199 context2 |
208 context2 |
200 } |
209 } |
201 } |
210 } |