index markup elements for more efficient cumulate/select operations;
authorwenzelm
Sat Nov 12 19:44:56 2011 +0100 (2011-11-12 ago)
changeset 45474f793dd5d84b2
parent 45473 66395afbd915
child 45476 6f9e24376ffd
index markup elements for more efficient cumulate/select operations;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_markup.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Nov 12 18:56:49 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Nov 12 19:44:56 2011 +0100
     1.3 @@ -488,7 +488,8 @@
     1.4                      case (a, Text.Info(r0, b))
     1.5                      if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
     1.6                        result((a, Text.Info(convert(r0 + command_start), b)))
     1.7 -                  }))
     1.8 +                  },
     1.9 +                  body.elements))
    1.10            } yield Text.Info(convert(r0 + command_start), a)
    1.11          }
    1.12  
    1.13 @@ -501,7 +502,7 @@
    1.14                def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
    1.15                def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
    1.16              }
    1.17 -          cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1))
    1.18 +          cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1, body.elements))
    1.19          }
    1.20        }
    1.21      }
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 18:56:49 2011 +0100
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 19:44:56 2011 +0100
     2.3 @@ -15,20 +15,29 @@
     2.4  
     2.5  object Markup_Tree
     2.6  {
     2.7 -  sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A])
     2.8 -  sealed case class Select[A](result: PartialFunction[Text.Markup, A])
     2.9 +  sealed case class Cumulate[A](
    2.10 +    info: A, result: PartialFunction[(A, Text.Markup), A], elements: Option[Set[String]])
    2.11 +  sealed case class Select[A](
    2.12 +    result: PartialFunction[Text.Markup, A], elements: Option[Set[String]])
    2.13  
    2.14    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    2.15  
    2.16    object Entry
    2.17    {
    2.18      def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
    2.19 -      Entry(markup.range, List(markup.info), subtree)
    2.20 +      Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
    2.21    }
    2.22  
    2.23 -  sealed case class Entry(range: Text.Range, rev_markup: List[XML.Elem], subtree: Markup_Tree)
    2.24 +  sealed case class Entry(
    2.25 +    range: Text.Range,
    2.26 +    rev_markup: List[XML.Elem],
    2.27 +    elements: Set[String],
    2.28 +    subtree: Markup_Tree)
    2.29    {
    2.30 -    def + (m: XML.Elem): Entry = copy(rev_markup = m :: rev_markup)
    2.31 +    def + (info: XML.Elem): Entry =
    2.32 +      if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup)
    2.33 +      else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
    2.34 +
    2.35      def markup: List[XML.Elem] = rev_markup.reverse
    2.36    }
    2.37  
    2.38 @@ -102,17 +111,18 @@
    2.39      val root_info = body.info
    2.40  
    2.41      def result(x: A, entry: Entry): Option[A] =
    2.42 -    {
    2.43 -      val (y, changed) =
    2.44 -        (entry.markup :\ (x, false))((info, res) =>
    2.45 -          {
    2.46 -            val (y, changed) = res
    2.47 -            val arg = (x, Text.Info(entry.range, info))
    2.48 -            if (body.result.isDefinedAt(arg)) (body.result(arg), true)
    2.49 -            else res
    2.50 -          })
    2.51 -      if (changed) Some(y) else None
    2.52 -    }
    2.53 +      if (body.elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
    2.54 +        val (y, changed) =
    2.55 +          (entry.markup :\ (x, false))((info, res) =>
    2.56 +            {
    2.57 +              val (y, changed) = res
    2.58 +              val arg = (x, Text.Info(entry.range, info))
    2.59 +              if (body.result.isDefinedAt(arg)) (body.result(arg), true)
    2.60 +              else res
    2.61 +            })
    2.62 +        if (changed) Some(y) else None
    2.63 +      }
    2.64 +      else None
    2.65  
    2.66      def stream(
    2.67        last: Text.Offset,
     3.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 18:56:49 2011 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 19:44:56 2011 +0100
     3.3 @@ -89,7 +89,8 @@
     3.4                          }
     3.5                        case _ => null
     3.6                      }
     3.7 -                }))
     3.8 +                },
     3.9 +                Some(Set(Markup.ENTITY))))
    3.10            markup match {
    3.11              case Text.Info(_, Some(link)) #:: _ => link
    3.12              case _ => null
     4.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 18:56:49 2011 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 19:44:56 2011 +0100
     4.3 @@ -89,11 +89,12 @@
     4.4  
     4.5    val message =
     4.6      Markup_Tree.Select[Color](
     4.7 -    {
     4.8 -      case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
     4.9 -      case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    4.10 -      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    4.11 -    })
    4.12 +      {
    4.13 +        case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    4.14 +        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    4.15 +        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    4.16 +      },
    4.17 +      Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
    4.18  
    4.19    val tooltip_message =
    4.20      Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
    4.21 @@ -102,7 +103,8 @@
    4.22          if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
    4.23            msgs + (serial ->
    4.24              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
    4.25 -      })
    4.26 +      },
    4.27 +      Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
    4.28  
    4.29    val gutter_message =
    4.30      Markup_Tree.Select[Icon](
    4.31 @@ -113,20 +115,23 @@
    4.32              case _ => warning_icon
    4.33            }
    4.34          case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
    4.35 -      })
    4.36 +      },
    4.37 +      Some(Set(Markup.WARNING, Markup.ERROR)))
    4.38  
    4.39    val background1 =
    4.40      Markup_Tree.Select[Color](
    4.41        {
    4.42          case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
    4.43          case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
    4.44 -      })
    4.45 +      },
    4.46 +      Some(Set(Markup.BAD, Markup.HILITE)))
    4.47  
    4.48    val background2 =
    4.49      Markup_Tree.Select[Color](
    4.50        {
    4.51          case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
    4.52 -      })
    4.53 +      },
    4.54 +      Some(Set(Markup.TOKEN_RANGE)))
    4.55  
    4.56    val foreground =
    4.57      Markup_Tree.Select[Color](
    4.58 @@ -134,7 +139,8 @@
    4.59          case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
    4.60          case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
    4.61          case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
    4.62 -      })
    4.63 +      },
    4.64 +      Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)))
    4.65  
    4.66    private val text_colors: Map[String, Color] =
    4.67      Map(
    4.68 @@ -164,8 +170,10 @@
    4.69    val text_color =
    4.70      Markup_Tree.Select[Color](
    4.71        {
    4.72 -        case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
    4.73 -      })
    4.74 +        case Text.Info(_, XML.Elem(Markup(m, _), _))
    4.75 +        if text_colors.isDefinedAt(m) => text_colors(m)
    4.76 +      },
    4.77 +      Some(Set() ++ text_colors.keys))
    4.78  
    4.79    private val tooltips: Map[String, String] =
    4.80      Map(
    4.81 @@ -191,16 +199,19 @@
    4.82      Markup_Tree.Select[String](
    4.83        {
    4.84          case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
    4.85 -        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
    4.86 +        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
    4.87 +          string_of_typing("ML:", body)
    4.88          case Text.Info(_, XML.Elem(Markup(name, _), _))
    4.89          if tooltips.isDefinedAt(name) => tooltips(name)
    4.90 -      })
    4.91 +      },
    4.92 +      Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys))
    4.93  
    4.94    val tooltip2 =
    4.95      Markup_Tree.Select[String](
    4.96        {
    4.97          case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
    4.98 -      })
    4.99 +      },
   4.100 +      Some(Set(Markup.TYPING)))
   4.101  
   4.102    private val subexp_include =
   4.103      Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   4.104 @@ -212,7 +223,8 @@
   4.105        {
   4.106          case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   4.107            (range, subexp_color)
   4.108 -      })
   4.109 +      },
   4.110 +      Some(subexp_include))
   4.111  
   4.112  
   4.113    /* token markup -- text styles */