src/Tools/jEdit/src/rendering.scala
changeset 52889 ea3338812e67
parent 52873 9e934d4fff00
child 52890 36e2c0c308eb
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 11:50:14 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 13:46:32 2013 +0200
     1.3 @@ -154,11 +154,12 @@
     1.4          snapshot.cumulate_markup[(Protocol.Status, Int)](
     1.5            range, (Protocol.Status.init, 0), Some(overview_include), _ =>
     1.6            {
     1.7 -            case ((status, pri), Text.Info(_, XML.Elem(markup, _)))
     1.8 -            if overview_include(markup.name) =>
     1.9 +            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
    1.10                if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
    1.11 -                (status, pri max Rendering.message_pri(markup.name))
    1.12 -              else (Protocol.command_status(status, markup), pri)
    1.13 +                Some((status, pri max Rendering.message_pri(markup.name)))
    1.14 +              else if (overview_include(markup.name))
    1.15 +                Some((Protocol.command_status(status, markup), pri))
    1.16 +              else None
    1.17            })
    1.18        if (results.isEmpty) None
    1.19        else {
    1.20 @@ -188,8 +189,10 @@
    1.21    {
    1.22      snapshot.select_markup(range, Some(highlight_include), _ =>
    1.23          {
    1.24 -          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
    1.25 -            Text.Info(snapshot.convert(info_range), highlight_color)
    1.26 +          case Text.Info(info_range, XML.Elem(markup, _)) =>
    1.27 +            if (highlight_include(markup.name))
    1.28 +              Some(Text.Info(snapshot.convert(info_range), highlight_color))
    1.29 +            else None
    1.30          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    1.31    }
    1.32  
    1.33 @@ -203,7 +206,8 @@
    1.34            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    1.35            if Path.is_ok(name) =>
    1.36              val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    1.37 -            Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
    1.38 +            val link = Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0))
    1.39 +            Some(link :: links)
    1.40  
    1.41            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    1.42            if !props.exists(
    1.43 @@ -216,8 +220,10 @@
    1.44                  Isabelle_System.source_file(Path.explode(name)) match {
    1.45                    case Some(path) =>
    1.46                      val jedit_file = Isabelle_System.platform_path(path)
    1.47 -                    Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
    1.48 -                  case None => links
    1.49 +                    val link =
    1.50 +                      Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0))
    1.51 +                    Some(link :: links)
    1.52 +                  case None => None
    1.53                  }
    1.54  
    1.55                case Position.Def_Id_Offset(id, offset) =>
    1.56 @@ -227,13 +233,17 @@
    1.57                        node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    1.58                          Iterator.single(command.source(Text.Range(0, command.decode(offset))))
    1.59                      val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    1.60 -                    Text.Info(snapshot.convert(info_range),
    1.61 -                      Hyperlink(command.node_name.node, line, column)) :: links
    1.62 -                  case None => links
    1.63 +                    val link =
    1.64 +                      Text.Info(snapshot.convert(info_range),
    1.65 +                        Hyperlink(command.node_name.node, line, column))
    1.66 +                    Some(link :: links)
    1.67 +                  case None => None
    1.68                  }
    1.69  
    1.70 -              case _ => links
    1.71 +              case _ => None
    1.72              }
    1.73 +
    1.74 +          case _ => None
    1.75          }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
    1.76    }
    1.77  
    1.78 @@ -246,10 +256,11 @@
    1.79          {
    1.80            case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    1.81            if !command_state.results.defined(serial) =>
    1.82 -            Text.Info(snapshot.convert(info_range), elem)
    1.83 -          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
    1.84 -          if name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
    1.85 -            Text.Info(snapshot.convert(info_range), elem)
    1.86 +            Some(Text.Info(snapshot.convert(info_range), elem))
    1.87 +          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _)) =>
    1.88 +            if (name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK)
    1.89 +              Some(Text.Info(snapshot.convert(info_range), elem))
    1.90 +            else None
    1.91          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    1.92  
    1.93  
    1.94 @@ -257,7 +268,7 @@
    1.95    {
    1.96      val results =
    1.97        snapshot.select_markup[Command.Results](range, None, command_state =>
    1.98 -        { case _ => command_state.results }).map(_.info)
    1.99 +        { case _ => Some(command_state.results) }).map(_.info)
   1.100      (Command.Results.empty /: results)(_ ++ _)
   1.101    }
   1.102  
   1.103 @@ -272,12 +283,14 @@
   1.104            if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
   1.105              val entry: Command.Results.Entry =
   1.106                (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   1.107 -            Text.Info(snapshot.convert(info_range), entry) :: msgs
   1.108 +            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   1.109  
   1.110            case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
   1.111            if !body.isEmpty =>
   1.112              val entry: Command.Results.Entry = (Document_ID.make(), msg)
   1.113 -            Text.Info(snapshot.convert(info_range), entry) :: msgs
   1.114 +            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   1.115 +
   1.116 +          case _ => None
   1.117          }).toList.flatMap(_.info)
   1.118      if (results.isEmpty) None
   1.119      else {
   1.120 @@ -328,7 +341,7 @@
   1.121          range, Text.Info(range, (Timing.zero, Nil)), Some(tooltip_elements), _ =>
   1.122          {
   1.123            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   1.124 -            Text.Info(r, (t1 + t2, info))
   1.125 +            Some(Text.Info(r, (t1 + t2, info)))
   1.126            case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   1.127              val kind1 = space_explode('_', kind).mkString(" ")
   1.128              val txt1 = kind1 + " " + quote(name)
   1.129 @@ -337,19 +350,20 @@
   1.130                if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   1.131                  "\n" + t.message
   1.132                else ""
   1.133 -            add(prev, r, (true, XML.Text(txt1 + txt2)))
   1.134 +            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   1.135            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
   1.136            if Path.is_ok(name) =>
   1.137              val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   1.138 -            add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
   1.139 +            Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
   1.140            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   1.141            if name == Markup.SORTING || name == Markup.TYPING =>
   1.142 -            add(prev, r, (true, pretty_typing("::", body)))
   1.143 +            Some(add(prev, r, (true, pretty_typing("::", body))))
   1.144            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   1.145 -            add(prev, r, (false, pretty_typing("ML:", body)))
   1.146 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
   1.147 -          if tooltips.isDefinedAt(name) =>
   1.148 -            add(prev, r, (true, XML.Text(tooltips(name))))
   1.149 +            Some(add(prev, r, (false, pretty_typing("ML:", body))))
   1.150 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   1.151 +            if (tooltips.isDefinedAt(name))
   1.152 +              Some(add(prev, r, (true, XML.Text(tooltips(name)))))
   1.153 +            else None
   1.154          }).toList.map(_.info)
   1.155  
   1.156      results.map(_.info).flatMap(_._2) match {
   1.157 @@ -383,15 +397,17 @@
   1.158          {
   1.159            case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
   1.160                List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
   1.161 -            pri max Rendering.information_pri
   1.162 +            Some(pri max Rendering.information_pri)
   1.163            case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
   1.164              body match {
   1.165                case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
   1.166 -                pri max Rendering.legacy_pri
   1.167 -              case _ => pri max Rendering.warning_pri
   1.168 +                Some(pri max Rendering.legacy_pri)
   1.169 +              case _ =>
   1.170 +                Some(pri max Rendering.warning_pri)
   1.171              }
   1.172            case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
   1.173 -            pri max Rendering.error_pri
   1.174 +            Some(pri max Rendering.error_pri)
   1.175 +          case _ => None
   1.176          })
   1.177      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   1.178      gutter_icons.get(pri)
   1.179 @@ -404,19 +420,19 @@
   1.180      Rendering.warning_pri -> warning_color,
   1.181      Rendering.error_pri -> error_color)
   1.182  
   1.183 -  private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   1.184 +  private val squiggly_include = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   1.185  
   1.186    def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   1.187    {
   1.188      val results =
   1.189 -      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
   1.190 +      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
   1.191          {
   1.192 -          case (pri, Text.Info(_, msg @ XML.Elem(Markup(name, _), _)))
   1.193 -          if name == Markup.WRITELN ||
   1.194 -            name == Markup.WARNING ||
   1.195 -            name == Markup.ERROR =>
   1.196 -              if (Protocol.is_information(msg)) pri max Rendering.information_pri
   1.197 -              else pri max Rendering.message_pri(name)
   1.198 +          case (pri, Text.Info(_, msg @ XML.Elem(markup, _))) =>
   1.199 +            if (Protocol.is_information(msg))
   1.200 +              Some(pri max Rendering.information_pri)
   1.201 +            else if (squiggly_include.contains(markup.name))
   1.202 +              Some(pri max Rendering.message_pri(markup.name))
   1.203 +            else None
   1.204          })
   1.205      for {
   1.206        Text.Info(r, pri) <- results
   1.207 @@ -442,19 +458,20 @@
   1.208        snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
   1.209          {
   1.210            case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
   1.211 -            pri max Rendering.information_pri
   1.212 -          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
   1.213 -          if name == Markup.WRITELN_MESSAGE ||
   1.214 -            name == Markup.TRACING_MESSAGE ||
   1.215 -            name == Markup.WARNING_MESSAGE ||
   1.216 -            name == Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
   1.217 +            Some(pri max Rendering.information_pri)
   1.218 +          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
   1.219 +            if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
   1.220 +                name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
   1.221 +              Some(pri max Rendering.message_pri(name))
   1.222 +            else None
   1.223          })
   1.224      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   1.225  
   1.226      val is_separator = pri > 0 &&
   1.227        snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
   1.228          {
   1.229 -          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
   1.230 +          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => Some(true)
   1.231 +          case _ => None
   1.232          }).exists(_.info)
   1.233  
   1.234      message_colors.get(pri).map((_, is_separator))
   1.235 @@ -483,20 +500,21 @@
   1.236              {
   1.237                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   1.238                if (Protocol.command_status_markup(markup.name)) =>
   1.239 -                (Some(Protocol.command_status(status, markup)), color)
   1.240 +                Some((Some(Protocol.command_status(status, markup)), color))
   1.241                case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   1.242 -                (None, Some(bad_color))
   1.243 +                Some((None, Some(bad_color)))
   1.244                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   1.245 -                (None, Some(intensify_color))
   1.246 +                Some((None, Some(intensify_color)))
   1.247                case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   1.248                  command_state.results.get(serial) match {
   1.249                    case Some(Protocol.Dialog_Result(res)) if res == result =>
   1.250 -                    (None, Some(active_result_color))
   1.251 +                    Some((None, Some(active_result_color)))
   1.252                    case _ =>
   1.253 -                    (None, Some(active_color))
   1.254 +                    Some((None, Some(active_color)))
   1.255                  }
   1.256 -              case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
   1.257 -                (None, Some(active_color))
   1.258 +              case (_, Text.Info(_, XML.Elem(markup, _))) =>
   1.259 +                if (active_include(markup.name)) Some((None, Some(active_color)))
   1.260 +                else None
   1.261              })
   1.262          color <-
   1.263            (result match {
   1.264 @@ -513,14 +531,16 @@
   1.265    def background2(range: Text.Range): Stream[Text.Info[Color]] =
   1.266      snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
   1.267        {
   1.268 -        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   1.269 +        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => Some(light_color)
   1.270 +        case _ => None
   1.271        })
   1.272  
   1.273  
   1.274    def bullet(range: Text.Range): Stream[Text.Info[Color]] =
   1.275      snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
   1.276        {
   1.277 -        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => bullet_color
   1.278 +        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => Some(bullet_color)
   1.279 +        case _ => None
   1.280        })
   1.281  
   1.282  
   1.283 @@ -530,10 +550,11 @@
   1.284    def foreground(range: Text.Range): Stream[Text.Info[Color]] =
   1.285      snapshot.select_markup(range, Some(foreground_elements), _ =>
   1.286        {
   1.287 -        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
   1.288 -        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
   1.289 -        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
   1.290 -        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => antiquoted_color
   1.291 +        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => Some(quoted_color)
   1.292 +        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => Some(quoted_color)
   1.293 +        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => Some(quoted_color)
   1.294 +        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => Some(antiquoted_color)
   1.295 +        case _ => None
   1.296        })
   1.297  
   1.298  
   1.299 @@ -570,8 +591,7 @@
   1.300      else
   1.301        snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
   1.302          {
   1.303 -          case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
   1.304 -          if text_colors.isDefinedAt(m) => text_colors(m)
   1.305 +          case (_, Text.Info(_, XML.Elem(markup, _))) => text_colors.get(markup.name)
   1.306          })
   1.307    }
   1.308  
   1.309 @@ -583,7 +603,7 @@
   1.310    def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
   1.311      snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
   1.312        {
   1.313 -        case (depth, Text.Info(_, XML.Elem(Markup(name, _), _)))
   1.314 -        if fold_depth_include(name) => depth + 1
   1.315 +        case (depth, Text.Info(_, XML.Elem(markup, _))) =>
   1.316 +          if (fold_depth_include(markup.name)) Some(depth + 1) else None
   1.317        })
   1.318  }