# HG changeset patch # User wenzelm # Date 1321096902 -3600 # Node ID 33e946d3f44959316ec242b62601402047062821 # Parent 3f290b6288cf7992cb1298ac2ae943f1115e6d74 tuned signature; express select in terms of cumulate; diff -r 3f290b6288cf -r 33e946d3f449 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Nov 12 11:45:49 2011 +0100 +++ b/src/Pure/PIDE/document.scala Sat Nov 12 12:21:42 2011 +0100 @@ -241,7 +241,7 @@ def revert(i: Text.Offset): Text.Offset def revert(range: Text.Range): Text.Range def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]] - def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A]) + def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A]) : Stream[Text.Info[Option[A]]] } @@ -492,19 +492,16 @@ } yield Text.Info(convert(r0 + command_start), a) } - def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A]) + def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A]) : Stream[Text.Info[Option[A]]] = { - val former_range = revert(range) - for { - (command, command_start) <- node.command_range(former_range).toStream - Text.Info(r0, x) <- command_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)) - } - } yield Text.Info(convert(r0 + command_start), x) + val result = body.result + val result1 = + new PartialFunction[(Option[A], Text.Markup), Option[A]] { + def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2) + def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2)) + } + cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1)) } } } diff -r 3f290b6288cf -r 33e946d3f449 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Sat Nov 12 11:45:49 2011 +0100 +++ b/src/Pure/PIDE/markup_tree.scala Sat Nov 12 12:21:42 2011 +0100 @@ -16,7 +16,7 @@ object Markup_Tree { sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A]) - type Select[A] = PartialFunction[Text.Markup, A] + sealed case class Select[A](result: PartialFunction[Text.Markup, A]) val empty: Markup_Tree = new Markup_Tree(Branches.empty) @@ -124,43 +124,6 @@ List((Text.Info(root_range, root_info), overlapping(root_range).toStream))) } - def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] = - { - def stream( - last: Text.Offset, - stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])]) - : Stream[Text.Info[Option[A]]] = - { - stack match { - case (parent, (range, (info, tree)) #:: more) :: rest => - val subrange = range.restrict(root_range) - val subtree = tree.overlapping(subrange).toStream - val start = subrange.start - - if (result.isDefinedAt(info)) { - val next = Text.Info[Option[A]](subrange, Some(result(info))) - val nexts = stream(start, (next, subtree) :: (parent, more) :: rest) - if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts - else nexts - } - else stream(last, (parent, subtree #::: more) :: rest) - - case (parent, Stream.Empty) :: rest => - val stop = parent.range.stop - val nexts = stream(stop, rest) - if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts - else nexts - - case Nil => - val stop = root_range.stop - if (last < stop) Stream(Text.Info(Text.Range(last, stop), None)) - else Stream.empty - } - } - stream(root_range.start, - List((Text.Info(root_range, None), overlapping(root_range).toStream))) - } - def swing_tree(parent: DefaultMutableTreeNode) (swing_node: Text.Markup => DefaultMutableTreeNode) { diff -r 3f290b6288cf -r 33e946d3f449 src/Tools/jEdit/src/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Sat Nov 12 11:45:49 2011 +0100 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Sat Nov 12 12:21:42 2011 +0100 @@ -57,37 +57,39 @@ case Some(model) => val snapshot = model.snapshot() val markup = - snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) { - // FIXME Isar_Document.Hyperlink extractor - case Text.Info(info_range, - XML.Elem(Markup(Markup.ENTITY, props), _)) - if (props.find( - { case (Markup.KIND, Markup.ML_OPEN) => true - case (Markup.KIND, Markup.ML_STRUCT) => true - case _ => false }).isEmpty) => - val Text.Range(begin, end) = info_range - val line = buffer.getLineOfOffset(begin) - (Position.File.unapply(props), Position.Line.unapply(props)) match { - case (Some(def_file), Some(def_line)) => - new External_Hyperlink(begin, end, line, def_file, def_line) - case _ if !snapshot.is_outdated => - (props, props) match { - case (Position.Id(def_id), Position.Offset(def_offset)) => - snapshot.state.find_command(snapshot.version, def_id) match { - case Some((def_node, def_cmd)) => - def_node.command_start(def_cmd) match { - case Some(def_cmd_start) => - new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line, - def_cmd_start + def_cmd.decode(def_offset)) + snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))( + Markup_Tree.Select[Hyperlink]( + { + // FIXME Isar_Document.Hyperlink extractor + case Text.Info(info_range, + XML.Elem(Markup(Markup.ENTITY, props), _)) + if (props.find( + { case (Markup.KIND, Markup.ML_OPEN) => true + case (Markup.KIND, Markup.ML_STRUCT) => true + case _ => false }).isEmpty) => + val Text.Range(begin, end) = info_range + val line = buffer.getLineOfOffset(begin) + (Position.File.unapply(props), Position.Line.unapply(props)) match { + case (Some(def_file), Some(def_line)) => + new External_Hyperlink(begin, end, line, def_file, def_line) + case _ if !snapshot.is_outdated => + (props, props) match { + case (Position.Id(def_id), Position.Offset(def_offset)) => + snapshot.state.find_command(snapshot.version, def_id) match { + case Some((def_node, def_cmd)) => + def_node.command_start(def_cmd) match { + case Some(def_cmd_start) => + new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line, + def_cmd_start + def_cmd.decode(def_offset)) + case None => null + } case None => null } - case None => null + case _ => null } case _ => null } - case _ => null - } - } + })) markup match { case Text.Info(_, Some(link)) #:: _ => link case _ => null diff -r 3f290b6288cf -r 33e946d3f449 src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Sat Nov 12 11:45:49 2011 +0100 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Sat Nov 12 12:21:42 2011 +0100 @@ -87,12 +87,13 @@ /* markup selectors */ - val message: Markup_Tree.Select[Color] = - { - case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color - case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color - case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color - } + val message = + Markup_Tree.Select[Color]( + { + case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color + case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color + case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color + }) val tooltip_message = Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty, @@ -103,33 +104,37 @@ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))) }) - val gutter_message: Markup_Tree.Select[Icon] = - { - case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) => - body match { - case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon - case _ => warning_icon - } - case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon - } + val gutter_message = + Markup_Tree.Select[Icon]( + { + case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) => + body match { + case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon + case _ => warning_icon + } + case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon + }) - val background1: Markup_Tree.Select[Color] = - { - case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color - case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color - } + val background1 = + Markup_Tree.Select[Color]( + { + case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color + case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color + }) - val background2: Markup_Tree.Select[Color] = - { - case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color - } + val background2 = + Markup_Tree.Select[Color]( + { + case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color + }) - val foreground: Markup_Tree.Select[Color] = - { - case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color - case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color - case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color - } + val foreground = + Markup_Tree.Select[Color]( + { + case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color + case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color + case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color + }) private val text_colors: Map[String, Color] = Map( @@ -156,10 +161,11 @@ Markup.ML_MALFORMED -> get_color("#FF6A6A"), Markup.ANTIQ -> get_color("blue")) - val text_color: Markup_Tree.Select[Color] = - { - case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m) - } + val text_color = + Markup_Tree.Select[Color]( + { + case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m) + }) private val tooltips: Map[String, String] = Map( @@ -181,29 +187,32 @@ Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)), margin = Isabelle.Int_Property("tooltip-margin")) - val tooltip1: Markup_Tree.Select[String] = - { - case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name) - case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body) - case Text.Info(_, XML.Elem(Markup(name, _), _)) - if tooltips.isDefinedAt(name) => tooltips(name) - } + val tooltip1 = + Markup_Tree.Select[String]( + { + case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name) + case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body) + case Text.Info(_, XML.Elem(Markup(name, _), _)) + if tooltips.isDefinedAt(name) => tooltips(name) + }) - val tooltip2: Markup_Tree.Select[String] = - { - case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body) - } + val tooltip2 = + Markup_Tree.Select[String]( + { + case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body) + }) private val subexp_include = Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE) - val subexp: Markup_Tree.Select[(Text.Range, Color)] = - { - case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => - (range, subexp_color) - } + val subexp = + Markup_Tree.Select[(Text.Range, Color)]( + { + case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => + (range, subexp_color) + }) /* token markup -- text styles */