src/Pure/PIDE/rendering.scala
author wenzelm
Sat Mar 04 13:36:06 2017 +0100 (2017-03-04)
changeset 65104 66b19d05dcee
parent 65101 4263b2a201b3
child 65107 70b0113fa4ef
permissions -rw-r--r--
decorations for background and foreground 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 = values
    30 
    31     // foreground
    32     val quoted = Value("quoted")
    33     val antiquoted = Value("antiquoted")
    34     val foreground = values -- background
    35   }
    36 
    37 
    38   /* message priorities */
    39 
    40   val state_pri = 1
    41   val writeln_pri = 2
    42   val information_pri = 3
    43   val tracing_pri = 4
    44   val warning_pri = 5
    45   val legacy_pri = 6
    46   val error_pri = 7
    47 
    48   val message_pri = Map(
    49     Markup.STATE -> state_pri,
    50     Markup.STATE_MESSAGE -> state_pri,
    51     Markup.WRITELN -> writeln_pri,
    52     Markup.WRITELN_MESSAGE -> writeln_pri,
    53     Markup.INFORMATION -> information_pri,
    54     Markup.INFORMATION_MESSAGE -> information_pri,
    55     Markup.TRACING -> tracing_pri,
    56     Markup.TRACING_MESSAGE -> tracing_pri,
    57     Markup.WARNING -> warning_pri,
    58     Markup.WARNING_MESSAGE -> warning_pri,
    59     Markup.LEGACY -> legacy_pri,
    60     Markup.LEGACY_MESSAGE -> legacy_pri,
    61     Markup.ERROR -> error_pri,
    62     Markup.ERROR_MESSAGE -> error_pri)
    63 
    64 
    65   /* markup elements */
    66 
    67   val active_elements =
    68     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    69       Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
    70 
    71   private val background_elements =
    72     Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
    73       Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    74       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    75       Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    76       Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
    77       Markup.Markdown_Item.name ++ active_elements
    78 
    79   private val foreground_elements =
    80     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    81       Markup.CARTOUCHE, Markup.ANTIQUOTED)
    82 
    83   private val semantic_completion_elements =
    84     Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    85 
    86   private val tooltip_descriptions =
    87     Map(
    88       Markup.CITATION -> "citation",
    89       Markup.TOKEN_RANGE -> "inner syntax token",
    90       Markup.FREE -> "free variable",
    91       Markup.SKOLEM -> "skolem variable",
    92       Markup.BOUND -> "bound variable",
    93       Markup.VAR -> "schematic variable",
    94       Markup.TFREE -> "free type variable",
    95       Markup.TVAR -> "schematic type variable")
    96 
    97   private val tooltip_elements =
    98     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    99       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
   100       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
   101       Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
   102 
   103   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
   104     Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
   105 
   106   val caret_focus_elements = Markup.Elements(Markup.ENTITY)
   107 }
   108 
   109 abstract class Rendering(
   110   val snapshot: Document.Snapshot,
   111   val options: Options,
   112   val resources: Resources)
   113 {
   114   override def toString: String = "Rendering(" + snapshot.toString + ")"
   115 
   116 
   117   /* completion */
   118 
   119   def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
   120       : Option[Text.Info[Completion.Semantic]] =
   121     if (snapshot.is_outdated) None
   122     else {
   123       snapshot.select(range, Rendering.semantic_completion_elements, _ =>
   124         {
   125           case Completion.Semantic.Info(info) =>
   126             completed_range match {
   127               case Some(range0) if range0.contains(info.range) && range0 != info.range => None
   128               case _ => Some(info)
   129             }
   130           case _ => None
   131         }).headOption.map(_.info)
   132     }
   133 
   134 
   135   /* tooltips */
   136 
   137   def tooltip_margin: Int
   138   def timing_threshold: Double
   139 
   140   def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   141   {
   142     def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
   143       r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
   144     {
   145       val r = snapshot.convert(r0)
   146       val (t, info) = prev.info
   147       if (prev.range == r)
   148         Text.Info(r, (t, info :+ p))
   149       else Text.Info(r, (t, Vector(p)))
   150     }
   151 
   152     val results =
   153       snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
   154         range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
   155         {
   156           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   157             Some(Text.Info(r, (t1 + t2, info)))
   158 
   159           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
   160           if kind != "" && kind != Markup.ML_DEF =>
   161             val kind1 = Word.implode(Word.explode('_', kind))
   162             val txt1 =
   163               if (name == "") kind1
   164               else if (kind1 == "") quote(name)
   165               else kind1 + " " + quote(name)
   166             val t = prev.info._1
   167             val txt2 =
   168               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   169                 "\n" + t.message
   170               else ""
   171             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   172 
   173           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
   174             val file = resources.append_file(snapshot.node_name.master_dir, name)
   175             val text =
   176               if (name == file) "file " + quote(file)
   177               else "path " + quote(name) + "\nfile " + quote(file)
   178             Some(add(prev, r, (true, XML.Text(text))))
   179 
   180           case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
   181             val text = "doc " + quote(name)
   182             Some(add(prev, r, (true, XML.Text(text))))
   183 
   184           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   185             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   186 
   187           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   188           if name == Markup.SORTING || name == Markup.TYPING =>
   189             Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
   190 
   191           case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   192             Some(add(prev, r, (true, Pretty.block(0, body))))
   193 
   194           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   195             Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
   196 
   197           case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
   198             val text =
   199               if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   200               else "breakpoint (disabled)"
   201             Some(add(prev, r, (true, XML.Text(text))))
   202 
   203           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   204             val lang = Word.implode(Word.explode('_', language))
   205             Some(add(prev, r, (true, XML.Text("language: " + lang))))
   206 
   207           case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
   208             val descr = if (kind == "") "expression" else "expression: " + kind
   209             Some(add(prev, r, (true, XML.Text(descr))))
   210 
   211           case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   212             Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
   213           case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
   214             Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
   215 
   216           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   217             Rendering.tooltip_descriptions.get(name).
   218               map(descr => add(prev, r, (true, XML.Text(descr))))
   219         }).map(_.info)
   220 
   221     results.map(_.info).flatMap(res => res._2.toList) match {
   222       case Nil => None
   223       case tips =>
   224         val r = Text.Range(results.head.range.start, results.last.range.stop)
   225         val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   226         Some(Text.Info(r, all_tips))
   227     }
   228   }
   229 
   230 
   231   /* text background */
   232 
   233   def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
   234   {
   235     for {
   236       Text.Info(r, result) <-
   237         snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
   238           range, (List(Markup.Empty), None), Rendering.background_elements,
   239           command_states =>
   240             {
   241               case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
   242               if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
   243                 Some((markup :: markups, color))
   244               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   245                 Some((Nil, Some(Rendering.Color.bad)))
   246               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   247                 Some((Nil, Some(Rendering.Color.intensify)))
   248               case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   249                 props match {
   250                   case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
   251                   case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
   252                   case _ => None
   253                 }
   254               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
   255                 val color =
   256                   depth match {
   257                     case 1 => Rendering.Color.markdown_item1
   258                     case 2 => Rendering.Color.markdown_item2
   259                     case 3 => Rendering.Color.markdown_item3
   260                     case _ => Rendering.Color.markdown_item4
   261                   }
   262                 Some((Nil, Some(color)))
   263               case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   264                 command_states.collectFirst(
   265                   { case st if st.results.defined(serial) => st.results.get(serial).get }) match
   266                 {
   267                   case Some(Protocol.Dialog_Result(res)) if res == result =>
   268                     Some((Nil, Some(Rendering.Color.active_result)))
   269                   case _ =>
   270                     Some((Nil, Some(Rendering.Color.active)))
   271                 }
   272               case (_, Text.Info(_, elem)) =>
   273                 if (Rendering.active_elements(elem.name))
   274                   Some((Nil, Some(Rendering.Color.active)))
   275                 else None
   276             })
   277       color <-
   278         (result match {
   279           case (markups, opt_color) if markups.nonEmpty =>
   280             val status = Protocol.Status.make(markups.iterator)
   281             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
   282             else if (status.is_running) Some(Rendering.Color.running1)
   283             else opt_color
   284           case (_, opt_color) => opt_color
   285         })
   286     } yield Text.Info(r, color)
   287   }
   288 
   289 
   290   /* text foreground */
   291 
   292   def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   293     snapshot.select(range, Rendering.foreground_elements, _ =>
   294       {
   295         case Text.Info(_, elem) =>
   296           if (elem.name == Markup.ANTIQUOTED) Some(Rendering.Color.antiquoted)
   297           else Some(Rendering.Color.quoted)
   298       })
   299 
   300 
   301   /* caret focus */
   302 
   303   private def entity_focus(range: Text.Range,
   304     check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
   305   {
   306     val results =
   307       snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
   308           {
   309             case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   310               props match {
   311                 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
   312                 case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
   313                 case _ => None
   314               }
   315             case _ => None
   316           })
   317     (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
   318   }
   319 
   320   def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
   321   {
   322     val focus_defs = entity_focus(caret_range)
   323     if (focus_defs.nonEmpty) focus_defs
   324     else {
   325       val visible_defs = entity_focus(visible_range)
   326       entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
   327     }
   328   }
   329 
   330   def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
   331   {
   332     val focus = caret_focus(caret_range, visible_range)
   333     if (focus.nonEmpty) {
   334       val results =
   335         snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
   336           {
   337             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   338               props match {
   339                 case Markup.Entity.Def(i) if focus(i) => Some(true)
   340                 case Markup.Entity.Ref(i) if focus(i) => Some(true)
   341                 case _ => None
   342               }
   343           })
   344       for (info <- results if info.info) yield info.range
   345     }
   346     else Nil
   347   }
   348 }