src/Tools/jEdit/src/rendering.scala
changeset 55647 106a57dec7af
parent 55646 ec4651c697e3
child 55649 1532ab0dc67b
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 12:32:06 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 12:57:14 2014 +0100
     1.3 @@ -146,6 +146,75 @@
     1.4      else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
     1.5      else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
     1.6      else JEditToken.KEYWORD1
     1.7 +
     1.8 +
     1.9 +  /* markup elements */
    1.10 +
    1.11 +  private val completion_elements =
    1.12 +    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    1.13 +      Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
    1.14 +      Markup.ML_STRING, Markup.ML_COMMENT)
    1.15 +
    1.16 +  private val highlight_elements =
    1.17 +    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    1.18 +      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    1.19 +      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    1.20 +      Markup.VAR, Markup.TFREE, Markup.TVAR)
    1.21 +
    1.22 +  private val hyperlink_elements =
    1.23 +    Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    1.24 +
    1.25 +  private val active_elements =
    1.26 +    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    1.27 +      Markup.SENDBACK, Markup.SIMP_TRACE)
    1.28 +
    1.29 +  private val tooltip_message_elements =
    1.30 +    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    1.31 +
    1.32 +  private val tooltip_descriptions =
    1.33 +    Map(
    1.34 +      Markup.TOKEN_RANGE -> "inner syntax token",
    1.35 +      Markup.FREE -> "free variable",
    1.36 +      Markup.SKOLEM -> "skolem variable",
    1.37 +      Markup.BOUND -> "bound variable",
    1.38 +      Markup.VAR -> "schematic variable",
    1.39 +      Markup.TFREE -> "free type variable",
    1.40 +      Markup.TVAR -> "schematic type variable")
    1.41 +
    1.42 +  private val tooltip_elements =
    1.43 +    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    1.44 +      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
    1.45 +      tooltip_descriptions.keys
    1.46 +
    1.47 +  private val gutter_elements =
    1.48 +    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.49 +
    1.50 +  private val squiggly_elements =
    1.51 +    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.52 +
    1.53 +  private val line_background_elements =
    1.54 +    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
    1.55 +      Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
    1.56 +      Markup.INFORMATION)
    1.57 +
    1.58 +  private val separator_elements = Set(Markup.SEPARATOR)
    1.59 +
    1.60 +  private val background1_elements =
    1.61 +    Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
    1.62 +      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    1.63 +      Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
    1.64 +      active_elements
    1.65 +
    1.66 +  private val background2_elements = Set(Markup.TOKEN_RANGE)
    1.67 +
    1.68 +  private val foreground_elements =
    1.69 +    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    1.70 +      Markup.CARTOUCHE, Markup.ANTIQUOTED)
    1.71 +
    1.72 +  private val bullet_elements = Set(Markup.BULLET)
    1.73 +
    1.74 +  private val fold_depth_elements =
    1.75 +    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
    1.76  }
    1.77  
    1.78  
    1.79 @@ -202,14 +271,10 @@
    1.80  
    1.81    /* completion context */
    1.82  
    1.83 -  private val completion_elements =
    1.84 -    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
    1.85 -      Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT)
    1.86 -
    1.87    def completion_context(caret: Text.Offset): Option[Completion.Context] =
    1.88      if (caret > 0) {
    1.89        val result =
    1.90 -        snapshot.select_markup(Text.Range(caret - 1, caret + 1), completion_elements, _ =>
    1.91 +        snapshot.select_markup(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ =>
    1.92            {
    1.93              case Text.Info(_, elem)
    1.94              if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
    1.95 @@ -229,7 +294,7 @@
    1.96  
    1.97    /* command status overview */
    1.98  
    1.99 -  val overview_limit = options.int("jedit_text_overview_limit")
   1.100 +  def overview_limit: Int = options.int("jedit_text_overview_limit")
   1.101  
   1.102    def overview_color(range: Text.Range): Option[Color] =
   1.103    {
   1.104 @@ -264,15 +329,9 @@
   1.105  
   1.106    /* highlighted area */
   1.107  
   1.108 -  private val highlight_elements =
   1.109 -    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   1.110 -      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
   1.111 -      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
   1.112 -      Markup.VAR, Markup.TFREE, Markup.TVAR)
   1.113 -
   1.114    def highlight(range: Text.Range): Option[Text.Info[Color]] =
   1.115    {
   1.116 -    snapshot.select_markup(range, highlight_elements, _ =>
   1.117 +    snapshot.select_markup(range, Rendering.highlight_elements, _ =>
   1.118        {
   1.119          case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
   1.120        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
   1.121 @@ -281,9 +340,6 @@
   1.122  
   1.123    /* hyperlinks */
   1.124  
   1.125 -  private val hyperlink_elements =
   1.126 -    Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
   1.127 -
   1.128    private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
   1.129      if (Path.is_ok(name))
   1.130        Isabelle_System.source_file(Path.explode(name)).map(path =>
   1.131 @@ -301,7 +357,7 @@
   1.132    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   1.133    {
   1.134      snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
   1.135 -      range, Vector.empty, hyperlink_elements, _ =>
   1.136 +      range, Vector.empty, Rendering.hyperlink_elements, _ =>
   1.137          {
   1.138            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
   1.139            if Path.is_ok(name) =>
   1.140 @@ -343,11 +399,8 @@
   1.141  
   1.142    /* active elements */
   1.143  
   1.144 -  private val active_elements =
   1.145 -    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE)
   1.146 -
   1.147    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
   1.148 -    snapshot.select_markup(range, active_elements, command_state =>
   1.149 +    snapshot.select_markup(range, Rendering.active_elements, command_state =>
   1.150        {
   1.151          case Text.Info(info_range, elem) =>
   1.152            if (elem.name == Markup.DIALOG) {
   1.153 @@ -373,14 +426,11 @@
   1.154  
   1.155    /* tooltip messages */
   1.156  
   1.157 -  private val tooltip_message_elements =
   1.158 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
   1.159 -
   1.160    def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
   1.161    {
   1.162      val results =
   1.163        snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](
   1.164 -        range, Nil, tooltip_message_elements, _ =>
   1.165 +        range, Nil, Rendering.tooltip_message_elements, _ =>
   1.166          {
   1.167            case (msgs, Text.Info(info_range,
   1.168              XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   1.169 @@ -407,25 +457,10 @@
   1.170  
   1.171    /* tooltips */
   1.172  
   1.173 -  private val tooltips: Map[String, String] =
   1.174 -    Map(
   1.175 -      Markup.TOKEN_RANGE -> "inner syntax token",
   1.176 -      Markup.FREE -> "free variable",
   1.177 -      Markup.SKOLEM -> "skolem variable",
   1.178 -      Markup.BOUND -> "bound variable",
   1.179 -      Markup.VAR -> "schematic variable",
   1.180 -      Markup.TFREE -> "free type variable",
   1.181 -      Markup.TVAR -> "schematic type variable")
   1.182 -
   1.183 -  private val tooltip_elements =
   1.184 -    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
   1.185 -      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
   1.186 -      tooltips.keys
   1.187 -
   1.188    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
   1.189      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
   1.190  
   1.191 -  private val timing_threshold: Double = options.real("jedit_timing_threshold")
   1.192 +  private def timing_threshold: Double = options.real("jedit_timing_threshold")
   1.193  
   1.194    def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
   1.195    {
   1.196 @@ -441,7 +476,7 @@
   1.197  
   1.198      val results =
   1.199        snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
   1.200 -        range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
   1.201 +        range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
   1.202          {
   1.203            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   1.204              Some(Text.Info(r, (t1 + t2, info)))
   1.205 @@ -468,9 +503,8 @@
   1.206            case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
   1.207              Some(add(prev, r, (true, XML.Text("language: " + language))))
   1.208            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   1.209 -            if (tooltips.isDefinedAt(name))
   1.210 -              Some(add(prev, r, (true, XML.Text(tooltips(name)))))
   1.211 -            else None
   1.212 +            Rendering.tooltip_descriptions.get(name).
   1.213 +              map(descr => add(prev, r, (true, XML.Text(descr))))
   1.214          }).map(_.info)
   1.215  
   1.216      results.map(_.info).flatMap(res => res._2.toList) match {
   1.217 @@ -482,7 +516,7 @@
   1.218      }
   1.219    }
   1.220  
   1.221 -  val tooltip_margin: Int = options.int("jedit_tooltip_margin")
   1.222 +  def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   1.223  
   1.224    lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   1.225    lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
   1.226 @@ -496,13 +530,10 @@
   1.227      Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
   1.228      Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
   1.229  
   1.230 -  private val gutter_elements =
   1.231 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   1.232 -
   1.233    def gutter_message(range: Text.Range): Option[Icon] =
   1.234    {
   1.235      val results =
   1.236 -      snapshot.cumulate_markup[Int](range, 0, gutter_elements, _ =>
   1.237 +      snapshot.cumulate_markup[Int](range, 0, Rendering.gutter_elements, _ =>
   1.238          {
   1.239            case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
   1.240                List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
   1.241 @@ -525,19 +556,16 @@
   1.242  
   1.243    /* squiggly underline */
   1.244  
   1.245 -  private val squiggly_colors = Map(
   1.246 +  private lazy val squiggly_colors = Map(
   1.247      Rendering.writeln_pri -> writeln_color,
   1.248      Rendering.information_pri -> information_color,
   1.249      Rendering.warning_pri -> warning_color,
   1.250      Rendering.error_pri -> error_color)
   1.251  
   1.252 -  private val squiggly_elements =
   1.253 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   1.254 -
   1.255    def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   1.256    {
   1.257      val results =
   1.258 -      snapshot.cumulate_markup[Int](range, 0, squiggly_elements, _ =>
   1.259 +      snapshot.cumulate_markup[Int](range, 0, Rendering.squiggly_elements, _ =>
   1.260          {
   1.261            case (pri, Text.Info(_, elem)) =>
   1.262              if (Protocol.is_information(elem))
   1.263 @@ -554,21 +582,17 @@
   1.264  
   1.265    /* message output */
   1.266  
   1.267 -  private val message_colors = Map(
   1.268 +  private lazy val message_colors = Map(
   1.269      Rendering.writeln_pri -> writeln_message_color,
   1.270      Rendering.information_pri -> information_message_color,
   1.271      Rendering.tracing_pri -> tracing_message_color,
   1.272      Rendering.warning_pri -> warning_message_color,
   1.273      Rendering.error_pri -> error_message_color)
   1.274  
   1.275 -  private val line_background_elements =
   1.276 -    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE,
   1.277 -      Markup.ERROR_MESSAGE, Markup.INFORMATION)
   1.278 -
   1.279    def line_background(range: Text.Range): Option[(Color, Boolean)] =
   1.280    {
   1.281      val results =
   1.282 -      snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
   1.283 +      snapshot.cumulate_markup[Int](range, 0, Rendering.line_background_elements, _ =>
   1.284          {
   1.285            case (pri, Text.Info(_, elem)) =>
   1.286              if (elem.name == Markup.INFORMATION)
   1.287 @@ -580,7 +604,7 @@
   1.288  
   1.289      val is_separator =
   1.290        pri > 0 &&
   1.291 -      snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
   1.292 +      snapshot.cumulate_markup[Boolean](range, false, Rendering.separator_elements, _ =>
   1.293          {
   1.294            case _ => Some(true)
   1.295          }).exists(_.info)
   1.296 @@ -594,11 +618,6 @@
   1.297  
   1.298    /* text background */
   1.299  
   1.300 -  private val background1_elements =
   1.301 -    Protocol.command_status_elements + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
   1.302 -      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
   1.303 -      active_elements
   1.304 -
   1.305    def background1(range: Text.Range): List[Text.Info[Color]] =
   1.306    {
   1.307      if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
   1.308 @@ -606,26 +625,27 @@
   1.309        for {
   1.310          Text.Info(r, result) <-
   1.311            snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   1.312 -            range, (Some(Protocol.Status.init), None), background1_elements, command_state =>
   1.313 -            {
   1.314 -              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   1.315 -              if (Protocol.command_status_elements(markup.name)) =>
   1.316 -                Some((Some(Protocol.command_status(status, markup)), color))
   1.317 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   1.318 -                Some((None, Some(bad_color)))
   1.319 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   1.320 -                Some((None, Some(intensify_color)))
   1.321 -              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   1.322 -                command_state.results.get(serial) match {
   1.323 -                  case Some(Protocol.Dialog_Result(res)) if res == result =>
   1.324 -                    Some((None, Some(active_result_color)))
   1.325 -                  case _ =>
   1.326 -                    Some((None, Some(active_color)))
   1.327 -                }
   1.328 -              case (_, Text.Info(_, elem)) =>
   1.329 -                if (active_elements(elem.name)) Some((None, Some(active_color)))
   1.330 -                else None
   1.331 -            })
   1.332 +            range, (Some(Protocol.Status.init), None), Rendering.background1_elements,
   1.333 +            command_state =>
   1.334 +              {
   1.335 +                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   1.336 +                if (Protocol.command_status_elements(markup.name)) =>
   1.337 +                  Some((Some(Protocol.command_status(status, markup)), color))
   1.338 +                case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   1.339 +                  Some((None, Some(bad_color)))
   1.340 +                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   1.341 +                  Some((None, Some(intensify_color)))
   1.342 +                case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   1.343 +                  command_state.results.get(serial) match {
   1.344 +                    case Some(Protocol.Dialog_Result(res)) if res == result =>
   1.345 +                      Some((None, Some(active_result_color)))
   1.346 +                    case _ =>
   1.347 +                      Some((None, Some(active_color)))
   1.348 +                  }
   1.349 +                case (_, Text.Info(_, elem)) =>
   1.350 +                  if (Rendering.active_elements(elem.name)) Some((None, Some(active_color)))
   1.351 +                  else None
   1.352 +              })
   1.353          color <-
   1.354            (result match {
   1.355              case (Some(status), opt_color) =>
   1.356 @@ -638,16 +658,13 @@
   1.357    }
   1.358  
   1.359    def background2(range: Text.Range): List[Text.Info[Color]] =
   1.360 -    snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ => _ => Some(light_color))
   1.361 +    snapshot.select_markup(range, Rendering.background2_elements, _ => _ => Some(light_color))
   1.362  
   1.363  
   1.364    /* text foreground */
   1.365  
   1.366 -  private val foreground_elements =
   1.367 -    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
   1.368 -
   1.369    def foreground(range: Text.Range): List[Text.Info[Color]] =
   1.370 -    snapshot.select_markup(range, foreground_elements, _ =>
   1.371 +    snapshot.select_markup(range, Rendering.foreground_elements, _ =>
   1.372        {
   1.373          case Text.Info(_, elem) =>
   1.374            if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
   1.375 @@ -656,7 +673,7 @@
   1.376  
   1.377    /* text color */
   1.378  
   1.379 -  private val text_colors: Map[String, Color] = Map(
   1.380 +  private lazy val text_colors: Map[String, Color] = Map(
   1.381        Markup.KEYWORD1 -> keyword1_color,
   1.382        Markup.KEYWORD2 -> keyword2_color,
   1.383        Markup.STRING -> Color.BLACK,
   1.384 @@ -685,7 +702,7 @@
   1.385        Markup.ML_STRING -> inner_quoted_color,
   1.386        Markup.ML_COMMENT -> inner_comment_color)
   1.387  
   1.388 -  private val text_color_elements = text_colors.keySet
   1.389 +  private lazy val text_color_elements = text_colors.keySet
   1.390  
   1.391    def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   1.392    {
   1.393 @@ -701,16 +718,13 @@
   1.394    /* virtual bullets */
   1.395  
   1.396    def bullet(range: Text.Range): List[Text.Info[Color]] =
   1.397 -    snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color))
   1.398 +    snapshot.select_markup(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
   1.399  
   1.400  
   1.401    /* text folds */
   1.402  
   1.403 -  private val fold_depth_elements =
   1.404 -    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   1.405 -
   1.406    def fold_depth(range: Text.Range): List[Text.Info[Int]] =
   1.407 -    snapshot.cumulate_markup[Int](range, 0, fold_depth_elements, _ =>
   1.408 +    snapshot.cumulate_markup[Int](range, 0, Rendering.fold_depth_elements, _ =>
   1.409        {
   1.410          case (depth, _) => Some(depth + 1)
   1.411        })