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