src/Tools/jEdit/src/token_markup.scala
author wenzelm
Tue, 21 Jun 2011 15:43:27 +0200
changeset 43491 7b7baa283434
parent 43489 132f99cc0a43
child 43502 736183a22fa4
permissions -rw-r--r--
hidden font: full height makes cursor more visible;
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}
43491
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    13
import java.awt.font.{TextAttribute, TransformAttribute}
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
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
    17
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
    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}
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
    20
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    21
import javax.swing.text.Segment
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    22
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    23
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    24
object Token_Markup
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    25
{
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    26
  /* extended syntax styles */
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    27
43440
a1db9a251a03 tuned signature;
wenzelm
parents: 43429
diff changeset
    28
  private val plain_range: Int = JEditToken.ID_COUNT
43488
39035276927c Symbol.is_ctrl: handle decoded version as well;
wenzelm
parents: 43487
diff changeset
    29
  private val full_range = 6 * plain_range + 1
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    30
  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
    31
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    32
  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
    33
  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
    34
  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
    35
  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
    36
  val hidden: Byte = (6 * plain_range).toByte
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    37
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    38
  private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    39
    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
    40
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    41
  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
    42
  {
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    43
    import scala.collection.JavaConversions._
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    44
    font_style(style, font =>
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    45
      style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i))))
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    46
  }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    47
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    48
  private def bold_style(style: SyntaxStyle): SyntaxStyle =
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    49
    font_style(style, _.deriveFont(Font.BOLD))
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    50
43491
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    51
  private def hidden_font(font: Font): Font =
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    52
  {
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    53
    import scala.collection.JavaConversions._
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    54
    val base_font = new Font(font.getFamily, 0, 1)
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    55
    val transform =
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    56
      new TransformAttribute(AffineTransform.getScaleInstance(1.0, font.getSize.toDouble))
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    57
    base_font.deriveFont(Map(TextAttribute.TRANSFORM -> transform))
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    58
  }
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    59
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    60
  class Style_Extender(symbols: Symbol.Interpretation) extends SyntaxUtilities.StyleExtender
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    61
  {
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    62
    if (symbols.font_names.length > 2)
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    63
      error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    64
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    65
    override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    66
    {
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    67
      val new_styles = new Array[SyntaxStyle](full_range)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    68
      for (i <- 0 until plain_range) {
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    69
        val style = styles(i)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    70
        new_styles(i) = style
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    71
        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
    72
        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
    73
        new_styles(bold(i.toByte)) = bold_style(style)
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    74
        for ((family, idx) <- symbols.font_index) {
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    75
          // FIXME adjust size
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    76
          new_styles(user_font(idx, i.toByte)) =
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    77
            font_style(style, font => new Font(family, font.getStyle, font.getSize))
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    78
        }
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    79
      }
43491
7b7baa283434 hidden font: full height makes cursor more visible;
wenzelm
parents: 43489
diff changeset
    80
      new_styles(hidden) = new SyntaxStyle(Color.white, null, hidden_font(styles(0).getFont))
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    81
      new_styles
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    82
    }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    83
  }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    84
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
    85
  def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    86
    : Map[Text.Offset, Byte => Byte] =
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
    87
  {
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    88
    // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    89
    def ctrl_style(sym: String): Option[Byte => Byte] =
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    90
      if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    91
      else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    92
      else if (symbols.is_bold_decoded(sym)) Some(bold(_))
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    93
      else None
43455
4b4b93672f15 some unicode chars for special control symbols;
wenzelm
parents: 43452
diff changeset
    94
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    95
    var result = Map[Text.Offset, Byte => Byte]()
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    96
    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
    97
    {
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    98
      for (i <- start until stop) result += (i -> style)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
    99
    }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   100
    var offset = 0
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   101
    var ctrl = ""
43489
132f99cc0a43 tuned iteration over short symbols;
wenzelm
parents: 43488
diff changeset
   102
    for (sym <- Symbol.iterator_string(text)) {
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   103
      if (ctrl_style(sym).isDefined) ctrl = sym
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   104
      else if (ctrl != "") {
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   105
        if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   106
          mark(offset - ctrl.length, offset, _ => hidden)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   107
          mark(offset, offset + sym.length, ctrl_style(ctrl).get)
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   108
        }
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   109
        ctrl = ""
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   110
      }
43488
39035276927c Symbol.is_ctrl: handle decoded version as well;
wenzelm
parents: 43487
diff changeset
   111
      symbols.lookup_font(sym) match {
39035276927c Symbol.is_ctrl: handle decoded version as well;
wenzelm
parents: 43487
diff changeset
   112
        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
43487
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   113
        case _ =>
98cd7e83fc5b some support for user symbol fonts;
wenzelm
parents: 43482
diff changeset
   114
      }
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   115
      offset += sym.length
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   116
    }
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43464
diff changeset
   117
    result
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   118
  }
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   119
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   120
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   121
  /* token marker */
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   122
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   123
  private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   124
43429
095f90f8dca3 simplified Line_Context (again);
wenzelm
parents: 43416
diff changeset
   125
  private class Line_Context(val context: Scan.Context)
095f90f8dca3 simplified Line_Context (again);
wenzelm
parents: 43416
diff changeset
   126
    extends TokenMarker.LineContext(isabelle_rules, null)
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   127
  {
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   128
    override def hashCode: Int = context.hashCode
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   129
    override def equals(that: Any): Boolean =
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   130
      that match {
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   131
        case other: Line_Context => context == other.context
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   132
        case _ => false
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   133
      }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   134
  }
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   135
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
   136
  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
   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
    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
   139
        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
   140
    {
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
   141
      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
   142
      val syntax = Isabelle.session.current_syntax()
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   143
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
   144
      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
   145
        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
   146
          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
   147
          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
   148
        }
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
   149
      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
   150
      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
   151
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
   152
      val extended = extended_styles(symbols, line)
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   153
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
   154
      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
   155
      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
   156
        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
   157
        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
   158
        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
   159
        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
   160
          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
   161
            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
   162
              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
   163
                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
   164
                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
   165
              }
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
   166
            handler.handleToken(line, style1, i, 1, context1)
43443
5d9693c2337e basic support for extended syntax styles: sub/superscript;
wenzelm
parents: 43440
diff changeset
   167
          }
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   168
        }
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
   169
        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
   170
        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
   171
      }
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
   172
      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
   173
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
   174
      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
   175
      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
   176
      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
   177
    }
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
   178
  }
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
   179
43416
e730cdd97dcf more precise imitatation of original TokenMarker: no locking, interned context etc.;
wenzelm
parents: 43414
diff changeset
   180
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
   181
  /* 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
   182
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
   183
  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
   184
  {
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
   185
    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
   186
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
   187
    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
   188
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
   189
    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
   190
    {
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
   191
      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
   192
      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
   193
        mode.setTokenMarker(isabelle_token_marker)
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   194
    }
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
   195
  }
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   196
}
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents:
diff changeset
   197