src/Pure/PIDE/rendering.scala
author wenzelm
Tue Dec 27 17:33:57 2016 +0100 (2016-12-27)
changeset 64676 fd2df1ea3bb4
parent 64660 ef85bb6491b3
child 64748 155bf8632104
permissions -rw-r--r--
clarified modules;
     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   /* message priorities */
    14 
    15   val state_pri = 1
    16   val writeln_pri = 2
    17   val information_pri = 3
    18   val tracing_pri = 4
    19   val warning_pri = 5
    20   val legacy_pri = 6
    21   val error_pri = 7
    22 
    23   val message_pri = Map(
    24     Markup.STATE -> state_pri,
    25     Markup.STATE_MESSAGE -> state_pri,
    26     Markup.WRITELN -> writeln_pri,
    27     Markup.WRITELN_MESSAGE -> writeln_pri,
    28     Markup.INFORMATION -> information_pri,
    29     Markup.INFORMATION_MESSAGE -> information_pri,
    30     Markup.TRACING -> tracing_pri,
    31     Markup.TRACING_MESSAGE -> tracing_pri,
    32     Markup.WARNING -> warning_pri,
    33     Markup.WARNING_MESSAGE -> warning_pri,
    34     Markup.LEGACY -> legacy_pri,
    35     Markup.LEGACY_MESSAGE -> legacy_pri,
    36     Markup.ERROR -> error_pri,
    37     Markup.ERROR_MESSAGE -> error_pri)
    38 
    39 
    40   /* markup elements */
    41 
    42   private val tooltip_descriptions =
    43     Map(
    44       Markup.CITATION -> "citation",
    45       Markup.TOKEN_RANGE -> "inner syntax token",
    46       Markup.FREE -> "free variable",
    47       Markup.SKOLEM -> "skolem variable",
    48       Markup.BOUND -> "bound variable",
    49       Markup.VAR -> "schematic variable",
    50       Markup.TFREE -> "free type variable",
    51       Markup.TVAR -> "schematic type variable")
    52 
    53   private val tooltip_elements =
    54     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    55       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    56       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    57       Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    58 
    59   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    60     Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    61 }
    62 
    63 abstract class Rendering(
    64   val snapshot: Document.Snapshot,
    65   val options: Options,
    66   val resources: Resources)
    67 {
    68   override def toString: String = "Rendering(" + snapshot.toString + ")"
    69 
    70 
    71   /* tooltips */
    72 
    73   def tooltip_margin: Int
    74   def timing_threshold: Double
    75 
    76   def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    77   {
    78     def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
    79       r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
    80     {
    81       val r = snapshot.convert(r0)
    82       val (t, info) = prev.info
    83       if (prev.range == r)
    84         Text.Info(r, (t, info :+ p))
    85       else Text.Info(r, (t, Vector(p)))
    86     }
    87 
    88     val results =
    89       snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    90         range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
    91         {
    92           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    93             Some(Text.Info(r, (t1 + t2, info)))
    94 
    95           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
    96           if kind != "" && kind != Markup.ML_DEF =>
    97             val kind1 = Word.implode(Word.explode('_', kind))
    98             val txt1 =
    99               if (name == "") kind1
   100               else if (kind1 == "") quote(name)
   101               else kind1 + " " + quote(name)
   102             val t = prev.info._1
   103             val txt2 =
   104               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   105                 "\n" + t.message
   106               else ""
   107             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   108 
   109           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
   110             val file = resources.append_file(snapshot.node_name.master_dir, name)
   111             val text =
   112               if (name == file) "file " + quote(file)
   113               else "path " + quote(name) + "\nfile " + quote(file)
   114             Some(add(prev, r, (true, XML.Text(text))))
   115 
   116           case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
   117             val text = "doc " + quote(name)
   118             Some(add(prev, r, (true, XML.Text(text))))
   119 
   120           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   121             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   122 
   123           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   124           if name == Markup.SORTING || name == Markup.TYPING =>
   125             Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
   126 
   127           case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   128             Some(add(prev, r, (true, Pretty.block(0, body))))
   129 
   130           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   131             Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
   132 
   133           case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
   134             val text =
   135               if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   136               else "breakpoint (disabled)"
   137             Some(add(prev, r, (true, XML.Text(text))))
   138 
   139           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   140             val lang = Word.implode(Word.explode('_', language))
   141             Some(add(prev, r, (true, XML.Text("language: " + lang))))
   142 
   143           case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
   144             val descr = if (kind == "") "expression" else "expression: " + kind
   145             Some(add(prev, r, (true, XML.Text(descr))))
   146 
   147           case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   148             Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
   149           case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
   150             Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
   151 
   152           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   153             Rendering.tooltip_descriptions.get(name).
   154               map(descr => add(prev, r, (true, XML.Text(descr))))
   155         }).map(_.info)
   156 
   157     results.map(_.info).flatMap(res => res._2.toList) match {
   158       case Nil => None
   159       case tips =>
   160         val r = Text.Range(results.head.range.start, results.last.range.stop)
   161         val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   162         Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
   163     }
   164   }
   165 }