src/Pure/PIDE/rendering.scala
author wenzelm
Wed Jan 11 20:01:55 2017 +0100 (2017-01-11)
changeset 64877 31e9920a0dc1
parent 64767 f5c4ffdb1124
child 65101 4263b2a201b3
permissions -rw-r--r--
support for semantic completion;
     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 semantic_completion_elements =
    43     Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    44 
    45   private val tooltip_descriptions =
    46     Map(
    47       Markup.CITATION -> "citation",
    48       Markup.TOKEN_RANGE -> "inner syntax token",
    49       Markup.FREE -> "free variable",
    50       Markup.SKOLEM -> "skolem variable",
    51       Markup.BOUND -> "bound variable",
    52       Markup.VAR -> "schematic variable",
    53       Markup.TFREE -> "free type variable",
    54       Markup.TVAR -> "schematic type variable")
    55 
    56   private val tooltip_elements =
    57     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    58       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    59       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    60       Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    61 
    62   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    63     Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    64 
    65   val caret_focus_elements = Markup.Elements(Markup.ENTITY)
    66 }
    67 
    68 abstract class Rendering(
    69   val snapshot: Document.Snapshot,
    70   val options: Options,
    71   val resources: Resources)
    72 {
    73   override def toString: String = "Rendering(" + snapshot.toString + ")"
    74 
    75 
    76   /* completion */
    77 
    78   def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
    79       : Option[Text.Info[Completion.Semantic]] =
    80     if (snapshot.is_outdated) None
    81     else {
    82       snapshot.select(range, Rendering.semantic_completion_elements, _ =>
    83         {
    84           case Completion.Semantic.Info(info) =>
    85             completed_range match {
    86               case Some(range0) if range0.contains(info.range) && range0 != info.range => None
    87               case _ => Some(info)
    88             }
    89           case _ => None
    90         }).headOption.map(_.info)
    91     }
    92 
    93 
    94   /* tooltips */
    95 
    96   def tooltip_margin: Int
    97   def timing_threshold: Double
    98 
    99   def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   100   {
   101     def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
   102       r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
   103     {
   104       val r = snapshot.convert(r0)
   105       val (t, info) = prev.info
   106       if (prev.range == r)
   107         Text.Info(r, (t, info :+ p))
   108       else Text.Info(r, (t, Vector(p)))
   109     }
   110 
   111     val results =
   112       snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
   113         range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
   114         {
   115           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   116             Some(Text.Info(r, (t1 + t2, info)))
   117 
   118           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
   119           if kind != "" && kind != Markup.ML_DEF =>
   120             val kind1 = Word.implode(Word.explode('_', kind))
   121             val txt1 =
   122               if (name == "") kind1
   123               else if (kind1 == "") quote(name)
   124               else kind1 + " " + quote(name)
   125             val t = prev.info._1
   126             val txt2 =
   127               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   128                 "\n" + t.message
   129               else ""
   130             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   131 
   132           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
   133             val file = resources.append_file(snapshot.node_name.master_dir, name)
   134             val text =
   135               if (name == file) "file " + quote(file)
   136               else "path " + quote(name) + "\nfile " + quote(file)
   137             Some(add(prev, r, (true, XML.Text(text))))
   138 
   139           case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
   140             val text = "doc " + quote(name)
   141             Some(add(prev, r, (true, XML.Text(text))))
   142 
   143           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   144             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   145 
   146           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   147           if name == Markup.SORTING || name == Markup.TYPING =>
   148             Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
   149 
   150           case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   151             Some(add(prev, r, (true, Pretty.block(0, body))))
   152 
   153           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   154             Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
   155 
   156           case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
   157             val text =
   158               if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   159               else "breakpoint (disabled)"
   160             Some(add(prev, r, (true, XML.Text(text))))
   161 
   162           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   163             val lang = Word.implode(Word.explode('_', language))
   164             Some(add(prev, r, (true, XML.Text("language: " + lang))))
   165 
   166           case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
   167             val descr = if (kind == "") "expression" else "expression: " + kind
   168             Some(add(prev, r, (true, XML.Text(descr))))
   169 
   170           case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   171             Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
   172           case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
   173             Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
   174 
   175           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   176             Rendering.tooltip_descriptions.get(name).
   177               map(descr => add(prev, r, (true, XML.Text(descr))))
   178         }).map(_.info)
   179 
   180     results.map(_.info).flatMap(res => res._2.toList) match {
   181       case Nil => None
   182       case tips =>
   183         val r = Text.Range(results.head.range.start, results.last.range.stop)
   184         val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   185         Some(Text.Info(r, all_tips))
   186     }
   187   }
   188 
   189 
   190   /* caret focus */
   191 
   192   private def entity_focus(range: Text.Range,
   193     check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
   194   {
   195     val results =
   196       snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
   197           {
   198             case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   199               props match {
   200                 case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
   201                 case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
   202                 case _ => None
   203               }
   204             case _ => None
   205           })
   206     (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
   207   }
   208 
   209   def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
   210   {
   211     val focus_defs = entity_focus(caret_range)
   212     if (focus_defs.nonEmpty) focus_defs
   213     else {
   214       val visible_defs = entity_focus(visible_range)
   215       entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
   216     }
   217   }
   218 
   219   def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
   220   {
   221     val focus = caret_focus(caret_range, visible_range)
   222     if (focus.nonEmpty) {
   223       val results =
   224         snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
   225           {
   226             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   227               props match {
   228                 case Markup.Entity.Def(i) if focus(i) => Some(true)
   229                 case Markup.Entity.Ref(i) if focus(i) => Some(true)
   230                 case _ => None
   231               }
   232           })
   233       for (info <- results if info.info) yield info.range
   234     }
   235     else Nil
   236   }
   237 }