src/Tools/jEdit/src/token_markup.scala
author wenzelm
Sat, 18 Jun 2011 23:34:34 +0200
changeset 43452 5cf548485529
parent 43443 5d9693c2337e
child 43455 4b4b93672f15
permissions -rw-r--r--
avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
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
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
    12
import org.gjt.sp.jedit.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
    13
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
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
    14
  ParserRuleSet, ModeProvider, 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
    15
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    16
import javax.swing.text.Segment
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    17
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    18
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    19
object Token_Markup
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    20
{
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    21
  /* extended syntax styles */
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    22
43440
a1db9a251a03 tuned signature;
wenzelm
parents: 43429
diff changeset
    23
  private val plain_range: Int = JEditToken.ID_COUNT
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    24
  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
    25
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    26
  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
    27
  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    28
  val hidden: Byte = (3 * plain_range).toByte
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    29
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    30
  // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    31
  // FIXME \\<^bold> \\<^loc>
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    32
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    33
  private val ctrl_styles: Map[String, Byte => Byte] =
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    34
    Map(
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    35
      "\\<^sub>" -> subscript,
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    36
      "\\<^sup>" -> superscript,
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    37
      "\\<^isub>" -> subscript,
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    38
      "\\<^isup>" -> superscript)
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    39
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    40
  private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    41
    : Map[Text.Offset, Byte => Byte] =
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    42
  {
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    43
    if (Isabelle.extended_styles) {
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    44
      var result = Map[Text.Offset, Byte => Byte]()
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    45
      def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    46
      {
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    47
        for (i <- start until stop) result += (i -> style)
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    48
      }
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    49
      var offset = 0
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    50
      var ctrl = ""
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    51
      for (sym <- Symbol.iterator(text).map(_.toString)) {
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    52
        if (ctrl_styles.isDefinedAt(sym)) ctrl = sym
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    53
        else if (ctrl != "") {
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    54
          if (symbols.is_controllable(sym)) {
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    55
            mark(offset - ctrl.length, offset, _ => hidden)
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    56
            mark(offset, offset + sym.length, ctrl_styles(ctrl))
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    57
          }
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    58
          ctrl = ""
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    59
        }
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    60
        offset += sym.length
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    61
      }
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    62
      result
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    63
    }
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    64
    else Map.empty
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    65
  }
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    66
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    67
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    68
  /* token marker */
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    69
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    70
  private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    71
43429
095f90f8dca3 simplified Line_Context (again);
wenzelm
parents: 43416
diff changeset
    72
  private class Line_Context(val context: Scan.Context)
095f90f8dca3 simplified Line_Context (again);
wenzelm
parents: 43416
diff changeset
    73
    extends TokenMarker.LineContext(isabelle_rules, null)
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    74
  {
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    75
    override def hashCode: Int = context.hashCode
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    76
    override def equals(that: Any): Boolean =
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    77
      that match {
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    78
        case other: Line_Context => context == other.context
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    79
        case _ => false
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    80
      }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    81
  }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    82
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
    83
  class Marker extends TokenMarker
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
    84
  {
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
    85
    override def markTokens(context: TokenMarker.LineContext,
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
    86
        handler: TokenHandler, line: Segment): TokenMarker.LineContext =
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
    87
    {
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
    88
      val symbols = Isabelle.system.symbols
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
    89
      val syntax = Isabelle.session.current_syntax()
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    90
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
    91
      val ctxt =
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
    92
        context match {
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
    93
          case c: Line_Context => c.context
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
    94
          case _ => Scan.Finished
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
    95
        }
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
    96
      val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
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
    97
      val context1 = new Line_Context(ctxt1)
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
    98
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
    99
      val extended = extended_styles(symbols, line)
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   100
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
   101
      var offset = 0
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
   102
      for (token <- tokens) {
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
   103
        val style = Isabelle_Markup.token_markup(syntax, token)
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
   104
        val length = token.source.length
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
   105
        val end_offset = offset + length
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
   106
        if ((offset until end_offset) exists extended.isDefinedAt) {
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
   107
          for (i <- offset until end_offset) {
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
   108
            val style1 =
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
   109
              extended.get(i) match {
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
   110
                case None => style
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
   111
                case Some(ext) => ext(style)
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
   112
              }
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
   113
            handler.handleToken(line, style1, i, 1, context1)
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   114
          }
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   115
        }
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
   116
        else handler.handleToken(line, style, offset, length, context1)
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
   117
        offset += length
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
   118
      }
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
   119
      handler.handleToken(line, JEditToken.END, line.count, 0, context1)
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
   120
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
   121
      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
   122
      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
   123
      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
   124
    }
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
   125
  }
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
   126
43416
e730cdd97dcf more precise imitatation of original TokenMarker: no locking, interned context etc.;
wenzelm
parents: 43414
diff changeset
   127
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
   128
  /* 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
   129
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
   130
  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
   131
  {
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
   132
    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
   133
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
   134
    val isabelle_token_marker = new Token_Markup.Marker
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
   135
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
   136
    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
   137
    {
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
   138
      super.loadMode(mode, xmh)
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
   139
      if (mode.getName == "isabelle")
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
   140
        mode.setTokenMarker(isabelle_token_marker)
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   141
    }
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
   142
  }
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   143
}
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   144