added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
Markup_Tree.select: plain Iterator;
misc tuning and simplification;
--- 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)
+ }
}
}
}
--- 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)
--- 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) -
--- 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
}
}
}
--- 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
}
}