src/Tools/jEdit/src/jedit_rendering.scala
author wenzelm
Mon Mar 11 18:58:06 2019 +0100 (2 months ago ago)
changeset 70079 990c6e8faf2c
parent 69666 c95edf19133b
child 70145 396e0120f7b8
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/jedit_rendering.scala
     2     Author:     Makarius
     3 
     4 Isabelle/jEdit-specific implementation of quasi-abstract rendering and
     5 markup interpretation.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.Color
    14 import javax.swing.Icon
    15 
    16 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
    17 import org.gjt.sp.jedit.jEdit
    18 
    19 import scala.collection.immutable.SortedMap
    20 
    21 
    22 object JEdit_Rendering
    23 {
    24   def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
    25     new JEdit_Rendering(snapshot, model, options)
    26 
    27 
    28   /* popup window bounds */
    29 
    30   def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
    31 
    32 
    33   /* Isabelle/Isar token markup */
    34 
    35   private val command_style: Map[String, Byte] =
    36   {
    37     import JEditToken._
    38     Map[String, Byte](
    39       Keyword.THY_END -> KEYWORD2,
    40       Keyword.PRF_ASM -> KEYWORD3,
    41       Keyword.PRF_ASM_GOAL -> KEYWORD3
    42     ).withDefaultValue(KEYWORD1)
    43   }
    44 
    45   private val token_style: Map[Token.Kind.Value, Byte] =
    46   {
    47     import JEditToken._
    48     Map[Token.Kind.Value, Byte](
    49       Token.Kind.KEYWORD -> KEYWORD2,
    50       Token.Kind.IDENT -> NULL,
    51       Token.Kind.LONG_IDENT -> NULL,
    52       Token.Kind.SYM_IDENT -> NULL,
    53       Token.Kind.VAR -> NULL,
    54       Token.Kind.TYPE_IDENT -> NULL,
    55       Token.Kind.TYPE_VAR -> NULL,
    56       Token.Kind.NAT -> NULL,
    57       Token.Kind.FLOAT -> NULL,
    58       Token.Kind.SPACE -> NULL,
    59       Token.Kind.STRING -> LITERAL1,
    60       Token.Kind.ALT_STRING -> LITERAL2,
    61       Token.Kind.VERBATIM -> COMMENT3,
    62       Token.Kind.CARTOUCHE -> COMMENT4,
    63       Token.Kind.INFORMAL_COMMENT -> COMMENT1,
    64       Token.Kind.FORMAL_COMMENT -> COMMENT1,
    65       Token.Kind.ERROR -> INVALID
    66     ).withDefaultValue(NULL)
    67   }
    68 
    69   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
    70     if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
    71     else if (token.is_delimiter) JEditToken.OPERATOR
    72     else token_style(token.kind)
    73 
    74 
    75   /* Isabelle/ML token markup */
    76 
    77   private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
    78   {
    79     import JEditToken._
    80     Map[ML_Lex.Kind.Value, Byte](
    81       ML_Lex.Kind.KEYWORD -> NULL,
    82       ML_Lex.Kind.IDENT -> NULL,
    83       ML_Lex.Kind.LONG_IDENT -> NULL,
    84       ML_Lex.Kind.TYPE_VAR -> NULL,
    85       ML_Lex.Kind.WORD -> DIGIT,
    86       ML_Lex.Kind.INT -> DIGIT,
    87       ML_Lex.Kind.REAL -> DIGIT,
    88       ML_Lex.Kind.CHAR -> LITERAL2,
    89       ML_Lex.Kind.STRING -> LITERAL1,
    90       ML_Lex.Kind.SPACE -> NULL,
    91       ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1,
    92       ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1,
    93       ML_Lex.Kind.ANTIQ -> NULL,
    94       ML_Lex.Kind.ANTIQ_START -> LITERAL4,
    95       ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
    96       ML_Lex.Kind.ANTIQ_OTHER -> NULL,
    97       ML_Lex.Kind.ANTIQ_STRING -> NULL,
    98       ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL,
    99       ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL,
   100       ML_Lex.Kind.ERROR -> INVALID
   101     ).withDefaultValue(NULL)
   102   }
   103 
   104   def ml_token_markup(token: ML_Lex.Token): Byte =
   105     if (!token.is_keyword) ml_token_style(token.kind)
   106     else if (token.is_delimiter) JEditToken.OPERATOR
   107     else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
   108     else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
   109     else JEditToken.KEYWORD1
   110 
   111 
   112   /* markup elements */
   113 
   114   private val indentation_elements =
   115     Markup.Elements(Markup.Command_Indent.name)
   116 
   117   private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
   118 
   119   private val highlight_elements =
   120     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
   121       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL,
   122       Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM,
   123       Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
   124       Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
   125 
   126   private val hyperlink_elements =
   127     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.POSITION,
   128       Markup.CITATION)
   129 
   130   private val gutter_elements =
   131     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
   132 
   133   private val squiggly_elements =
   134     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
   135 
   136   private val line_background_elements =
   137     Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
   138       Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE,
   139       Markup.ERROR_MESSAGE)
   140 
   141   private val separator_elements =
   142     Markup.Elements(Markup.SEPARATOR)
   143 
   144   private val bullet_elements =
   145     Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT)
   146 
   147   private val fold_depth_elements =
   148     Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   149 }
   150 
   151 
   152 class JEdit_Rendering(snapshot: Document.Snapshot, _model: Document_Model, options: Options)
   153   extends Rendering(snapshot, options, PIDE.session)
   154 {
   155   def model: Document_Model = _model
   156 
   157 
   158   /* colors */
   159 
   160   def color(s: String): Color =
   161     if (s == "main_color") main_color
   162     else Color_Value(options.string(s))
   163 
   164   def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
   165 
   166   lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
   167     Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
   168 
   169   val main_color = jEdit.getColorProperty("view.fgColor")
   170 
   171   val outdated_color = color("outdated_color")
   172   val bullet_color = color("bullet_color")
   173   val tooltip_color = color("tooltip_color")
   174   val spell_checker_color = color("spell_checker_color")
   175   val entity_ref_color = color("entity_ref_color")
   176   val breakpoint_disabled_color = color("breakpoint_disabled_color")
   177   val breakpoint_enabled_color = color("breakpoint_enabled_color")
   178   val caret_debugger_color = color("caret_debugger_color")
   179   val highlight_color = color("highlight_color")
   180   val hyperlink_color = color("hyperlink_color")
   181   val active_hover_color = color("active_hover_color")
   182   val caret_invisible_color = color("caret_invisible_color")
   183   val completion_color = color("completion_color")
   184   val search_color = color("search_color")
   185 
   186 
   187   /* indentation */
   188 
   189   def indentation(range: Text.Range): Int =
   190     snapshot.select(range, JEdit_Rendering.indentation_elements, _ =>
   191       {
   192         case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i)
   193         case _ => None
   194       }).headOption.map(_.info).getOrElse(0)
   195 
   196 
   197   /* breakpoints */
   198 
   199   def breakpoint(range: Text.Range): Option[(Command, Long)] =
   200     if (snapshot.is_outdated) None
   201     else
   202       snapshot.select(range, JEdit_Rendering.breakpoint_elements, command_states =>
   203         {
   204           case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
   205             command_states match {
   206               case st :: _ => Some((st.command, breakpoint))
   207               case _ => None
   208             }
   209           case _ => None
   210         }).headOption.map(_.info)
   211 
   212 
   213   /* caret focus */
   214 
   215   def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
   216     snapshot.select(range, Rendering.caret_focus_elements, _ =>
   217       {
   218         case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) =>
   219           Some(entity_ref_color)
   220         case _ => None
   221       })
   222 
   223 
   224   /* highlighted area */
   225 
   226   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   227     snapshot.select(range, JEdit_Rendering.highlight_elements, _ =>
   228       {
   229         case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
   230       }).headOption.map(_.info)
   231 
   232 
   233   /* hyperlinks */
   234 
   235   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   236   {
   237     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
   238       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
   239         {
   240           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
   241             val file = perhaps_append_file(snapshot.node_name, name)
   242             val link = PIDE.editor.hyperlink_file(true, file)
   243             Some(links :+ Text.Info(snapshot.convert(info_range), link))
   244 
   245           case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
   246             PIDE.editor.hyperlink_doc(name).map(link =>
   247               (links :+ Text.Info(snapshot.convert(info_range), link)))
   248 
   249           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
   250             val link = PIDE.editor.hyperlink_url(name)
   251             Some(links :+ Text.Info(snapshot.convert(info_range), link))
   252 
   253           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   254             val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
   255             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
   256 
   257           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
   258             val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
   259             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
   260 
   261           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
   262             val opt_link =
   263               Document_Model.bibtex_entries_iterator().collectFirst(
   264                 { case Text.Info(entry_range, (entry, model)) if entry == name =>
   265                     PIDE.editor.hyperlink_model(true, model, entry_range.start) })
   266             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
   267 
   268           case _ => None
   269         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   270   }
   271 
   272 
   273   /* active elements */
   274 
   275   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
   276     snapshot.select(range, Rendering.active_elements, command_states =>
   277       {
   278         case Text.Info(info_range, elem) =>
   279           if (elem.name == Markup.DIALOG) {
   280             elem match {
   281               case Protocol.Dialog(_, serial, _)
   282               if !command_states.exists(st => st.results.defined(serial)) =>
   283                 Some(Text.Info(snapshot.convert(info_range), elem))
   284               case _ => None
   285             }
   286           }
   287           else Some(Text.Info(snapshot.convert(info_range), elem))
   288       }).headOption.map(_.info)
   289 
   290 
   291   /* tooltips */
   292 
   293   def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   294   override def timing_threshold: Double = options.real("jedit_timing_threshold")
   295 
   296   def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
   297     tooltips(Rendering.tooltip_elements, range).map(info => info.map(Pretty.fbreaks(_)))
   298 
   299   def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
   300     tooltips(Rendering.tooltip_message_elements, range).map(info => info.map(Pretty.fbreaks(_)))
   301 
   302   lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   303   lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
   304 
   305 
   306   /* gutter */
   307 
   308   private def gutter_message_pri(msg: XML.Tree): Int =
   309     if (Protocol.is_error(msg)) Rendering.error_pri
   310     else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
   311     else if (Protocol.is_warning(msg)) Rendering.warning_pri
   312     else if (Protocol.is_information(msg)) Rendering.information_pri
   313     else 0
   314 
   315   private lazy val gutter_message_content = Map(
   316     Rendering.information_pri ->
   317       (JEdit_Lib.load_icon(options.string("gutter_information_icon")),
   318         color(Rendering.Color.information_message)),
   319     Rendering.warning_pri ->
   320       (JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
   321         color(Rendering.Color.warning_message)),
   322     Rendering.legacy_pri ->
   323       (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
   324         color(Rendering.Color.legacy_message)),
   325     Rendering.error_pri ->
   326       (JEdit_Lib.load_icon(options.string("gutter_error_icon")),
   327         color(Rendering.Color.error_message)))
   328 
   329   def gutter_content(range: Text.Range): Option[(Icon, Color)] =
   330   {
   331     val pris =
   332       snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
   333         {
   334           case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
   335             Some(pri max gutter_message_pri(msg))
   336           case _ => None
   337         }).map(_.info)
   338 
   339     gutter_message_content.get((0 /: pris)(_ max _))
   340   }
   341 
   342 
   343   /* message output */
   344 
   345   def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   346     message_underline_color(JEdit_Rendering.squiggly_elements, range)
   347 
   348   def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] =
   349   {
   350     val results =
   351       snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
   352         {
   353           case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
   354         })
   355     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   356 
   357     Rendering.message_background_color.get(pri).map(message_color =>
   358       {
   359         val is_separator =
   360           snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ =>
   361             {
   362               case _ => Some(true)
   363             }).exists(_.info)
   364         (message_color, is_separator)
   365       })
   366   }
   367 
   368 
   369   /* text color */
   370 
   371   def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] =
   372   {
   373     if (current_color == Syntax_Style.hidden_color) List(Text.Info(range, current_color))
   374     else
   375       snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
   376         {
   377           case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color(_))
   378         })
   379   }
   380 
   381 
   382   /* virtual bullets */
   383 
   384   def bullet(range: Text.Range): List[Text.Info[Color]] =
   385     snapshot.select(range, JEdit_Rendering.bullet_elements, _ =>
   386       {
   387         case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
   388           PIDE.session.debugger.active_breakpoint_state(breakpoint).map(b =>
   389             if (b) breakpoint_enabled_color else breakpoint_disabled_color)
   390         case _ => Some(bullet_color)
   391       })
   392 
   393 
   394   /* text folds */
   395 
   396   def fold_depth(range: Text.Range): List[Text.Info[Int]] =
   397     snapshot.cumulate[Int](range, 0, JEdit_Rendering.fold_depth_elements, _ =>
   398       {
   399         case (depth, _) => Some(depth + 1)
   400       })
   401 }