src/Pure/PIDE/rendering.scala
author wenzelm
Tue Mar 07 17:56:57 2017 +0100 (2017-03-07)
changeset 65144 b5782e996651
parent 65143 36cd85caf09a
child 65145 576d52aa0a78
permissions -rw-r--r--
more generic colors;
     1 /*  Title:      Pure/PIDE/rendering.scala
     2     Author:     Makarius
     3 
     4 Isabelle-specific implementation of quasi-abstract rendering and
     5 markup interpretation.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 object Rendering
    12 {
    13   /* color */
    14 
    15   object Color extends Enumeration
    16   {
    17     // background
    18     val unprocessed1 = Value("unprocessed1")
    19     val running1 = Value("running1")
    20     val bad = Value("bad")
    21     val intensify = Value("intensify")
    22     val entity = Value("entity")
    23     val active = Value("active")
    24     val active_result = Value("active_result")
    25     val markdown_item1 = Value("markdown_item1")
    26     val markdown_item2 = Value("markdown_item2")
    27     val markdown_item3 = Value("markdown_item3")
    28     val markdown_item4 = Value("markdown_item4")
    29     val background_colors = values
    30 
    31     // foreground
    32     val quoted = Value("quoted")
    33     val antiquoted = Value("antiquoted")
    34     val foreground_colors = values -- background_colors
    35 
    36     // message underline
    37     val writeln = Value("writeln")
    38     val information = Value("information")
    39     val warning = Value("warning")
    40     val legacy = Value("legacy")
    41     val error = Value("error")
    42     val message_underline_colors = values -- background_colors -- foreground_colors
    43 
    44     // message background
    45     val writeln_message = Value("writeln_message")
    46     val information_message = Value("information_message")
    47     val tracing_message = Value("tracing_message")
    48     val warning_message = Value("warning_message")
    49     val legacy_message = Value("legacy_message")
    50     val error_message = Value("error_message")
    51     val message_background_colors =
    52       values -- background_colors -- foreground_colors -- message_underline_colors
    53 
    54     // text
    55     val text = Value("text")
    56     val keyword1 = Value("keyword1")
    57     val keyword2 = Value("keyword2")
    58     val keyword3 = Value("keyword3")
    59     val quasi_keyword = Value("quasi_keyword")
    60     val improper = Value("improper")
    61     val operator = Value("operator")
    62     val tfree = Value("tfree")
    63     val tvar = Value("tvar")
    64     val free = Value("free")
    65     val skolem = Value("skolem")
    66     val bound = Value("bound")
    67     val var_ = Value("var")
    68     val inner_numeral = Value("inner_numeral")
    69     val inner_quoted = Value("inner_quoted")
    70     val inner_cartouche = Value("inner_cartouche")
    71     val inner_comment = Value("inner_comment")
    72     val dynamic = Value("dynamic")
    73     val class_parameter = Value("class_parameter")
    74     val antiquote = Value("antiquote")
    75     val text_colors =
    76       values -- background_colors -- foreground_colors -- message_underline_colors --
    77       message_background_colors
    78   }
    79 
    80 
    81   /* message priorities */
    82 
    83   val state_pri = 1
    84   val writeln_pri = 2
    85   val information_pri = 3
    86   val tracing_pri = 4
    87   val warning_pri = 5
    88   val legacy_pri = 6
    89   val error_pri = 7
    90 
    91   val message_pri = Map(
    92     Markup.STATE -> state_pri,
    93     Markup.STATE_MESSAGE -> state_pri,
    94     Markup.WRITELN -> writeln_pri,
    95     Markup.WRITELN_MESSAGE -> writeln_pri,
    96     Markup.INFORMATION -> information_pri,
    97     Markup.INFORMATION_MESSAGE -> information_pri,
    98     Markup.TRACING -> tracing_pri,
    99     Markup.TRACING_MESSAGE -> tracing_pri,
   100     Markup.WARNING -> warning_pri,
   101     Markup.WARNING_MESSAGE -> warning_pri,
   102     Markup.LEGACY -> legacy_pri,
   103     Markup.LEGACY_MESSAGE -> legacy_pri,
   104     Markup.ERROR -> error_pri,
   105     Markup.ERROR_MESSAGE -> error_pri
   106   ).withDefaultValue(0)
   107 
   108   val message_underline_color = Map(
   109     writeln_pri -> Color.writeln,
   110     information_pri -> Color.information,
   111     warning_pri -> Color.warning,
   112     legacy_pri -> Color.legacy,
   113     error_pri -> Color.error)
   114 
   115   val message_background_color = Map(
   116     writeln_pri -> Color.writeln_message,
   117     information_pri -> Color.information_message,
   118     tracing_pri -> Color.tracing_message,
   119     warning_pri -> Color.warning_message,
   120     legacy_pri -> Color.legacy_message,
   121     error_pri -> Color.error_message)
   122 
   123 
   124   /* text color */
   125 
   126   val text_color = Map(
   127     Markup.KEYWORD1 -> Color.keyword1,
   128     Markup.KEYWORD2 -> Color.keyword2,
   129     Markup.KEYWORD3 -> Color.keyword3,
   130     Markup.QUASI_KEYWORD -> Color.quasi_keyword,
   131     Markup.IMPROPER -> Color.improper,
   132     Markup.OPERATOR -> Color.operator,
   133     Markup.STRING -> Color.text,
   134     Markup.ALT_STRING -> Color.text,
   135     Markup.VERBATIM -> Color.text,
   136     Markup.CARTOUCHE -> Color.text,
   137     Markup.LITERAL -> Color.keyword1,
   138     Markup.DELIMITER -> Color.text,
   139     Markup.TFREE -> Color.tfree,
   140     Markup.TVAR -> Color.tvar,
   141     Markup.FREE -> Color.free,
   142     Markup.SKOLEM -> Color.skolem,
   143     Markup.BOUND -> Color.bound,
   144     Markup.VAR -> Color.var_,
   145     Markup.INNER_STRING -> Color.inner_quoted,
   146     Markup.INNER_CARTOUCHE -> Color.inner_cartouche,
   147     Markup.INNER_COMMENT -> Color.inner_comment,
   148     Markup.DYNAMIC_FACT -> Color.dynamic,
   149     Markup.CLASS_PARAMETER -> Color.class_parameter,
   150     Markup.ANTIQUOTE -> Color.antiquote,
   151     Markup.ML_KEYWORD1 -> Color.keyword1,
   152     Markup.ML_KEYWORD2 -> Color.keyword2,
   153     Markup.ML_KEYWORD3 -> Color.keyword3,
   154     Markup.ML_DELIMITER -> Color.text,
   155     Markup.ML_NUMERAL -> Color.inner_numeral,
   156     Markup.ML_CHAR -> Color.inner_quoted,
   157     Markup.ML_STRING -> Color.inner_quoted,
   158     Markup.ML_COMMENT -> Color.inner_comment,
   159     Markup.SML_STRING -> Color.inner_quoted,
   160     Markup.SML_COMMENT -> Color.inner_comment)
   161 
   162 
   163   /* markup elements */
   164 
   165   val active_elements =
   166     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
   167       Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
   168 
   169   private val background_elements =
   170     Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
   171       Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
   172       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
   173       Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
   174       Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
   175       Markup.Markdown_Item.name ++ active_elements
   176 
   177   private val foreground_elements =
   178     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
   179       Markup.CARTOUCHE, Markup.ANTIQUOTED)
   180 
   181   private val semantic_completion_elements =
   182     Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
   183 
   184   private val tooltip_descriptions =
   185     Map(
   186       Markup.CITATION -> "citation",
   187       Markup.TOKEN_RANGE -> "inner syntax token",
   188       Markup.FREE -> "free variable",
   189       Markup.SKOLEM -> "skolem variable",
   190       Markup.BOUND -> "bound variable",
   191       Markup.VAR -> "schematic variable",
   192       Markup.TFREE -> "free type variable",
   193       Markup.TVAR -> "schematic type variable")
   194 
   195   val tooltip_elements =
   196     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
   197       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
   198       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
   199       Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
   200 
   201   val tooltip_message_elements =
   202     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
   203       Markup.BAD)
   204 
   205   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
   206     Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
   207 
   208   val caret_focus_elements = Markup.Elements(Markup.ENTITY)
   209 
   210   val text_color_elements = Markup.Elements(text_color.keySet)
   211 }
   212 
   213 abstract class Rendering(
   214   val snapshot: Document.Snapshot,
   215   val options: Options,
   216   val resources: Resources)
   217 {
   218   override def toString: String = "Rendering(" + snapshot.toString + ")"
   219 
   220 
   221   /* completion */
   222 
   223   def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
   224       : Option[Text.Info[Completion.Semantic]] =
   225     if (snapshot.is_outdated) None
   226     else {
   227       snapshot.select(range, Rendering.semantic_completion_elements, _ =>
   228         {
   229           case Completion.Semantic.Info(info) =>
   230             completed_range match {
   231               case Some(range0) if range0.contains(info.range) && range0 != info.range => None
   232               case _ => Some(info)
   233             }
   234           case _ => None
   235         }).headOption.map(_.info)
   236     }
   237 
   238 
   239   /* spell checker */
   240 
   241   private lazy val spell_checker_elements =
   242     Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
   243 
   244   def spell_checker_ranges(range: Text.Range): List[Text.Range] =
   245     snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
   246 
   247   def spell_checker_point(range: Text.Range): Option[Text.Range] =
   248     snapshot.select(range, spell_checker_elements, _ =>
   249       {
   250         case info => Some(snapshot.convert(info.range))
   251       }).headOption.map(_.info)
   252 
   253 
   254   /* tooltips */
   255 
   256   def timing_threshold: Double
   257 
   258   private sealed case class Tooltip_Info(
   259     range: Text.Range,
   260     timing: Timing = Timing.zero,
   261     messages: List[Command.Results.Entry] = Nil,
   262     rev_infos: List[(Boolean, XML.Tree)] = Nil)
   263   {
   264     def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
   265     def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
   266     {
   267       val r = snapshot.convert(r0)
   268       if (range == r) copy(messages = (serial -> tree) :: messages)
   269       else copy(range = r, messages = List(serial -> tree))
   270     }
   271     def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
   272     {
   273       val r = snapshot.convert(r0)
   274       if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
   275       else copy (range = r, rev_infos = List(important -> tree))
   276     }
   277     def infos(important: Boolean): List[XML.Tree] =
   278       rev_infos.filter(p => p._1 == important).reverse.map(_._2)
   279   }
   280 
   281   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   282   {
   283     val results =
   284       snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ =>
   285         {
   286           case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
   287 
   288           case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   289           if Rendering.tooltip_message_elements(name) && body.nonEmpty =>
   290             Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body)))
   291 
   292           case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
   293           if kind != "" && kind != Markup.ML_DEF =>
   294             val kind1 = Word.implode(Word.explode('_', kind))
   295             val txt1 =
   296               if (name == "") kind1
   297               else if (kind1 == "") quote(name)
   298               else kind1 + " " + quote(name)
   299             val txt2 =
   300               if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold)
   301                 "\n" + info.timing.message
   302               else ""
   303             Some(info + (r0, true, XML.Text(txt1 + txt2)))
   304 
   305           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
   306             val file = resources.append_file(snapshot.node_name.master_dir, name)
   307             val text =
   308               if (name == file) "file " + quote(file)
   309               else "path " + quote(name) + "\nfile " + quote(file)
   310             Some(info + (r0, true, XML.Text(text)))
   311 
   312           case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
   313             val text = "doc " + quote(name)
   314             Some(info + (r0, true, XML.Text(text)))
   315 
   316           case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
   317             Some(info + (r0, true, XML.Text("URL " + quote(name))))
   318 
   319           case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
   320           if name == Markup.SORTING || name == Markup.TYPING =>
   321             Some(info + (r0, true, Rendering.pretty_typing("::", body)))
   322 
   323           case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   324             Some(info + (r0, true, Pretty.block(0, body)))
   325 
   326           case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   327             Some(info + (r0, false, Rendering.pretty_typing("ML:", body)))
   328 
   329           case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
   330             val text =
   331               if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   332               else "breakpoint (disabled)"
   333             Some(info + (r0, true, XML.Text(text)))
   334 
   335           case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   336             val lang = Word.implode(Word.explode('_', language))
   337             Some(info + (r0, true, XML.Text("language: " + lang)))
   338 
   339           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
   340             val descr = if (kind == "") "expression" else "expression: " + kind
   341             Some(info + (r0, true, XML.Text(descr)))
   342 
   343           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   344             Some(info + (r0, true, XML.Text("Markdown: paragraph")))
   345           case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
   346             Some(info + (r0, true, XML.Text("Markdown: " + kind)))
   347 
   348           case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
   349             Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
   350         }).map(_.info)
   351 
   352     if (results.isEmpty) None
   353     else {
   354       val r = Text.Range(results.head.range.start, results.last.range.stop)
   355       val all_tips =
   356         Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList :::
   357         results.flatMap(res => res.infos(true)) :::
   358         results.flatMap(res => res.infos(false)).lastOption.toList
   359       if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
   360     }
   361   }
   362 
   363 
   364   /* text background */
   365 
   366   def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
   367   {
   368     for {
   369       Text.Info(r, result) <-
   370         snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
   371           range, (List(Markup.Empty), None), Rendering.background_elements,
   372           command_states =>
   373             {
   374               case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
   375               if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
   376                 Some((markup :: markups, color))
   377               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   378                 Some((Nil, Some(Rendering.Color.bad)))
   379               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   380                 Some((Nil, Some(Rendering.Color.intensify)))
   381               case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   382                 props match {
   383                   case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
   384                   case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
   385                   case _ => None
   386                 }
   387               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
   388                 val color =
   389                   depth match {
   390                     case 1 => Rendering.Color.markdown_item1
   391                     case 2 => Rendering.Color.markdown_item2
   392                     case 3 => Rendering.Color.markdown_item3
   393                     case _ => Rendering.Color.markdown_item4
   394                   }
   395                 Some((Nil, Some(color)))
   396               case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   397                 command_states.collectFirst(
   398                   { case st if st.results.defined(serial) => st.results.get(serial).get }) match
   399                 {
   400                   case Some(Protocol.Dialog_Result(res)) if res == result =>
   401                     Some((Nil, Some(Rendering.Color.active_result)))
   402                   case _ =>
   403                     Some((Nil, Some(Rendering.Color.active)))
   404                 }
   405               case (_, Text.Info(_, elem)) =>
   406                 if (Rendering.active_elements(elem.name))
   407                   Some((Nil, Some(Rendering.Color.active)))
   408                 else None
   409             })
   410       color <-
   411         (result match {
   412           case (markups, opt_color) if markups.nonEmpty =>
   413             val status = Protocol.Status.make(markups.iterator)
   414             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
   415             else if (status.is_running) Some(Rendering.Color.running1)
   416             else opt_color
   417           case (_, opt_color) => opt_color
   418         })
   419     } yield Text.Info(r, color)
   420   }
   421 
   422 
   423   /* text foreground */
   424 
   425   def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   426     snapshot.select(range, Rendering.foreground_elements, _ =>
   427       {
   428         case Text.Info(_, elem) =>
   429           if (elem.name == Markup.ANTIQUOTED) Some(Rendering.Color.antiquoted)
   430           else Some(Rendering.Color.quoted)
   431       })
   432 
   433 
   434   /* caret focus */
   435 
   436   private def entity_focus(range: Text.Range,
   437     check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
   438   {
   439     val results =
   440       snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
   441           {
   442             case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   443               props match {
   444                 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
   445                 case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
   446                 case _ => None
   447               }
   448             case _ => None
   449           })
   450     (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
   451   }
   452 
   453   def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
   454   {
   455     val focus_defs = entity_focus(caret_range)
   456     if (focus_defs.nonEmpty) focus_defs
   457     else {
   458       val visible_defs = entity_focus(visible_range)
   459       entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
   460     }
   461   }
   462 
   463   def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
   464   {
   465     val focus = caret_focus(caret_range, visible_range)
   466     if (focus.nonEmpty) {
   467       val results =
   468         snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
   469           {
   470             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   471               props match {
   472                 case Markup.Entity.Def(i) if focus(i) => Some(true)
   473                 case Markup.Entity.Ref(i) if focus(i) => Some(true)
   474                 case _ => None
   475               }
   476           })
   477       for (info <- results if info.info) yield info.range
   478     }
   479     else Nil
   480   }
   481 
   482 
   483   /* message underline color */
   484 
   485   def message_underline_color(elements: Markup.Elements, range: Text.Range)
   486     : List[Text.Info[Rendering.Color.Value]] =
   487   {
   488     val results =
   489       snapshot.cumulate[Int](range, 0, elements, _ =>
   490         {
   491           case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
   492         })
   493     for {
   494       Text.Info(r, pri) <- results
   495       color <- Rendering.message_underline_color.get(pri)
   496     } yield Text.Info(r, color)
   497   }
   498 }