src/Tools/jEdit/src/token_markup.scala
author wenzelm
Thu, 29 Aug 2013 12:38:33 +0200
changeset 53274 1760c01f1c78
parent 53249 c95e9aee959c
child 53277 6aa348237973
permissions -rw-r--r--
maintain Completion_Popup.Text_Area as client property like Document_View; global Completion_Popup.Text_Area init/exit like SideKickPlugin; eliminated old SideKick completion -- cover all Isabelle modes uniformly; dynamic lookup of Isabelle.mode_syntax -- NB: buffer mode might be undefined in intermediate stages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/token_markup.scala
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     3
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     4
Outer syntax token markup.
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     5
*/
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     6
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     8
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
     9
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    10
import isabelle._
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    11
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    12
import java.awt.{Font, Color}
43502
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    13
import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
43491
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    14
import java.awt.geom.AffineTransform
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    15
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    16
import org.gjt.sp.util.SyntaxUtilities
44358
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
    17
import org.gjt.sp.jedit.{jEdit, Mode}
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
    18
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    19
  ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    20
import org.gjt.sp.jedit.textarea.{TextArea, Selection}
44358
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
    21
import org.gjt.sp.jedit.buffer.JEditBuffer
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
    22
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    23
import javax.swing.text.Segment
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    24
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    25
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    26
object Token_Markup
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    27
{
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    28
  /* editing support for control symbols */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    29
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    30
  val is_control_style =
53021
d0fa3f446b9d discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents: 50663
diff changeset
    31
    Set(Symbol.sub_decoded, Symbol.sup_decoded, Symbol.bold_decoded)
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    32
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    33
  def update_control_style(control: String, text: String): String =
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    34
  {
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    35
    val result = new StringBuilder
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    36
    for (sym <- Symbol.iterator(text) if !is_control_style(sym)) {
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    37
      if (Symbol.is_controllable(sym)) result ++= control
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    38
      result ++= sym
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    39
    }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    40
    result.toString
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    41
  }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    42
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    43
  def edit_control_style(text_area: TextArea, control: String)
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    44
  {
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    45
    Swing_Thread.assert()
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    46
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    47
    val buffer = text_area.getBuffer
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    48
50663
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    49
    text_area.getSelection.foreach(sel => {
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    50
      val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    51
      JEdit_Lib.try_get_text(buffer, before) match {
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    52
        case Some(s) if is_control_style(s) =>
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    53
          text_area.extendSelection(before.start, before.stop)
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    54
        case _ =>
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    55
      }
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    56
    })
f8d7d332fec0 more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
wenzelm
parents: 50210
diff changeset
    57
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    58
    text_area.getSelection.toList match {
50210
747db833fbf7 no special treatment of control_reset, in accordance to other control styles;
wenzelm
parents: 50205
diff changeset
    59
      case Nil =>
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    60
        text_area.setSelectedText(control)
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    61
      case sels =>
50195
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50187
diff changeset
    62
        JEdit_Lib.buffer_edit(buffer) {
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    63
          sels.foreach(sel =>
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    64
            text_area.setSelectedText(sel,
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    65
              update_control_style(control, text_area.getSelectedText(sel))))
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    66
        }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    67
    }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    68
  }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    69
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents: 48884
diff changeset
    70
43502
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    71
  /* font operations */
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    72
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    73
  private def font_metrics(font: Font): LineMetrics =
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    74
    font.getLineMetrics("", new FontRenderContext(null, false, false))
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    75
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    76
  private def imitate_font(family: String, font: Font): Font =
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    77
  {
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    78
    val font1 = new Font (family, font.getStyle, font.getSize)
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    79
    font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    80
  }
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    81
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    82
  private def transform_font(font: Font, transform: AffineTransform): Font =
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    83
  {
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    84
    import scala.collection.JavaConversions._
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    85
    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    86
  }
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    87
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
    88
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    89
  /* extended syntax styles */
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    90
43440
a1db9a251a03 tuned signature;
wenzelm
parents: 43429
diff changeset
    91
  private val plain_range: Int = JEditToken.ID_COUNT
43488
39035276927c Symbol.is_ctrl: handle decoded version as well;
wenzelm
parents: 43487
diff changeset
    92
  private val full_range = 6 * plain_range + 1
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    93
  private def check_range(i: Int) { require(0 <= i && i < plain_range) }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    94
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    95
  def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    96
  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
43460
2852f309174a support for bold style within text buffer;
wenzelm
parents: 43458
diff changeset
    97
  def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    98
  def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    99
  val hidden: Byte = (6 * plain_range).toByte
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   100
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   101
  private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   102
    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   103
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   104
  private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   105
  {
43502
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   106
    font_style(style, font0 =>
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   107
      {
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   108
        import scala.collection.JavaConversions._
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   109
        val font1 = font0.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   110
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   111
        def shift(y: Float): Font =
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   112
          transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   113
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   114
        val m0 = font_metrics(font0)
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   115
        val m1 = font_metrics(font1)
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   116
        val a = m1.getAscent - m0.getAscent
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   117
        val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   118
        if (a > 0.0f) shift(a)
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   119
        else if (b > 0.0f) shift(- b)
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   120
        else font1
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   121
      })
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   122
  }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   123
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   124
  private def bold_style(style: SyntaxStyle): SyntaxStyle =
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   125
    font_style(style, _.deriveFont(Font.BOLD))
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   126
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: 50195
diff changeset
   127
  val hidden_color: Color = new Color(255, 255, 255, 0)
44356
f6a2e5ce2ce5 avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
wenzelm
parents: 44355
diff changeset
   128
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43553
diff changeset
   129
  class Style_Extender extends SyntaxUtilities.StyleExtender
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   130
  {
44355
9c38bdc6d755 default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
wenzelm
parents: 44238
diff changeset
   131
    val max_user_fonts = 2
9c38bdc6d755 default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
wenzelm
parents: 44238
diff changeset
   132
    if (Symbol.font_names.length > max_user_fonts)
9c38bdc6d755 default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
wenzelm
parents: 44238
diff changeset
   133
      error("Too many user symbol fonts (max " + max_user_fonts + " permitted): " +
9c38bdc6d755 default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
wenzelm
parents: 44238
diff changeset
   134
        Symbol.font_names.mkString(", "))
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   135
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   136
    override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   137
    {
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   138
      val new_styles = new Array[SyntaxStyle](full_range)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   139
      for (i <- 0 until plain_range) {
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   140
        val style = styles(i)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   141
        new_styles(i) = style
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   142
        new_styles(subscript(i.toByte)) = script_style(style, -1)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   143
        new_styles(superscript(i.toByte)) = script_style(style, 1)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   144
        new_styles(bold(i.toByte)) = bold_style(style)
44355
9c38bdc6d755 default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
wenzelm
parents: 44238
diff changeset
   145
        for (idx <- 0 until max_user_fonts)
9c38bdc6d755 default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
wenzelm
parents: 44238
diff changeset
   146
          new_styles(user_font(idx, i.toByte)) = style
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43675
diff changeset
   147
        for ((family, idx) <- Symbol.font_index)
43502
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   148
          new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   149
      }
43502
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   150
      new_styles(hidden) =
44356
f6a2e5ce2ce5 avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
wenzelm
parents: 44355
diff changeset
   151
        new SyntaxStyle(hidden_color, null,
43502
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   152
          { val font = styles(0).getFont
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   153
            transform_font(new Font(font.getFamily, 0, 1),
736183a22fa4 more precise font transformations: shift sub/superscript, adjust size for user fonts;
wenzelm
parents: 43491
diff changeset
   154
              AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   155
      new_styles
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   156
    }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   157
  }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   158
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43553
diff changeset
   159
  def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   160
  {
44238
36120feb70ed some convenience actions/shortcuts for control symbols;
wenzelm
parents: 43695
diff changeset
   161
    // FIXME Symbol.bsub_decoded etc.
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   162
    def control_style(sym: String): Option[Byte => Byte] =
53021
d0fa3f446b9d discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents: 50663
diff changeset
   163
      if (sym == Symbol.sub_decoded) Some(subscript(_))
d0fa3f446b9d discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents: 50663
diff changeset
   164
      else if (sym == Symbol.sup_decoded) Some(superscript(_))
44238
36120feb70ed some convenience actions/shortcuts for control symbols;
wenzelm
parents: 43695
diff changeset
   165
      else if (sym == Symbol.bold_decoded) Some(bold(_))
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   166
      else None
43455
4b4b93672f15 some unicode chars for special control symbols;
wenzelm
parents: 43452
diff changeset
   167
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   168
    var result = Map[Text.Offset, Byte => Byte]()
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   169
    def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   170
    {
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   171
      for (i <- start until stop) result += (i -> style)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   172
    }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   173
    var offset = 0
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   174
    var control = ""
43675
8252d51d70e2 simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents: 43661
diff changeset
   175
    for (sym <- Symbol.iterator(text)) {
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   176
      if (control_style(sym).isDefined) control = sym
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   177
      else if (control != "") {
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43675
diff changeset
   178
        if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   179
          mark(offset - control.length, offset, _ => hidden)
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   180
          mark(offset, offset + sym.length, control_style(control).get)
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   181
        }
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   182
        control = ""
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   183
      }
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43675
diff changeset
   184
      Symbol.lookup_font(sym) match {
43488
39035276927c Symbol.is_ctrl: handle decoded version as well;
wenzelm
parents: 43487
diff changeset
   185
        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   186
        case _ =>
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   187
      }
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   188
      offset += sym.length
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   189
    }
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   190
    result
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   191
  }
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   192
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   193
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   194
  /* token marker */
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   195
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   196
  private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   197
44358
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   198
  private class Line_Context(val context: Option[Scan.Context])
43429
095f90f8dca3 simplified Line_Context (again);
wenzelm
parents: 43416
diff changeset
   199
    extends TokenMarker.LineContext(isabelle_rules, null)
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   200
  {
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   201
    override def hashCode: Int = context.hashCode
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   202
    override def equals(that: Any): Boolean =
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   203
      that match {
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   204
        case other: Line_Context => context == other.context
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   205
        case _ => false
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   206
      }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   207
  }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   208
48713
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   209
  class Marker(ext_styles: Boolean, get_syntax: => Option[Outer_Syntax]) extends TokenMarker
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   210
  {
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   211
    override def markTokens(context: TokenMarker.LineContext,
46210
553ec602d337 paranoia null check -- prevent spurious crash of jedit token markup;
wenzelm
parents: 46178
diff changeset
   212
        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   213
    {
44358
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   214
      val line_ctxt =
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   215
        context match {
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   216
          case c: Line_Context => c.context
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   217
          case _ => Some(Scan.Finished)
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   218
        }
46210
553ec602d337 paranoia null check -- prevent spurious crash of jedit token markup;
wenzelm
parents: 46178
diff changeset
   219
      val line = if (raw_line == null) new Segment else raw_line
553ec602d337 paranoia null check -- prevent spurious crash of jedit token markup;
wenzelm
parents: 46178
diff changeset
   220
43553
df80747342cb proper tokens only if session is ready;
wenzelm
parents: 43511
diff changeset
   221
      val context1 =
44702
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   222
      {
48713
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   223
        val syntax = get_syntax
44702
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   224
        val (styled_tokens, context1) =
48713
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   225
          if (line_ctxt.isDefined && syntax.isDefined) {
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   226
            val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50196
diff changeset
   227
            val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax.get, tok), tok))
44702
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   228
            (styled_tokens, new Line_Context(Some(ctxt1)))
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   229
          }
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   230
          else {
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   231
            val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   232
            (List((JEditToken.NULL, token)), new Line_Context(None))
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   233
          }
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   234
48713
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   235
        val extended =
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   236
          if (ext_styles) extended_styles(line)
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   237
          else Map.empty[Text.Offset, Byte => Byte]
44702
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   238
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   239
        var offset = 0
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   240
        for ((style, token) <- styled_tokens) {
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   241
          val length = token.source.length
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   242
          val end_offset = offset + length
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   243
          if ((offset until end_offset) exists
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   244
              (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   245
            for (i <- offset until end_offset) {
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   246
              val style1 =
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   247
                extended.get(i) match {
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   248
                  case None => style
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   249
                  case Some(ext) => ext(style)
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   250
                }
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   251
              handler.handleToken(line, style1, i, 1, context1)
43553
df80747342cb proper tokens only if session is ready;
wenzelm
parents: 43511
diff changeset
   252
            }
df80747342cb proper tokens only if session is ready;
wenzelm
parents: 43511
diff changeset
   253
          }
44702
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   254
          else handler.handleToken(line, style, offset, length, context1)
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   255
          offset += length
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   256
        }
44702
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   257
        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   258
        context1
eb00752507c7 improved handling of extended styles and hard tabs when prover is inactive;
wenzelm
parents: 44701
diff changeset
   259
      }
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   260
      val context2 = context1.intern
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   261
      handler.setLineContext(context2)
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   262
      context2
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   263
    }
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   264
  }
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   265
43416
e730cdd97dcf more precise imitatation of original TokenMarker: no locking, interned context etc.;
wenzelm
parents: 43414
diff changeset
   266
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   267
  /* mode provider */
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   268
48713
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   269
  private val markers = Map(
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50199
diff changeset
   270
    "isabelle" -> new Token_Markup.Marker(true, PIDE.get_recent_syntax()),
48713
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   271
    "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   272
    "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
44358
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   273
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   274
  class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   275
  {
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   276
    for (mode <- orig_provider.getModes) addMode(mode)
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   277
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   278
    override def loadMode(mode: Mode, xmh: XModeHandler)
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   279
    {
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   280
      super.loadMode(mode, xmh)
48713
de26cf3191a3 more token markers, based on actual outer syntax;
wenzelm
parents: 47058
diff changeset
   281
      markers.get(mode.getName).map(mode.setTokenMarker(_))
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   282
    }
43452
5cf548485529 avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents: 43443
diff changeset
   283
  }
44358
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   284
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   285
  def refresh_buffer(buffer: JEditBuffer)
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   286
  {
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   287
    buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53249
diff changeset
   288
    val marker = markers.get(JEdit_Lib.buffer_mode(buffer))
53249
c95e9aee959c tuned -- help finding rare NPE on cold start;
wenzelm
parents: 53021
diff changeset
   289
    marker.map(buffer.setTokenMarker(_))
44358
2a2df4de1bbe more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents: 44356
diff changeset
   290
  }
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   291
}
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   292