src/Tools/jEdit/src/jedit_rendering.scala
author wenzelm
Sun, 13 Dec 2020 17:48:51 +0100
changeset 72901 16fd39c9e31f
parent 72900 c9813630cca4
child 72902 3c09adb4b042
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 64621
diff changeset
     1
/*  Title:      Tools/jEdit/src/jedit_rendering.scala
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     3
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 64621
diff changeset
     4
Isabelle/jEdit-specific implementation of quasi-abstract rendering and
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50196
diff changeset
     5
markup interpretation.
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     6
*/
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     7
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     8
package isabelle.jedit
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     9
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    10
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    11
import isabelle._
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    12
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    13
import java.awt.Color
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    14
import javax.swing.Icon
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    15
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    16
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
61175
1d9c121cbe4d avoid hardwired colors;
wenzelm
parents: 61011
diff changeset
    17
import org.gjt.sp.jedit.jEdit
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    18
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
    19
import scala.collection.immutable.SortedMap
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
    20
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    21
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
    22
object JEdit_Rendering
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    23
{
72718
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    24
  /* make rendering */
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    25
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66082
diff changeset
    26
  def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
c137a9f038a6 clarified signature;
wenzelm
parents: 66082
diff changeset
    27
    new JEdit_Rendering(snapshot, model, options)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    28
72718
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    29
  def text(snapshot: Document.Snapshot, formatted_body: XML.Body,
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    30
    results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) =
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    31
  {
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    32
    val command = Command.rich_text(Document_ID.make(), results, formatted_body)
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    33
    val snippet = snapshot.command_snippet(command)
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    34
    val model = File_Model.empty(PIDE.session)
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    35
    val rendering = apply(snippet, model, PIDE.options.value)
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    36
    (command.source, rendering)
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    37
  }
59a7f82a7180 clarified signature;
wenzelm
parents: 71601
diff changeset
    38
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
    39
53230
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 52980
diff changeset
    40
  /* popup window bounds */
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 52980
diff changeset
    41
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 52980
diff changeset
    42
  def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 52980
diff changeset
    43
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 52980
diff changeset
    44
55501
fdde1d62e1fb refined ML keyword styles;
wenzelm
parents: 55500
diff changeset
    45
  /* Isabelle/Isar token markup */
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    46
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    47
  private val command_style: Map[String, Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    48
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    49
    import JEditToken._
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    50
    Map[String, Byte](
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    51
      Keyword.THY_END -> KEYWORD2,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    52
      Keyword.PRF_ASM -> KEYWORD3,
59125
ee19c92ae8b4 more explicit markup for improper commands;
wenzelm
parents: 59118
diff changeset
    53
      Keyword.PRF_ASM_GOAL -> KEYWORD3
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    54
    ).withDefaultValue(KEYWORD1)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    55
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    56
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    57
  private val token_style: Map[Token.Kind.Value, Byte] =
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    58
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    59
    import JEditToken._
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    60
    Map[Token.Kind.Value, Byte](
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    61
      Token.Kind.KEYWORD -> KEYWORD2,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    62
      Token.Kind.IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    63
      Token.Kind.LONG_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    64
      Token.Kind.SYM_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    65
      Token.Kind.VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    66
      Token.Kind.TYPE_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    67
      Token.Kind.TYPE_VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    68
      Token.Kind.NAT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    69
      Token.Kind.FLOAT -> NULL,
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 58901
diff changeset
    70
      Token.Kind.SPACE -> NULL,
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
    71
      Token.Kind.STRING -> LITERAL1,
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
    72
      Token.Kind.ALT_STRING -> LITERAL2,
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    73
      Token.Kind.VERBATIM -> COMMENT3,
69963
396e0120f7b8 clarified rendering: use COMMENT4 elsewhere;
wenzelm
parents: 69898
diff changeset
    74
      Token.Kind.CARTOUCHE -> COMMENT3,
67439
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 67438
diff changeset
    75
      Token.Kind.INFORMAL_COMMENT -> COMMENT1,
78759a7bd874 more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents: 67438
diff changeset
    76
      Token.Kind.FORMAL_COMMENT -> COMMENT1,
48754
c2c1e5944536 clarified undefined, unparsed, unfinished command spans;
wenzelm
parents: 48751
diff changeset
    77
      Token.Kind.ERROR -> INVALID
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    78
    ).withDefaultValue(NULL)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    79
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    80
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    81
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
63441
4c3fa4dba79f explicit kind "before_command";
wenzelm
parents: 63347
diff changeset
    82
    if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55503
diff changeset
    83
    else if (token.is_delimiter) JEditToken.OPERATOR
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    84
    else token_style(token.kind)
55500
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    85
55501
fdde1d62e1fb refined ML keyword styles;
wenzelm
parents: 55500
diff changeset
    86
fdde1d62e1fb refined ML keyword styles;
wenzelm
parents: 55500
diff changeset
    87
  /* Isabelle/ML token markup */
fdde1d62e1fb refined ML keyword styles;
wenzelm
parents: 55500
diff changeset
    88
55500
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    89
  private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    90
  {
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    91
    import JEditToken._
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    92
    Map[ML_Lex.Kind.Value, Byte](
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55503
diff changeset
    93
      ML_Lex.Kind.KEYWORD -> NULL,
55500
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    94
      ML_Lex.Kind.IDENT -> NULL,
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    95
      ML_Lex.Kind.LONG_IDENT -> NULL,
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    96
      ML_Lex.Kind.TYPE_VAR -> NULL,
55503
wenzelm
parents: 55501
diff changeset
    97
      ML_Lex.Kind.WORD -> DIGIT,
wenzelm
parents: 55501
diff changeset
    98
      ML_Lex.Kind.INT -> DIGIT,
wenzelm
parents: 55501
diff changeset
    99
      ML_Lex.Kind.REAL -> DIGIT,
55500
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
   100
      ML_Lex.Kind.CHAR -> LITERAL2,
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
   101
      ML_Lex.Kind.STRING -> LITERAL1,
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
   102
      ML_Lex.Kind.SPACE -> NULL,
67438
fdb7b995974d clarified modules;
wenzelm
parents: 67365
diff changeset
   103
      ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1,
fdb7b995974d clarified modules;
wenzelm
parents: 67365
diff changeset
   104
      ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1,
55512
75c68e05f9ea support ML antiquotations in Scala;
wenzelm
parents: 55505
diff changeset
   105
      ML_Lex.Kind.ANTIQ -> NULL,
75c68e05f9ea support ML antiquotations in Scala;
wenzelm
parents: 55505
diff changeset
   106
      ML_Lex.Kind.ANTIQ_START -> LITERAL4,
75c68e05f9ea support ML antiquotations in Scala;
wenzelm
parents: 55505
diff changeset
   107
      ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
75c68e05f9ea support ML antiquotations in Scala;
wenzelm
parents: 55505
diff changeset
   108
      ML_Lex.Kind.ANTIQ_OTHER -> NULL,
55514
8ef781e282d9 more uniform rendering of text that is formally interpreted: avoid clash with inner markup;
wenzelm
parents: 55512
diff changeset
   109
      ML_Lex.Kind.ANTIQ_STRING -> NULL,
8ef781e282d9 more uniform rendering of text that is formally interpreted: avoid clash with inner markup;
wenzelm
parents: 55512
diff changeset
   110
      ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL,
8ef781e282d9 more uniform rendering of text that is formally interpreted: avoid clash with inner markup;
wenzelm
parents: 55512
diff changeset
   111
      ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL,
55500
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
   112
      ML_Lex.Kind.ERROR -> INVALID
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
   113
    ).withDefaultValue(NULL)
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
   114
  }
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
   115
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
   116
  def ml_token_markup(token: ML_Lex.Token): Byte =
55501
fdde1d62e1fb refined ML keyword styles;
wenzelm
parents: 55500
diff changeset
   117
    if (!token.is_keyword) ml_token_style(token.kind)
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55503
diff changeset
   118
    else if (token.is_delimiter) JEditToken.OPERATOR
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55503
diff changeset
   119
    else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55503
diff changeset
   120
    else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
55501
fdde1d62e1fb refined ML keyword styles;
wenzelm
parents: 55500
diff changeset
   121
    else JEditToken.KEYWORD1
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   122
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   123
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   124
  /* markup elements */
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   125
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   126
  private val indentation_elements =
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   127
    Markup.Elements(Markup.Command_Indent.name)
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   128
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60876
diff changeset
   129
  private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60876
diff changeset
   130
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   131
  private val highlight_elements =
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58464
diff changeset
   132
    Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
69650
c95edf19133b clarified message;
wenzelm
parents: 69648
diff changeset
   133
      Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL,
69648
97ddaec3e2ae support hyperlink to theory exports;
wenzelm
parents: 67447
diff changeset
   134
      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM,
97ddaec3e2ae support hyperlink to theory exports;
wenzelm
parents: 67447
diff changeset
   135
      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
67323
d02208cefbdb PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
wenzelm
parents: 66150
diff changeset
   136
      Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   137
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   138
  private val hyperlink_elements =
70016
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69963
diff changeset
   139
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL,
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69963
diff changeset
   140
      Markup.POSITION, Markup.CITATION)
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   141
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   142
  private val gutter_elements =
59203
5f0bd5afc16d explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents: 59184
diff changeset
   143
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   144
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   145
  private val squiggly_elements =
59203
5f0bd5afc16d explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents: 59184
diff changeset
   146
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   147
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   148
  private val line_background_elements =
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 59129
diff changeset
   149
    Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
59203
5f0bd5afc16d explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents: 59184
diff changeset
   150
      Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE,
5f0bd5afc16d explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents: 59184
diff changeset
   151
      Markup.ERROR_MESSAGE)
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   152
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55790
diff changeset
   153
  private val separator_elements =
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56600
diff changeset
   154
    Markup.Elements(Markup.SEPARATOR)
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   155
55820
61869776ce1f tuned signature -- more explicit Document.Elements;
wenzelm
parents: 55790
diff changeset
   156
  private val bullet_elements =
60913
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60893
diff changeset
   157
    Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT)
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   158
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   159
  private val fold_depth_elements =
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56600
diff changeset
   160
    Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   161
}
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   162
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   163
72856
3a27e6f83ce1 clarified signature;
wenzelm
parents: 72718
diff changeset
   164
class JEdit_Rendering(snapshot: Document.Snapshot, model: Document_Model, options: Options)
65213
51c0f094dc02 proper local debugger state, depending on session;
wenzelm
parents: 65190
diff changeset
   165
  extends Rendering(snapshot, options, PIDE.session)
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   166
{
72856
3a27e6f83ce1 clarified signature;
wenzelm
parents: 72718
diff changeset
   167
  override def get_text(range: Text.Range): Option[String] = model.get_text(range)
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66082
diff changeset
   168
c137a9f038a6 clarified signature;
wenzelm
parents: 66082
diff changeset
   169
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   170
  /* colors */
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   171
65144
b5782e996651 more generic colors;
wenzelm
parents: 65139
diff changeset
   172
  def color(s: String): Color =
65145
wenzelm
parents: 65144
diff changeset
   173
    if (s == "main_color") main_color
65144
b5782e996651 more generic colors;
wenzelm
parents: 65139
diff changeset
   174
    else Color_Value(options.string(s))
b5782e996651 more generic colors;
wenzelm
parents: 65139
diff changeset
   175
b5782e996651 more generic colors;
wenzelm
parents: 65139
diff changeset
   176
  def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   177
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 65100
diff changeset
   178
  lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
65102
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   179
    Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 65100
diff changeset
   180
65145
wenzelm
parents: 65144
diff changeset
   181
  val main_color = jEdit.getColorProperty("view.fgColor")
wenzelm
parents: 65144
diff changeset
   182
65102
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   183
  val outdated_color = color("outdated_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   184
  val bullet_color = color("bullet_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   185
  val tooltip_color = color("tooltip_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   186
  val spell_checker_color = color("spell_checker_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   187
  val entity_ref_color = color("entity_ref_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   188
  val breakpoint_disabled_color = color("breakpoint_disabled_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   189
  val breakpoint_enabled_color = color("breakpoint_enabled_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   190
  val caret_debugger_color = color("caret_debugger_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   191
  val highlight_color = color("highlight_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   192
  val hyperlink_color = color("hyperlink_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   193
  val active_hover_color = color("active_hover_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   194
  val caret_invisible_color = color("caret_invisible_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   195
  val completion_color = color("completion_color")
136b620b11af tuned signature;
wenzelm
parents: 65101
diff changeset
   196
  val search_color = color("search_color")
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   197
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   198
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   199
  /* indentation */
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   200
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   201
  def indentation(range: Text.Range): Int =
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   202
    snapshot.select(range, JEdit_Rendering.indentation_elements, _ =>
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   203
      {
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   204
        case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i)
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   205
        case _ => None
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   206
      }).headOption.map(_.info).getOrElse(0)
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   207
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63441
diff changeset
   208
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60876
diff changeset
   209
  /* breakpoints */
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60876
diff changeset
   210
60880
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   211
  def breakpoint(range: Text.Range): Option[(Command, Long)] =
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   212
    if (snapshot.is_outdated) None
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   213
    else
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   214
      snapshot.select(range, JEdit_Rendering.breakpoint_elements, command_states =>
60880
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   215
        {
60882
45bfd18835f1 tuned signature;
wenzelm
parents: 60880
diff changeset
   216
          case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
60880
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   217
            command_states match {
60882
45bfd18835f1 tuned signature;
wenzelm
parents: 60880
diff changeset
   218
              case st :: _ => Some((st.command, breakpoint))
60880
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   219
              case _ => None
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   220
            }
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   221
          case _ => None
fa958e24ff24 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
wenzelm
parents: 60878
diff changeset
   222
        }).headOption.map(_.info)
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60876
diff changeset
   223
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60876
diff changeset
   224
62986
9d2fae6b31cc background color for entity def/ref focus;
wenzelm
parents: 62806
diff changeset
   225
  /* caret focus */
9d2fae6b31cc background color for entity def/ref focus;
wenzelm
parents: 62806
diff changeset
   226
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72870
diff changeset
   227
  def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
72901
16fd39c9e31f tuned signature;
wenzelm
parents: 72900
diff changeset
   228
    snapshot.select(range, Rendering.entity_elements, _ =>
62988
224e8d8a4fb8 tuned rendering;
wenzelm
parents: 62986
diff changeset
   229
      {
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72870
diff changeset
   230
        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _))
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72870
diff changeset
   231
        if focus(i) => Some(entity_ref_color)
62988
224e8d8a4fb8 tuned rendering;
wenzelm
parents: 62986
diff changeset
   232
        case _ => None
224e8d8a4fb8 tuned rendering;
wenzelm
parents: 62986
diff changeset
   233
      })
224e8d8a4fb8 tuned rendering;
wenzelm
parents: 62986
diff changeset
   234
62986
9d2fae6b31cc background color for entity def/ref focus;
wenzelm
parents: 62806
diff changeset
   235
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   236
  /* highlighted area */
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   237
49358
0fa351b1bd14 clarified markup names;
wenzelm
parents: 49356
diff changeset
   238
  def highlight(range: Text.Range): Option[Text.Info[Color]] =
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   239
    snapshot.select(range, JEdit_Rendering.highlight_elements, _ =>
55620
19dffae33cde cumulate/select wrt. precise elements guard;
wenzelm
parents: 55619
diff changeset
   240
      {
19dffae33cde cumulate/select wrt. precise elements guard;
wenzelm
parents: 55619
diff changeset
   241
        case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
55689
wenzelm
parents: 55688
diff changeset
   242
      }).headOption.map(_.info)
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   243
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   244
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   245
  /* hyperlinks */
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   246
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66053
diff changeset
   247
  def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   248
  {
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66053
diff changeset
   249
    snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   250
      range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   251
        {
56458
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56395
diff changeset
   252
          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
65488
331f09d9535e tuned signature;
wenzelm
parents: 65487
diff changeset
   253
            val file = perhaps_append_file(snapshot.node_name, name)
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66053
diff changeset
   254
            val link = PIDE.editor.hyperlink_file(true, file)
55622
ce575c2212fc clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents: 55620
diff changeset
   255
            Some(links :+ Text.Info(snapshot.convert(info_range), link))
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   256
70016
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69963
diff changeset
   257
          case (links, Text.Info(info_range, XML.Elem(Markup.Export_Path(name), _))) =>
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69963
diff changeset
   258
            val link = PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name)
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69963
diff changeset
   259
            Some(links :+ Text.Info(snapshot.convert(info_range), link))
a8142ac5e4b6 more PIDE markup and hyperlinks;
wenzelm
parents: 69963
diff changeset
   260
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61603
diff changeset
   261
          case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66053
diff changeset
   262
            PIDE.editor.hyperlink_doc(name).map(link =>
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61603
diff changeset
   263
              (links :+ Text.Info(snapshot.convert(info_range), link)))
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61603
diff changeset
   264
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 54515
diff changeset
   265
          case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66053
diff changeset
   266
            val link = PIDE.editor.hyperlink_url(name)
55622
ce575c2212fc clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents: 55620
diff changeset
   267
            Some(links :+ Text.Info(snapshot.convert(info_range), link))
54702
3daeba5130f0 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents: 54515
diff changeset
   268
64660
ef85bb6491b3 omit unused markup;
wenzelm
parents: 64654
diff changeset
   269
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66053
diff changeset
   270
            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59319
diff changeset
   271
            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   272
55545
4a9f76263ece hyperlink for visible positions;
wenzelm
parents: 55526
diff changeset
   273
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66053
diff changeset
   274
            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59319
diff changeset
   275
            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
52889
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52873
diff changeset
   276
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58464
diff changeset
   277
          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58464
diff changeset
   278
            val opt_link =
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66114
diff changeset
   279
              Document_Model.bibtex_entries_iterator().collectFirst(
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64829
diff changeset
   280
                { case Text.Info(entry_range, (entry, model)) if entry == name =>
66082
2d12a730a380 clarified modules;
wenzelm
parents: 66053
diff changeset
   281
                    PIDE.editor.hyperlink_model(true, model, entry_range.start) })
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59319
diff changeset
   282
            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 58464
diff changeset
   283
52889
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52873
diff changeset
   284
          case _ => None
55622
ce575c2212fc clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
wenzelm
parents: 55620
diff changeset
   285
        }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   286
  }
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   287
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   288
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   289
  /* active elements */
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   290
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50215
diff changeset
   291
  def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 65100
diff changeset
   292
    snapshot.select(range, Rendering.active_elements, command_states =>
55620
19dffae33cde cumulate/select wrt. precise elements guard;
wenzelm
parents: 55619
diff changeset
   293
      {
19dffae33cde cumulate/select wrt. precise elements guard;
wenzelm
parents: 55619
diff changeset
   294
        case Text.Info(info_range, elem) =>
55623
wenzelm
parents: 55622
diff changeset
   295
          if (elem.name == Markup.DIALOG) {
wenzelm
parents: 55622
diff changeset
   296
            elem match {
wenzelm
parents: 55622
diff changeset
   297
              case Protocol.Dialog(_, serial, _)
56354
a6f8c3566560 more direct command states -- merge_results is hardly ever needed;
wenzelm
parents: 56352
diff changeset
   298
              if !command_states.exists(st => st.results.defined(serial)) =>
55623
wenzelm
parents: 55622
diff changeset
   299
                Some(Text.Info(snapshot.convert(info_range), elem))
wenzelm
parents: 55622
diff changeset
   300
              case _ => None
wenzelm
parents: 55622
diff changeset
   301
            }
wenzelm
parents: 55622
diff changeset
   302
          }
wenzelm
parents: 55622
diff changeset
   303
          else Some(Text.Info(snapshot.convert(info_range), elem))
55689
wenzelm
parents: 55688
diff changeset
   304
      }).headOption.map(_.info)
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49476
diff changeset
   305
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   306
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   307
  /* tooltips */
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   308
55647
106a57dec7af more lightweight Rendering;
wenzelm
parents: 55646
diff changeset
   309
  def tooltip_margin: Int = options.int("jedit_tooltip_margin")
69898
990c6e8faf2c tuned signature;
wenzelm
parents: 69650
diff changeset
   310
  override def timing_threshold: Double = options.real("jedit_timing_threshold")
50554
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50547
diff changeset
   311
71496
5d62f797e40c tuned signature;
wenzelm
parents: 70016
diff changeset
   312
  def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] =
5d62f797e40c tuned signature;
wenzelm
parents: 70016
diff changeset
   313
  {
5d62f797e40c tuned signature;
wenzelm
parents: 70016
diff changeset
   314
    val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71496
diff changeset
   315
    tooltips(elements, range).map(info => info.map(Pretty.fbreaks))
71496
5d62f797e40c tuned signature;
wenzelm
parents: 70016
diff changeset
   316
  }
64748
155bf8632104 clarified multiple tooltips;
wenzelm
parents: 64677
diff changeset
   317
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71496
diff changeset
   318
  lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71496
diff changeset
   319
  lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
52472
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52471
diff changeset
   320
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52471
diff changeset
   321
56495
0b9334adcf05 more explicit message discrimination;
wenzelm
parents: 56458
diff changeset
   322
  /* gutter */
0b9334adcf05 more explicit message discrimination;
wenzelm
parents: 56458
diff changeset
   323
0b9334adcf05 more explicit message discrimination;
wenzelm
parents: 56458
diff changeset
   324
  private def gutter_message_pri(msg: XML.Tree): Int =
64676
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   325
    if (Protocol.is_error(msg)) Rendering.error_pri
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   326
    else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   327
    else if (Protocol.is_warning(msg)) Rendering.warning_pri
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   328
    else if (Protocol.is_information(msg)) Rendering.information_pri
56495
0b9334adcf05 more explicit message discrimination;
wenzelm
parents: 56458
diff changeset
   329
    else 0
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   330
59129
6959ceb53ac8 more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
wenzelm
parents: 59125
diff changeset
   331
  private lazy val gutter_message_content = Map(
64676
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   332
    Rendering.information_pri ->
65127
ce8b8f979afd more generic colors;
wenzelm
parents: 65125
diff changeset
   333
      (JEdit_Lib.load_icon(options.string("gutter_information_icon")),
ce8b8f979afd more generic colors;
wenzelm
parents: 65125
diff changeset
   334
        color(Rendering.Color.information_message)),
64676
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   335
    Rendering.warning_pri ->
65127
ce8b8f979afd more generic colors;
wenzelm
parents: 65125
diff changeset
   336
      (JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
ce8b8f979afd more generic colors;
wenzelm
parents: 65125
diff changeset
   337
        color(Rendering.Color.warning_message)),
64676
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   338
    Rendering.legacy_pri ->
65127
ce8b8f979afd more generic colors;
wenzelm
parents: 65125
diff changeset
   339
      (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
ce8b8f979afd more generic colors;
wenzelm
parents: 65125
diff changeset
   340
        color(Rendering.Color.legacy_message)),
64676
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   341
    Rendering.error_pri ->
65127
ce8b8f979afd more generic colors;
wenzelm
parents: 65125
diff changeset
   342
      (JEdit_Lib.load_icon(options.string("gutter_error_icon")),
ce8b8f979afd more generic colors;
wenzelm
parents: 65125
diff changeset
   343
        color(Rendering.Color.error_message)))
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   344
59129
6959ceb53ac8 more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
wenzelm
parents: 59125
diff changeset
   345
  def gutter_content(range: Text.Range): Option[(Icon, Color)] =
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   346
  {
56495
0b9334adcf05 more explicit message discrimination;
wenzelm
parents: 56458
diff changeset
   347
    val pris =
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   348
      snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   349
        {
72870
8c468d602db1 clarified: omit presumably pointless Markup.Serial (see also 0b9334adcf05);
wenzelm
parents: 72856
diff changeset
   350
          case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem))
52889
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52873
diff changeset
   351
          case _ => None
56495
0b9334adcf05 more explicit message discrimination;
wenzelm
parents: 56458
diff changeset
   352
        }).map(_.info)
0b9334adcf05 more explicit message discrimination;
wenzelm
parents: 56458
diff changeset
   353
59129
6959ceb53ac8 more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
wenzelm
parents: 59125
diff changeset
   354
    gutter_message_content.get((0 /: pris)(_ max _))
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   355
  }
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   357
65128
wenzelm
parents: 65127
diff changeset
   358
  /* message output */
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   359
65121
12c6774a8f65 more generic rendering;
wenzelm
parents: 65102
diff changeset
   360
  def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
12c6774a8f65 more generic rendering;
wenzelm
parents: 65102
diff changeset
   361
    message_underline_color(JEdit_Rendering.squiggly_elements, range)
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   362
65124
759c64c39a6f more generic colors;
wenzelm
parents: 65121
diff changeset
   363
  def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] =
49473
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49423
diff changeset
   364
  {
49474
e7ff10e1a155 clarified message background;
wenzelm
parents: 49473
diff changeset
   365
    val results =
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   366
      snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
49473
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49423
diff changeset
   367
        {
64676
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
   368
          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
49474
e7ff10e1a155 clarified message background;
wenzelm
parents: 49473
diff changeset
   369
        })
e7ff10e1a155 clarified message background;
wenzelm
parents: 49473
diff changeset
   370
    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
e7ff10e1a155 clarified message background;
wenzelm
parents: 49473
diff changeset
   371
65124
759c64c39a6f more generic colors;
wenzelm
parents: 65121
diff changeset
   372
    Rendering.message_background_color.get(pri).map(message_color =>
61719
318f324d41f5 less intrusive rendering, notably for State dockable;
wenzelm
parents: 61718
diff changeset
   373
      {
318f324d41f5 less intrusive rendering, notably for State dockable;
wenzelm
parents: 61718
diff changeset
   374
        val is_separator =
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   375
          snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ =>
61719
318f324d41f5 less intrusive rendering, notably for State dockable;
wenzelm
parents: 61718
diff changeset
   376
            {
318f324d41f5 less intrusive rendering, notably for State dockable;
wenzelm
parents: 61718
diff changeset
   377
              case _ => Some(true)
318f324d41f5 less intrusive rendering, notably for State dockable;
wenzelm
parents: 61718
diff changeset
   378
            }).exists(_.info)
318f324d41f5 less intrusive rendering, notably for State dockable;
wenzelm
parents: 61718
diff changeset
   379
        (message_color, is_separator)
318f324d41f5 less intrusive rendering, notably for State dockable;
wenzelm
parents: 61718
diff changeset
   380
      })
49473
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49423
diff changeset
   381
  }
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   382
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
   383
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   384
  /* text color */
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   385
65144
b5782e996651 more generic colors;
wenzelm
parents: 65139
diff changeset
   386
  def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] =
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   387
  {
65258
a0701669d159 clarified modules;
wenzelm
parents: 65247
diff changeset
   388
    if (current_color == Syntax_Style.hidden_color) List(Text.Info(range, current_color))
50196
94886ebf090f retain hidden_color (i.e. transparent white) instead of replacing it by semantic text color, to make control symbols more hidden and avoid "dirty" lines with some fonts;
wenzelm
parents: 50164
diff changeset
   389
    else
65144
b5782e996651 more generic colors;
wenzelm
parents: 65139
diff changeset
   390
      snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
50196
94886ebf090f retain hidden_color (i.e. transparent white) instead of replacing it by semantic text color, to make control symbols more hidden and avoid "dirty" lines with some fonts;
wenzelm
parents: 50164
diff changeset
   391
        {
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71496
diff changeset
   392
          case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color)
50196
94886ebf090f retain hidden_color (i.e. transparent white) instead of replacing it by semantic text color, to make control symbols more hidden and avoid "dirty" lines with some fonts;
wenzelm
parents: 50164
diff changeset
   393
        })
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   394
  }
50542
58bd88159f8f fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents: 50507
diff changeset
   395
58bd88159f8f fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents: 50507
diff changeset
   396
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   397
  /* virtual bullets */
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   398
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   399
  def bullet(range: Text.Range): List[Text.Info[Color]] =
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   400
    snapshot.select(range, JEdit_Rendering.bullet_elements, _ =>
60913
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60893
diff changeset
   401
      {
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60893
diff changeset
   402
        case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
65247
63d91d5de121 tuned signature;
wenzelm
parents: 65246
diff changeset
   403
          PIDE.session.debugger.active_breakpoint_state(breakpoint).map(b =>
60913
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60893
diff changeset
   404
            if (b) breakpoint_enabled_color else breakpoint_disabled_color)
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60893
diff changeset
   405
        case _ => Some(bullet_color)
7432d6bb4195 clarified breakpoint rendering;
wenzelm
parents: 60893
diff changeset
   406
      })
55626
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   407
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   408
0e2b7f04c944 tuned comments;
wenzelm
parents: 55625
diff changeset
   409
  /* text folds */
50542
58bd88159f8f fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents: 50507
diff changeset
   410
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52890
diff changeset
   411
  def fold_depth(range: Text.Range): List[Text.Info[Int]] =
64621
7116f2634e32 clarified module name;
wenzelm
parents: 63681
diff changeset
   412
    snapshot.cumulate[Int](range, 0, JEdit_Rendering.fold_depth_elements, _ =>
50542
58bd88159f8f fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents: 50507
diff changeset
   413
      {
55620
19dffae33cde cumulate/select wrt. precise elements guard;
wenzelm
parents: 55619
diff changeset
   414
        case (depth, _) => Some(depth + 1)
50542
58bd88159f8f fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents: 50507
diff changeset
   415
      })
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   416
}