--- a/src/Tools/jEdit/src/jedit/document_model.scala Fri Aug 20 22:35:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sun Aug 22 12:54:12 2010 +0200
@@ -257,14 +257,17 @@
override def markTokens(prev: TokenMarker.LineContext,
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
{
+ // FIXME proper synchronization / thread context (!??)
+ val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+
val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
val line = if (prev == null) 0 else previous.line + 1
val context = new Document_Model.Token_Markup.LineContext(line, previous)
+
val start = buffer.getLineStartOffset(line)
val stop = start + line_segment.count
-
- // FIXME proper synchronization / thread context (!??)
- val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+ val range = Text.Range(start, stop)
+ val former_range = snapshot.revert(range)
/* FIXME
for (text_area <- Isabelle.jedit_text_areas(buffer)
@@ -275,35 +278,39 @@
def handle_token(style: Byte, offset: Text.Offset, length: Int) =
handler.handleToken(line_segment, style, offset, length, context)
+ val syntax = session.current_syntax()
+ val token_markup: PartialFunction[Any, Byte] =
+ {
+ case XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)
+ if syntax.keyword_kind(name).isDefined =>
+ Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
+
+ case XML.Elem(Markup(name, _), _)
+ if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
+ Document_Model.Token_Markup.token_style(name)
+ }
+
var next_x = start
for {
- (command, command_start) <-
- snapshot.node.command_range(snapshot.revert(Text.Range(start, stop)))
- markup <- snapshot.state(command).highlight
- val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
- if (abs_stop > start)
- if (abs_start < stop)
+ (command, command_start) <- snapshot.node.command_range(former_range)
+ val root_node =
+ Markup_Tree.Node((former_range - command_start).restrict(command.range), Token.NULL)
+ node <- snapshot.state(command).markup.select(root_node)(token_markup)
+ val Text.Range(abs_start, abs_stop) = snapshot.convert(node.range + command_start)
+ if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?)
+ }
+ {
val token_start = (abs_start - start) max 0
val token_length =
(abs_stop - abs_start) -
((start - abs_start) max 0) -
((abs_stop - stop) max 0)
- }
- {
- val token_type =
- markup.info match {
- case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
- Document_Model.Token_Markup.command_style(kind)
- case Command.HighlightInfo(kind, _) =>
- Document_Model.Token_Markup.token_style(kind)
- case _ => Token.NULL
- }
- if (start + token_start > next_x)
+ if (start + token_start > next_x) // FIXME ??
handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
- handle_token(token_type, token_start, token_length)
+ handle_token(node.info, token_start, token_length)
next_x = start + token_start + token_length
}
- if (next_x < stop)
+ if (next_x < stop) // FIXME ??
handle_token(Token.COMMENT1, next_x - start, stop - next_x)
handle_token(Token.END, line_segment.count, 0)