# HG changeset patch # User wenzelm # Date 1283087351 -7200 # Node ID a9e37daf5bd0538f0cb5e3a0b77401eb9a82727d # Parent f3221fd64426da91422befa9aa253a6f04c901fd added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.; Markup_Tree.select: plain Iterator; misc tuning and simplification; diff -r f3221fd64426 -r a9e37daf5bd0 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Aug 28 22:58:24 2010 +0200 +++ b/src/Pure/PIDE/document.scala Sun Aug 29 15:09:11 2010 +0200 @@ -147,6 +147,8 @@ def convert(range: Text.Range): Text.Range = range.map(convert(_)) def revert(i: Text.Offset): Text.Offset def revert(range: Text.Range): Text.Range = range.map(revert(_)) + def select_markup[A](range: Text.Range) + (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] } object State @@ -275,6 +277,23 @@ def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) + + def select_markup[A](range: Text.Range) + (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] = + { + val former_range = revert(range) + for { + (command, command_start) <- node.command_range(former_range) + Text.Info(r0, x) <- state(command).markup. + select((former_range - command_start).restrict(command.range)) { + case Text.Info(r0, info) + if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) => + result(Text.Info(convert(r0 + command_start), info)) + } { default } + val r = convert(r0 + command_start) + if !r.is_singularity + } yield Text.Info(r, x) + } } } } diff -r f3221fd64426 -r a9e37daf5bd0 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Sat Aug 28 22:58:24 2010 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Sun Aug 29 15:09:11 2010 +0200 @@ -90,7 +90,7 @@ Branches.overlapping(range, branches).toStream def select[A](root_range: Text.Range) - (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] = + (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] = { def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]) : Stream[Text.Info[A]] = @@ -122,6 +122,7 @@ } } stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range)))) + .iterator } def swing_tree(parent: DefaultMutableTreeNode) diff -r f3221fd64426 -r a9e37daf5bd0 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Sat Aug 28 22:58:24 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Sun Aug 29 15:09:11 2010 +0200 @@ -266,7 +266,6 @@ val start = buffer.getLineStartOffset(line) val stop = start + line_segment.count val range = Text.Range(start, stop) - val former_range = snapshot.revert(range) /* FIXME for (text_area <- Isabelle.jedit_text_areas(buffer) @@ -290,14 +289,8 @@ } var next_x = start - for { - (command, command_start) <- snapshot.node.command_range(former_range) - info <- snapshot.state(command).markup. - select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL) - val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start) - if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?) - } - { + for (info <- snapshot.select_markup(range)(token_markup)(Token.NULL)) { + val Text.Range(abs_start, abs_stop) = info.range val token_start = (abs_start - start) max 0 val token_length = (abs_stop - abs_start) - diff -r f3221fd64426 -r a9e37daf5bd0 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Sat Aug 28 22:58:24 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Sun Aug 29 15:09:11 2010 +0200 @@ -189,20 +189,15 @@ override def getToolTipText(x: Int, y: Int): String = { - Swing_Thread.assert() - - val snapshot = model.snapshot() - val offset = snapshot.revert(text_area.xyToOffset(x, y)) - snapshot.node.command_at(offset) match { - case Some((command, command_start)) => - // FIXME Isar_Document.Tooltip extractor - (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) { + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot() + val offset = text_area.xyToOffset(x, y) + val markup = + snapshot.select_markup(Text.Range(offset, offset + 1)) { case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => - val typing = - Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body) - Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40)) - } { null }).head.info - case None => null + Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40)) + } { null } + if (markup.hasNext) markup.next.info else null } } } diff -r f3221fd64426 -r a9e37daf5bd0 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sat Aug 28 22:58:24 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Aug 29 15:09:11 2010 +0200 @@ -45,38 +45,35 @@ Document_Model(buffer) match { case Some(model) => val snapshot = model.snapshot() - val offset = snapshot.revert(buffer_offset) - snapshot.node.command_at(offset) match { - case Some((command, command_start)) => + val markup = + snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) { // FIXME Isar_Document.Hyperlink extractor - (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) { - case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _), - List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) => - val Text.Range(begin, end) = snapshot.convert(info_range + command_start) - val line = buffer.getLineOfOffset(begin) + case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _), + List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) => + val Text.Range(begin, end) = info_range + val line = buffer.getLineOfOffset(begin) + (Position.File.unapply(props), Position.Line.unapply(props)) match { + case (Some(ref_file), Some(ref_line)) => + new External_Hyperlink(begin, end, line, ref_file, ref_line) + case _ => + (props, props) match { + case (Position.Id(ref_id), Position.Offset(ref_offset)) => + snapshot.lookup_command(ref_id) match { + case Some(ref_cmd) => + snapshot.node.command_start(ref_cmd) match { + case Some(ref_cmd_start) => + new Internal_Hyperlink(begin, end, line, + snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset))) + case None => null + } + case None => null + } + case _ => null + } + } + } { null } + if (markup.hasNext) markup.next.info else null - (Position.File.unapply(props), Position.Line.unapply(props)) match { - case (Some(ref_file), Some(ref_line)) => - new External_Hyperlink(begin, end, line, ref_file, ref_line) - case _ => - (Position.Id.unapply(props), Position.Offset.unapply(props)) match { - case (Some(ref_id), Some(ref_offset)) => - snapshot.lookup_command(ref_id) match { - case Some(ref_cmd) => - snapshot.node.command_start(ref_cmd) match { - case Some(ref_cmd_start) => - new Internal_Hyperlink(begin, end, line, - snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset))) - case None => null - } - case None => null - } - case _ => null - } - } - } { null }).head.info - case None => null - } case None => null } }