src/Tools/jEdit/src/jedit_rendering.scala
changeset 64622 529bbb8977c7
parent 64621 7116f2634e32
child 64654 31b681e38c70
     1.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Dec 20 21:35:56 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Dec 20 22:24:16 2016 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -/*  Title:      Tools/jEdit/src/rendering.scala
     1.5 +/*  Title:      Tools/jEdit/src/jedit_rendering.scala
     1.6      Author:     Makarius
     1.7  
     1.8 -Isabelle-specific implementation of quasi-abstract rendering and
     1.9 +Isabelle/jEdit-specific implementation of quasi-abstract rendering and
    1.10  markup interpretation.
    1.11  */
    1.12  
    1.13 @@ -175,23 +175,6 @@
    1.14      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
    1.15        Markup.BAD)
    1.16  
    1.17 -  private val tooltip_descriptions =
    1.18 -    Map(
    1.19 -      Markup.CITATION -> "citation",
    1.20 -      Markup.TOKEN_RANGE -> "inner syntax token",
    1.21 -      Markup.FREE -> "free variable",
    1.22 -      Markup.SKOLEM -> "skolem variable",
    1.23 -      Markup.BOUND -> "bound variable",
    1.24 -      Markup.VAR -> "schematic variable",
    1.25 -      Markup.TFREE -> "free type variable",
    1.26 -      Markup.TVAR -> "schematic type variable")
    1.27 -
    1.28 -  private val tooltip_elements =
    1.29 -    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    1.30 -      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    1.31 -      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    1.32 -      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    1.33 -
    1.34    private val gutter_elements =
    1.35      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
    1.36  
    1.37 @@ -226,11 +209,9 @@
    1.38  }
    1.39  
    1.40  
    1.41 -class JEdit_Rendering private(val snapshot: Document.Snapshot, val options: Options)
    1.42 +class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
    1.43 +  extends Rendering(snapshot, options, PIDE.resources)
    1.44  {
    1.45 -  override def toString: String = "Rendering(" + snapshot.toString + ")"
    1.46 -
    1.47 -
    1.48    /* colors */
    1.49  
    1.50    def color_value(s: String): Color = Color_Value(options.string(s))
    1.51 @@ -479,18 +460,13 @@
    1.52  
    1.53    /* hyperlinks */
    1.54  
    1.55 -  private def jedit_file(name: String): String =
    1.56 -    if (Path.is_valid(name))
    1.57 -      PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
    1.58 -    else name
    1.59 -
    1.60    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    1.61    {
    1.62      snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    1.63        range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
    1.64          {
    1.65            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
    1.66 -            val link = PIDE.editor.hyperlink_file(true, jedit_file(name))
    1.67 +            val link = PIDE.editor.hyperlink_file(true, resolve_file(name))
    1.68              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    1.69  
    1.70            case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
    1.71 @@ -580,105 +556,8 @@
    1.72  
    1.73    /* tooltips */
    1.74  
    1.75 -  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    1.76 -    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    1.77 -
    1.78 -  private def timing_threshold: Double = options.real("jedit_timing_threshold")
    1.79 -
    1.80 -  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    1.81 -  {
    1.82 -    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
    1.83 -      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
    1.84 -    {
    1.85 -      val r = snapshot.convert(r0)
    1.86 -      val (t, info) = prev.info
    1.87 -      if (prev.range == r)
    1.88 -        Text.Info(r, (t, info :+ p))
    1.89 -      else Text.Info(r, (t, Vector(p)))
    1.90 -    }
    1.91 -
    1.92 -    val results =
    1.93 -      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    1.94 -        range, Text.Info(range, (Timing.zero, Vector.empty)), JEdit_Rendering.tooltip_elements, _ =>
    1.95 -        {
    1.96 -          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    1.97 -            Some(Text.Info(r, (t1 + t2, info)))
    1.98 -
    1.99 -          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
   1.100 -          if kind != "" &&
   1.101 -            kind != Markup.ML_DEF &&
   1.102 -            kind != Markup.ML_OPEN &&
   1.103 -            kind != Markup.ML_STRUCTURE =>
   1.104 -            val kind1 = Word.implode(Word.explode('_', kind))
   1.105 -            val txt1 =
   1.106 -              if (name == "") kind1
   1.107 -              else if (kind1 == "") quote(name)
   1.108 -              else kind1 + " " + quote(name)
   1.109 -            val t = prev.info._1
   1.110 -            val txt2 =
   1.111 -              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   1.112 -                "\n" + t.message
   1.113 -              else ""
   1.114 -            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   1.115 -
   1.116 -          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
   1.117 -            val file = jedit_file(name)
   1.118 -            val text =
   1.119 -              if (name == file) "file " + quote(file)
   1.120 -              else "path " + quote(name) + "\nfile " + quote(file)
   1.121 -            Some(add(prev, r, (true, XML.Text(text))))
   1.122 -
   1.123 -          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
   1.124 -            val text = "doc " + quote(name)
   1.125 -            Some(add(prev, r, (true, XML.Text(text))))
   1.126 -
   1.127 -          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   1.128 -            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   1.129 -
   1.130 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   1.131 -          if name == Markup.SORTING || name == Markup.TYPING =>
   1.132 -            Some(add(prev, r, (true, pretty_typing("::", body))))
   1.133 -
   1.134 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   1.135 -            Some(add(prev, r, (true, Pretty.block(0, body))))
   1.136 -
   1.137 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   1.138 -            Some(add(prev, r, (false, pretty_typing("ML:", body))))
   1.139 -
   1.140 -          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
   1.141 -            val text =
   1.142 -              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   1.143 -              else "breakpoint (disabled)"
   1.144 -            Some(add(prev, r, (true, XML.Text(text))))
   1.145 -
   1.146 -          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   1.147 -            val lang = Word.implode(Word.explode('_', language))
   1.148 -            Some(add(prev, r, (true, XML.Text("language: " + lang))))
   1.149 -
   1.150 -          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
   1.151 -            val descr = if (kind == "") "expression" else "expression: " + kind
   1.152 -            Some(add(prev, r, (true, XML.Text(descr))))
   1.153 -
   1.154 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   1.155 -            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
   1.156 -          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
   1.157 -            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
   1.158 -
   1.159 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   1.160 -            JEdit_Rendering.tooltip_descriptions.get(name).
   1.161 -              map(descr => add(prev, r, (true, XML.Text(descr))))
   1.162 -        }).map(_.info)
   1.163 -
   1.164 -    results.map(_.info).flatMap(res => res._2.toList) match {
   1.165 -      case Nil => None
   1.166 -      case tips =>
   1.167 -        val r = Text.Range(results.head.range.start, results.last.range.stop)
   1.168 -        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   1.169 -        Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
   1.170 -    }
   1.171 -  }
   1.172 -
   1.173    def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   1.174 +  def timing_threshold: Double = options.real("jedit_timing_threshold")
   1.175  
   1.176    lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   1.177    lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))