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