# HG changeset patch # User wenzelm # Date 1282474452 -7200 # Node ID 0fe2c01ef7da40763cd8e876e94b99f20c687c70 # Parent f7d7b805464841eb68d3a50030fb20905e29aecd Command.State: accumulate markup reports uniformly; Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo; tuned; diff -r f7d7b8054648 -r 0fe2c01ef7da src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Aug 20 22:35:01 2010 +0200 +++ b/src/Pure/PIDE/command.scala Sun Aug 22 12:54:12 2010 +0200 @@ -14,9 +14,6 @@ object Command { - case class HighlightInfo(kind: String, sub_kind: Option[String]) { - override def toString = kind - } case class TypeInfo(ty: String) case class RefInfo(file: Option[String], line: Option[Int], command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !? @@ -46,14 +43,6 @@ /* markup */ - lazy val highlight: List[Markup_Tree.Node[Any]] = - { - markup.filter(_.info match { - case Command.HighlightInfo(_, _) => true - case _ => false - }).flatten(markup_root_node) - } - private lazy val types: List[Markup_Tree.Node[Any]] = markup.filter(_.info match { case Command.TypeInfo(_) => true @@ -85,38 +74,16 @@ def accumulate(message: XML.Tree): Command.State = message match { case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status) - - case XML.Elem(Markup(Markup.REPORT, _), elems) => - (this /: elems)((state, elem) => - elem match { - case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => - atts match { - case Position.Range(range) => - if (kind == Markup.ML_TYPING) { - val info = Pretty.string_of(body, margin = 40) - state.add_markup(command.decode_range(range, Command.TypeInfo(info))) - } - else if (kind == Markup.ML_REF) { - body match { - case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) => - state.add_markup( - command.decode_range(range, - Command.RefInfo( - Position.get_file(props), - Position.get_line(props), - Position.get_id(props), - Position.get_offset(props)))) - case _ => state - } - } - else { - state.add_markup( - command.decode_range(range, - Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) - } - case _ => state - } - case _ => System.err.println("Ignored report message: " + elem); state + case XML.Elem(Markup(Markup.REPORT, _), msgs) => + (this /: msgs)((state, msg) => + msg match { + case XML.Elem(Markup(name, atts), args) + if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined => + val range = command.decode_range(Position.get_range(atts).get) + val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) + val node = Markup_Tree.Node[Any](range, XML.Elem(Markup(name, props), args)) + add_markup(node) + case _ => System.err.println("Ignored report message: " + msg); state }) case _ => add_result(message) } @@ -152,15 +119,11 @@ val source: String = span.map(_.source).mkString def source(range: Text.Range): String = source.substring(range.start, range.stop) def length: Int = source.length + val range: Text.Range = Text.Range(0, length) lazy val symbol_index = new Symbol.Index(source) - - - /* markup */ - - def decode_range(range: Text.Range, info: Any): Markup_Tree.Node[Any] = - new Markup_Tree.Node(symbol_index.decode(range), info) + def decode_range(r: Text.Range): Text.Range = symbol_index.decode(r) /* accumulated results */ diff -r f7d7b8054648 -r 0fe2c01ef7da src/Tools/jEdit/src/jedit/document_model.scala --- 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)