tuned signature;
authorwenzelm
Sat Nov 12 12:21:42 2011 +0100 (2011-11-12)
changeset 4546833e946d3f449
parent 45467 3f290b6288cf
child 45469 25306d92f4ad
tuned signature;
express select in terms of cumulate;
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 11:45:49 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Nov 12 12:21:42 2011 +0100
     1.3 @@ -241,7 +241,7 @@
     1.4      def revert(i: Text.Offset): Text.Offset
     1.5      def revert(range: Text.Range): Text.Range
     1.6      def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
     1.7 -    def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
     1.8 +    def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
     1.9        : Stream[Text.Info[Option[A]]]
    1.10    }
    1.11  
    1.12 @@ -492,19 +492,16 @@
    1.13            } yield Text.Info(convert(r0 + command_start), a)
    1.14          }
    1.15  
    1.16 -        def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    1.17 +        def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
    1.18            : Stream[Text.Info[Option[A]]] =
    1.19          {
    1.20 -          val former_range = revert(range)
    1.21 -          for {
    1.22 -            (command, command_start) <- node.command_range(former_range).toStream
    1.23 -            Text.Info(r0, x) <- command_state(command).markup.
    1.24 -              select((former_range - command_start).restrict(command.range)) {
    1.25 -                case Text.Info(r0, info)
    1.26 -                if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
    1.27 -                  result(Text.Info(convert(r0 + command_start), info))
    1.28 -              }
    1.29 -          } yield Text.Info(convert(r0 + command_start), x)
    1.30 +          val result = body.result
    1.31 +          val result1 =
    1.32 +            new PartialFunction[(Option[A], Text.Markup), Option[A]] {
    1.33 +              def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
    1.34 +              def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
    1.35 +            }
    1.36 +          cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1))
    1.37          }
    1.38        }
    1.39      }
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 11:45:49 2011 +0100
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 12:21:42 2011 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4  object Markup_Tree
     2.5  {
     2.6    sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A])
     2.7 -  type Select[A] = PartialFunction[Text.Markup, A]
     2.8 +  sealed case class Select[A](result: PartialFunction[Text.Markup, A])
     2.9  
    2.10    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    2.11  
    2.12 @@ -124,43 +124,6 @@
    2.13        List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
    2.14    }
    2.15  
    2.16 -  def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
    2.17 -  {
    2.18 -    def stream(
    2.19 -      last: Text.Offset,
    2.20 -      stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
    2.21 -        : Stream[Text.Info[Option[A]]] =
    2.22 -    {
    2.23 -      stack match {
    2.24 -        case (parent, (range, (info, tree)) #:: more) :: rest =>
    2.25 -          val subrange = range.restrict(root_range)
    2.26 -          val subtree = tree.overlapping(subrange).toStream
    2.27 -          val start = subrange.start
    2.28 -
    2.29 -          if (result.isDefinedAt(info)) {
    2.30 -            val next = Text.Info[Option[A]](subrange, Some(result(info)))
    2.31 -            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
    2.32 -            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
    2.33 -            else nexts
    2.34 -          }
    2.35 -          else stream(last, (parent, subtree #::: more) :: rest)
    2.36 -
    2.37 -        case (parent, Stream.Empty) :: rest =>
    2.38 -          val stop = parent.range.stop
    2.39 -          val nexts = stream(stop, rest)
    2.40 -          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
    2.41 -          else nexts
    2.42 -
    2.43 -        case Nil =>
    2.44 -          val stop = root_range.stop
    2.45 -          if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
    2.46 -          else Stream.empty
    2.47 -      }
    2.48 -    }
    2.49 -    stream(root_range.start,
    2.50 -      List((Text.Info(root_range, None), overlapping(root_range).toStream)))
    2.51 -  }
    2.52 -
    2.53    def swing_tree(parent: DefaultMutableTreeNode)
    2.54      (swing_node: Text.Markup => DefaultMutableTreeNode)
    2.55    {
     3.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 11:45:49 2011 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 12:21:42 2011 +0100
     3.3 @@ -57,37 +57,39 @@
     3.4          case Some(model) =>
     3.5            val snapshot = model.snapshot()
     3.6            val markup =
     3.7 -            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
     3.8 -              // FIXME Isar_Document.Hyperlink extractor
     3.9 -              case Text.Info(info_range,
    3.10 -                  XML.Elem(Markup(Markup.ENTITY, props), _))
    3.11 -                if (props.find(
    3.12 -                  { case (Markup.KIND, Markup.ML_OPEN) => true
    3.13 -                    case (Markup.KIND, Markup.ML_STRUCT) => true
    3.14 -                    case _ => false }).isEmpty) =>
    3.15 -                val Text.Range(begin, end) = info_range
    3.16 -                val line = buffer.getLineOfOffset(begin)
    3.17 -                (Position.File.unapply(props), Position.Line.unapply(props)) match {
    3.18 -                  case (Some(def_file), Some(def_line)) =>
    3.19 -                    new External_Hyperlink(begin, end, line, def_file, def_line)
    3.20 -                  case _ if !snapshot.is_outdated =>
    3.21 -                    (props, props) match {
    3.22 -                      case (Position.Id(def_id), Position.Offset(def_offset)) =>
    3.23 -                        snapshot.state.find_command(snapshot.version, def_id) match {
    3.24 -                          case Some((def_node, def_cmd)) =>
    3.25 -                            def_node.command_start(def_cmd) match {
    3.26 -                              case Some(def_cmd_start) =>
    3.27 -                                new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
    3.28 -                                  def_cmd_start + def_cmd.decode(def_offset))
    3.29 +            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
    3.30 +              Markup_Tree.Select[Hyperlink](
    3.31 +                {
    3.32 +                  // FIXME Isar_Document.Hyperlink extractor
    3.33 +                  case Text.Info(info_range,
    3.34 +                      XML.Elem(Markup(Markup.ENTITY, props), _))
    3.35 +                    if (props.find(
    3.36 +                      { case (Markup.KIND, Markup.ML_OPEN) => true
    3.37 +                        case (Markup.KIND, Markup.ML_STRUCT) => true
    3.38 +                        case _ => false }).isEmpty) =>
    3.39 +                    val Text.Range(begin, end) = info_range
    3.40 +                    val line = buffer.getLineOfOffset(begin)
    3.41 +                    (Position.File.unapply(props), Position.Line.unapply(props)) match {
    3.42 +                      case (Some(def_file), Some(def_line)) =>
    3.43 +                        new External_Hyperlink(begin, end, line, def_file, def_line)
    3.44 +                      case _ if !snapshot.is_outdated =>
    3.45 +                        (props, props) match {
    3.46 +                          case (Position.Id(def_id), Position.Offset(def_offset)) =>
    3.47 +                            snapshot.state.find_command(snapshot.version, def_id) match {
    3.48 +                              case Some((def_node, def_cmd)) =>
    3.49 +                                def_node.command_start(def_cmd) match {
    3.50 +                                  case Some(def_cmd_start) =>
    3.51 +                                    new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
    3.52 +                                      def_cmd_start + def_cmd.decode(def_offset))
    3.53 +                                  case None => null
    3.54 +                                }
    3.55                                case None => null
    3.56                              }
    3.57 -                          case None => null
    3.58 +                          case _ => null
    3.59                          }
    3.60                        case _ => null
    3.61                      }
    3.62 -                  case _ => null
    3.63 -                }
    3.64 -            }
    3.65 +                }))
    3.66            markup match {
    3.67              case Text.Info(_, Some(link)) #:: _ => link
    3.68              case _ => null
     4.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 11:45:49 2011 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 12:21:42 2011 +0100
     4.3 @@ -87,12 +87,13 @@
     4.4  
     4.5    /* markup selectors */
     4.6  
     4.7 -  val message: Markup_Tree.Select[Color] =
     4.8 -  {
     4.9 -    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    4.10 -    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    4.11 -    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    4.12 -  }
    4.13 +  val message =
    4.14 +    Markup_Tree.Select[Color](
    4.15 +    {
    4.16 +      case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    4.17 +      case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    4.18 +      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    4.19 +    })
    4.20  
    4.21    val tooltip_message =
    4.22      Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
    4.23 @@ -103,33 +104,37 @@
    4.24              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
    4.25        })
    4.26  
    4.27 -  val gutter_message: Markup_Tree.Select[Icon] =
    4.28 -  {
    4.29 -    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
    4.30 -      body match {
    4.31 -        case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
    4.32 -        case _ => warning_icon
    4.33 -      }
    4.34 -    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
    4.35 -  }
    4.36 +  val gutter_message =
    4.37 +    Markup_Tree.Select[Icon](
    4.38 +      {
    4.39 +        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
    4.40 +          body match {
    4.41 +            case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
    4.42 +            case _ => warning_icon
    4.43 +          }
    4.44 +        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
    4.45 +      })
    4.46  
    4.47 -  val background1: Markup_Tree.Select[Color] =
    4.48 -  {
    4.49 -    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
    4.50 -    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
    4.51 -  }
    4.52 +  val background1 =
    4.53 +    Markup_Tree.Select[Color](
    4.54 +      {
    4.55 +        case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
    4.56 +        case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
    4.57 +      })
    4.58  
    4.59 -  val background2: Markup_Tree.Select[Color] =
    4.60 -  {
    4.61 -    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
    4.62 -  }
    4.63 +  val background2 =
    4.64 +    Markup_Tree.Select[Color](
    4.65 +      {
    4.66 +        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
    4.67 +      })
    4.68  
    4.69 -  val foreground: Markup_Tree.Select[Color] =
    4.70 -  {
    4.71 -    case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
    4.72 -    case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
    4.73 -    case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
    4.74 -  }
    4.75 +  val foreground =
    4.76 +    Markup_Tree.Select[Color](
    4.77 +      {
    4.78 +        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
    4.79 +        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
    4.80 +        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
    4.81 +      })
    4.82  
    4.83    private val text_colors: Map[String, Color] =
    4.84      Map(
    4.85 @@ -156,10 +161,11 @@
    4.86        Markup.ML_MALFORMED -> get_color("#FF6A6A"),
    4.87        Markup.ANTIQ -> get_color("blue"))
    4.88  
    4.89 -  val text_color: Markup_Tree.Select[Color] =
    4.90 -  {
    4.91 -    case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
    4.92 -  }
    4.93 +  val text_color =
    4.94 +    Markup_Tree.Select[Color](
    4.95 +      {
    4.96 +        case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
    4.97 +      })
    4.98  
    4.99    private val tooltips: Map[String, String] =
   4.100      Map(
   4.101 @@ -181,29 +187,32 @@
   4.102      Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
   4.103        margin = Isabelle.Int_Property("tooltip-margin"))
   4.104  
   4.105 -  val tooltip1: Markup_Tree.Select[String] =
   4.106 -  {
   4.107 -    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
   4.108 -    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
   4.109 -    case Text.Info(_, XML.Elem(Markup(name, _), _))
   4.110 -    if tooltips.isDefinedAt(name) => tooltips(name)
   4.111 -  }
   4.112 +  val tooltip1 =
   4.113 +    Markup_Tree.Select[String](
   4.114 +      {
   4.115 +        case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
   4.116 +        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
   4.117 +        case Text.Info(_, XML.Elem(Markup(name, _), _))
   4.118 +        if tooltips.isDefinedAt(name) => tooltips(name)
   4.119 +      })
   4.120  
   4.121 -  val tooltip2: Markup_Tree.Select[String] =
   4.122 -  {
   4.123 -    case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
   4.124 -  }
   4.125 +  val tooltip2 =
   4.126 +    Markup_Tree.Select[String](
   4.127 +      {
   4.128 +        case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
   4.129 +      })
   4.130  
   4.131    private val subexp_include =
   4.132      Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   4.133        Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
   4.134        Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
   4.135  
   4.136 -  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
   4.137 -  {
   4.138 -    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   4.139 -      (range, subexp_color)
   4.140 -  }
   4.141 +  val subexp =
   4.142 +    Markup_Tree.Select[(Text.Range, Color)](
   4.143 +      {
   4.144 +        case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   4.145 +          (range, subexp_color)
   4.146 +      })
   4.147  
   4.148  
   4.149    /* token markup -- text styles */