src/Tools/jEdit/src/token_markup.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 65258 a0701669d159
permissions -rw-r--r--
tuned signature;
wenzelm@43414
     1
/*  Title:      Tools/jEdit/src/token_markup.scala
wenzelm@43414
     2
    Author:     Makarius
wenzelm@43414
     3
wenzelm@43414
     4
Outer syntax token markup.
wenzelm@43414
     5
*/
wenzelm@43414
     6
wenzelm@43414
     7
package isabelle.jedit
wenzelm@43414
     8
wenzelm@43414
     9
wenzelm@43414
    10
import isabelle._
wenzelm@43414
    11
wenzelm@43482
    12
import java.awt.{Font, Color}
wenzelm@53785
    13
import java.awt.font.TextAttribute
wenzelm@43491
    14
import java.awt.geom.AffineTransform
wenzelm@63421
    15
import javax.swing.text.Segment
wenzelm@63421
    16
wenzelm@63421
    17
import scala.collection.convert.WrapAsJava
wenzelm@43482
    18
wenzelm@43482
    19
import org.gjt.sp.util.SyntaxUtilities
wenzelm@59076
    20
import org.gjt.sp.jedit.{jEdit, Mode, Buffer}
wenzelm@58701
    21
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
wenzelm@58701
    22
  ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
wenzelm@63422
    23
import org.gjt.sp.jedit.indent.IndentRule
wenzelm@50183
    24
import org.gjt.sp.jedit.textarea.{TextArea, Selection}
wenzelm@61192
    25
import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@43452
    26
wenzelm@43414
    27
wenzelm@43414
    28
object Token_Markup
wenzelm@43414
    29
{
wenzelm@50183
    30
  /* editing support for control symbols */
wenzelm@50183
    31
wenzelm@50187
    32
  def edit_control_style(text_area: TextArea, control: String)
wenzelm@50183
    33
  {
wenzelm@57612
    34
    GUI_Thread.assert {}
wenzelm@50183
    35
wenzelm@50183
    36
    val buffer = text_area.getBuffer
wenzelm@50183
    37
wenzelm@62104
    38
    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
wenzelm@62104
    39
wenzelm@62104
    40
    def update_style(text: String): String =
wenzelm@62104
    41
    {
wenzelm@62104
    42
      val result = new StringBuilder
wenzelm@62104
    43
      for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
wenzelm@62104
    44
        if (Symbol.is_controllable(sym)) result ++= control_decoded
wenzelm@62104
    45
        result ++= sym
wenzelm@62104
    46
      }
wenzelm@62104
    47
      result.toString
wenzelm@62104
    48
    }
wenzelm@62104
    49
wenzelm@50663
    50
    text_area.getSelection.foreach(sel => {
wenzelm@50663
    51
      val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
wenzelm@50663
    52
      JEdit_Lib.try_get_text(buffer, before) match {
wenzelm@62104
    53
        case Some(s) if HTML.control.isDefinedAt(s) =>
wenzelm@50663
    54
          text_area.extendSelection(before.start, before.stop)
wenzelm@50663
    55
        case _ =>
wenzelm@50663
    56
      }
wenzelm@50663
    57
    })
wenzelm@50663
    58
wenzelm@50183
    59
    text_area.getSelection.toList match {
wenzelm@50210
    60
      case Nil =>
wenzelm@62104
    61
        text_area.setSelectedText(control_decoded)
wenzelm@50183
    62
      case sels =>
wenzelm@50195
    63
        JEdit_Lib.buffer_edit(buffer) {
wenzelm@50183
    64
          sels.foreach(sel =>
wenzelm@62104
    65
            text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
wenzelm@50183
    66
        }
wenzelm@50183
    67
    }
wenzelm@50183
    68
  }
wenzelm@50183
    69
wenzelm@50183
    70
wenzelm@43443
    71
  /* extended syntax styles */
wenzelm@43414
    72
wenzelm@43440
    73
  private val plain_range: Int = JEditToken.ID_COUNT
wenzelm@43488
    74
  private val full_range = 6 * plain_range + 1
wenzelm@43414
    75
  private def check_range(i: Int) { require(0 <= i && i < plain_range) }
wenzelm@43414
    76
wenzelm@43414
    77
  def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
wenzelm@43414
    78
  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
wenzelm@43460
    79
  def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
wenzelm@43487
    80
  def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
wenzelm@43487
    81
  val hidden: Byte = (6 * plain_range).toByte
wenzelm@43487
    82
wenzelm@43487
    83
  private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
wenzelm@43487
    84
    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
wenzelm@43414
    85
wenzelm@43482
    86
  private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
wenzelm@43482
    87
  {
wenzelm@43502
    88
    font_style(style, font0 =>
wenzelm@43502
    89
      {
wenzelm@43502
    90
        import scala.collection.JavaConversions._
wenzelm@43502
    91
        val font1 = font0.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
wenzelm@43502
    92
wenzelm@43502
    93
        def shift(y: Float): Font =
wenzelm@53785
    94
          GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
wenzelm@43502
    95
wenzelm@59230
    96
        val m0 = GUI.line_metrics(font0)
wenzelm@59230
    97
        val m1 = GUI.line_metrics(font1)
wenzelm@43502
    98
        val a = m1.getAscent - m0.getAscent
wenzelm@43502
    99
        val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
wenzelm@43502
   100
        if (a > 0.0f) shift(a)
wenzelm@43502
   101
        else if (b > 0.0f) shift(- b)
wenzelm@43502
   102
        else font1
wenzelm@43502
   103
      })
wenzelm@43482
   104
  }
wenzelm@43482
   105
wenzelm@43482
   106
  private def bold_style(style: SyntaxStyle): SyntaxStyle =
wenzelm@57126
   107
    font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD))
wenzelm@43482
   108
wenzelm@50196
   109
  val hidden_color: Color = new Color(255, 255, 255, 0)
wenzelm@44356
   110
wenzelm@43661
   111
  class Style_Extender extends SyntaxUtilities.StyleExtender
wenzelm@43482
   112
  {
wenzelm@44355
   113
    val max_user_fonts = 2
wenzelm@44355
   114
    if (Symbol.font_names.length > max_user_fonts)
wenzelm@60238
   115
      error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
wenzelm@44355
   116
        Symbol.font_names.mkString(", "))
wenzelm@43487
   117
wenzelm@43482
   118
    override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
wenzelm@43482
   119
    {
wenzelm@43482
   120
      val new_styles = new Array[SyntaxStyle](full_range)
wenzelm@43482
   121
      for (i <- 0 until plain_range) {
wenzelm@43482
   122
        val style = styles(i)
wenzelm@43482
   123
        new_styles(i) = style
wenzelm@43482
   124
        new_styles(subscript(i.toByte)) = script_style(style, -1)
wenzelm@43482
   125
        new_styles(superscript(i.toByte)) = script_style(style, 1)
wenzelm@43482
   126
        new_styles(bold(i.toByte)) = bold_style(style)
wenzelm@44355
   127
        for (idx <- 0 until max_user_fonts)
wenzelm@44355
   128
          new_styles(user_font(idx, i.toByte)) = style
wenzelm@43695
   129
        for ((family, idx) <- Symbol.font_index)
wenzelm@59286
   130
          new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
wenzelm@43482
   131
      }
wenzelm@43502
   132
      new_styles(hidden) =
wenzelm@44356
   133
        new SyntaxStyle(hidden_color, null,
wenzelm@43502
   134
          { val font = styles(0).getFont
wenzelm@53785
   135
            GUI.transform_font(new Font(font.getFamily, 0, 1),
wenzelm@43502
   136
              AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
wenzelm@43482
   137
      new_styles
wenzelm@43482
   138
    }
wenzelm@43482
   139
  }
wenzelm@43482
   140
wenzelm@43661
   141
  def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
wenzelm@43443
   142
  {
wenzelm@44238
   143
    // FIXME Symbol.bsub_decoded etc.
wenzelm@50187
   144
    def control_style(sym: String): Option[Byte => Byte] =
wenzelm@53021
   145
      if (sym == Symbol.sub_decoded) Some(subscript(_))
wenzelm@53021
   146
      else if (sym == Symbol.sup_decoded) Some(superscript(_))
wenzelm@44238
   147
      else if (sym == Symbol.bold_decoded) Some(bold(_))
wenzelm@43482
   148
      else None
wenzelm@43455
   149
wenzelm@43482
   150
    var result = Map[Text.Offset, Byte => Byte]()
wenzelm@43482
   151
    def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
wenzelm@43482
   152
    {
wenzelm@43482
   153
      for (i <- start until stop) result += (i -> style)
wenzelm@43482
   154
    }
wenzelm@43482
   155
    var offset = 0
wenzelm@50187
   156
    var control = ""
wenzelm@43675
   157
    for (sym <- Symbol.iterator(text)) {
wenzelm@50187
   158
      if (control_style(sym).isDefined) control = sym
wenzelm@50187
   159
      else if (control != "") {
wenzelm@43695
   160
        if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
wenzelm@50187
   161
          mark(offset - control.length, offset, _ => hidden)
wenzelm@50187
   162
          mark(offset, offset + sym.length, control_style(control).get)
wenzelm@43482
   163
        }
wenzelm@50187
   164
        control = ""
wenzelm@43443
   165
      }
wenzelm@43695
   166
      Symbol.lookup_font(sym) match {
wenzelm@43488
   167
        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
wenzelm@43487
   168
        case _ =>
wenzelm@43487
   169
      }
wenzelm@43482
   170
      offset += sym.length
wenzelm@43443
   171
    }
wenzelm@43482
   172
    result
wenzelm@43443
   173
  }
wenzelm@43443
   174
wenzelm@43414
   175
wenzelm@58529
   176
  /* line context */
wenzelm@43414
   177
wenzelm@58748
   178
  object Line_Context
wenzelm@58748
   179
  {
wenzelm@63444
   180
    def init(mode: String): Line_Context =
wenzelm@63603
   181
      new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
wenzelm@63454
   182
wenzelm@63454
   183
    def prev(buffer: JEditBuffer, line: Int): Line_Context =
wenzelm@63454
   184
      if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
wenzelm@63454
   185
      else next(buffer, line - 1)
wenzelm@63454
   186
wenzelm@63454
   187
    def next(buffer: JEditBuffer, line: Int): Line_Context =
wenzelm@63454
   188
    {
wenzelm@63454
   189
      val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
wenzelm@63454
   190
      def context =
wenzelm@63454
   191
        line_mgr.getLineContext(line) match {
wenzelm@63454
   192
          case c: Line_Context => Some(c)
wenzelm@63454
   193
          case _ => None
wenzelm@63454
   194
        }
wenzelm@63454
   195
      context getOrElse {
wenzelm@63454
   196
        buffer.markTokens(line, DummyTokenHandler.INSTANCE)
wenzelm@63454
   197
        context getOrElse init(JEdit_Lib.buffer_mode(buffer))
wenzelm@63454
   198
      }
wenzelm@63454
   199
    }
wenzelm@58748
   200
  }
wenzelm@58748
   201
wenzelm@58699
   202
  class Line_Context(
wenzelm@63444
   203
      val mode: String,
wenzelm@58699
   204
      val context: Option[Scan.Line_Context],
wenzelm@63603
   205
      val structure: Line_Structure)
wenzelm@63444
   206
    extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
wenzelm@43414
   207
  {
wenzelm@63454
   208
    def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
wenzelm@63454
   209
wenzelm@63444
   210
    override def hashCode: Int = (mode, context, structure).hashCode
wenzelm@43414
   211
    override def equals(that: Any): Boolean =
wenzelm@43414
   212
      that match {
wenzelm@63444
   213
        case other: Line_Context =>
wenzelm@63444
   214
          mode == other.mode && context == other.context && structure == other.structure
wenzelm@43414
   215
        case _ => false
wenzelm@43414
   216
      }
wenzelm@43414
   217
  }
wenzelm@43414
   218
wenzelm@58749
   219
wenzelm@59924
   220
  /* tokens from line (inclusive) */
wenzelm@58749
   221
wenzelm@58802
   222
  private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
wenzelm@58802
   223
    : Option[List[Token]] =
wenzelm@58748
   224
  {
wenzelm@63454
   225
    val line_context = Line_Context.prev(buffer, line)
wenzelm@58748
   226
    for {
wenzelm@58748
   227
      ctxt <- line_context.context
wenzelm@58748
   228
      text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line))
wenzelm@59083
   229
    } yield Token.explode_line(syntax.keywords, text, ctxt)._1
wenzelm@58748
   230
  }
wenzelm@58699
   231
wenzelm@58749
   232
  def line_token_iterator(
wenzelm@58750
   233
      syntax: Outer_Syntax,
wenzelm@58750
   234
      buffer: JEditBuffer,
wenzelm@58750
   235
      start_line: Int,
wenzelm@58750
   236
      end_line: Int): Iterator[Text.Info[Token]] =
wenzelm@58749
   237
    for {
wenzelm@58750
   238
      line <- Range(start_line max 0, end_line min buffer.getLineCount).iterator
wenzelm@58749
   239
      tokens <- try_line_tokens(syntax, buffer, line).iterator
wenzelm@58749
   240
      starts =
wenzelm@58749
   241
        tokens.iterator.scanLeft(buffer.getLineStartOffset(line))(
wenzelm@58749
   242
          (i, tok) => i + tok.source.length)
wenzelm@58750
   243
      (i, tok) <- starts zip tokens.iterator
wenzelm@58750
   244
    } yield Text.Info(Text.Range(i, i + tok.source.length), tok)
wenzelm@58749
   245
wenzelm@58749
   246
  def line_token_reverse_iterator(
wenzelm@58750
   247
      syntax: Outer_Syntax,
wenzelm@58750
   248
      buffer: JEditBuffer,
wenzelm@58750
   249
      start_line: Int,
wenzelm@58750
   250
      end_line: Int): Iterator[Text.Info[Token]] =
wenzelm@58749
   251
    for {
wenzelm@58750
   252
      line <- Range(start_line min (buffer.getLineCount - 1), end_line max -1, -1).iterator
wenzelm@58749
   253
      tokens <- try_line_tokens(syntax, buffer, line).iterator
wenzelm@58749
   254
      stops =
wenzelm@58749
   255
        tokens.reverseIterator.scanLeft(buffer.getLineEndOffset(line) min buffer.getLength)(
wenzelm@58749
   256
          (i, tok) => i - tok.source.length)
wenzelm@58750
   257
      (i, tok) <- stops zip tokens.reverseIterator
wenzelm@58750
   258
    } yield Text.Info(Text.Range(i - tok.source.length, i), tok)
wenzelm@58749
   259
wenzelm@58694
   260
wenzelm@59924
   261
  /* tokens from offset (inclusive) */
wenzelm@59924
   262
wenzelm@59924
   263
  def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
wenzelm@59924
   264
      Iterator[Text.Info[Token]] =
wenzelm@59924
   265
    if (JEdit_Lib.buffer_range(buffer).contains(offset))
wenzelm@59924
   266
      line_token_iterator(syntax, buffer, buffer.getLineOfOffset(offset), buffer.getLineCount).
wenzelm@59924
   267
        dropWhile(info => !info.range.contains(offset))
wenzelm@59924
   268
    else Iterator.empty
wenzelm@59924
   269
wenzelm@59924
   270
  def token_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
wenzelm@59924
   271
      Iterator[Text.Info[Token]] =
wenzelm@59924
   272
    if (JEdit_Lib.buffer_range(buffer).contains(offset))
wenzelm@59924
   273
      line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1).
wenzelm@59924
   274
        dropWhile(info => !info.range.contains(offset))
wenzelm@59924
   275
    else Iterator.empty
wenzelm@59924
   276
wenzelm@59924
   277
wenzelm@58809
   278
  /* command spans */
wenzelm@58802
   279
wenzelm@58802
   280
  def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
wenzelm@58802
   281
    : Option[Text.Info[Command_Span.Span]] =
wenzelm@58802
   282
  {
wenzelm@63441
   283
    val keywords = syntax.keywords
wenzelm@63441
   284
wenzelm@59924
   285
    def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
wenzelm@59924
   286
      token_reverse_iterator(syntax, buffer, i).
wenzelm@63441
   287
        find(info => keywords.is_before_command(info.info) || info.info.is_command)
wenzelm@59924
   288
wenzelm@59924
   289
    def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
wenzelm@59924
   290
      token_iterator(syntax, buffer, i).
wenzelm@63441
   291
        find(info => keywords.is_before_command(info.info) || info.info.is_command)
wenzelm@59924
   292
wenzelm@58802
   293
    if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
wenzelm@59924
   294
      val start_info =
wenzelm@59924
   295
      {
wenzelm@59924
   296
        val info1 = maybe_command_start(offset)
wenzelm@59924
   297
        info1 match {
wenzelm@59924
   298
          case Some(Text.Info(range1, tok1)) if tok1.is_command =>
wenzelm@59924
   299
            val info2 = maybe_command_start(range1.start - 1)
wenzelm@59924
   300
            info2 match {
wenzelm@63441
   301
              case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2
wenzelm@59924
   302
              case _ => info1
wenzelm@59924
   303
            }
wenzelm@59924
   304
          case _ => info1
wenzelm@59924
   305
        }
wenzelm@59924
   306
      }
wenzelm@63441
   307
      val (start_before_command, start, start_next) =
wenzelm@59924
   308
        start_info match {
wenzelm@63441
   309
          case Some(Text.Info(range, tok)) =>
wenzelm@63441
   310
            (keywords.is_before_command(tok), range.start, range.stop)
wenzelm@59924
   311
          case None => (false, 0, 0)
wenzelm@59924
   312
        }
wenzelm@59924
   313
wenzelm@59924
   314
      val stop_info =
wenzelm@59924
   315
      {
wenzelm@59924
   316
        val info1 = maybe_command_stop(start_next)
wenzelm@59924
   317
        info1 match {
wenzelm@63441
   318
          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command =>
wenzelm@59924
   319
            maybe_command_stop(range1.stop)
wenzelm@59924
   320
          case _ => info1
wenzelm@59924
   321
        }
wenzelm@59924
   322
      }
wenzelm@58802
   323
      val stop =
wenzelm@59924
   324
        stop_info match {
wenzelm@59924
   325
          case Some(Text.Info(range, _)) => range.start
wenzelm@59924
   326
          case None => buffer.getLength
wenzelm@59924
   327
        }
wenzelm@58802
   328
wenzelm@58802
   329
      val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("")
wenzelm@58802
   330
      val spans = syntax.parse_spans(text)
wenzelm@58802
   331
wenzelm@58802
   332
      (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator).
wenzelm@58802
   333
        map({ case (i, span) => Text.Info(Text.Range(i, i + span.length), span) }).
wenzelm@58802
   334
        find(_.range.contains(offset))
wenzelm@58802
   335
    }
wenzelm@58802
   336
    else None
wenzelm@58802
   337
  }
wenzelm@58802
   338
wenzelm@58809
   339
  private def _command_span_iterator(
wenzelm@58809
   340
      syntax: Outer_Syntax,
wenzelm@58809
   341
      buffer: JEditBuffer,
wenzelm@58809
   342
      offset: Text.Offset,
wenzelm@58809
   343
      next_offset: Text.Range => Text.Offset): Iterator[Text.Info[Command_Span.Span]] =
wenzelm@58809
   344
    new Iterator[Text.Info[Command_Span.Span]]
wenzelm@58809
   345
    {
wenzelm@58809
   346
      private var next_span = command_span(syntax, buffer, offset)
wenzelm@58809
   347
      def hasNext: Boolean = next_span.isDefined
wenzelm@58809
   348
      def next: Text.Info[Command_Span.Span] =
wenzelm@58809
   349
      {
wenzelm@58809
   350
        val span = next_span.getOrElse(Iterator.empty.next)
wenzelm@58809
   351
        next_span = command_span(syntax, buffer, next_offset(span.range))
wenzelm@58809
   352
        span
wenzelm@58809
   353
      }
wenzelm@58809
   354
    }
wenzelm@58809
   355
wenzelm@58809
   356
  def command_span_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
wenzelm@58809
   357
      : Iterator[Text.Info[Command_Span.Span]] =
wenzelm@58809
   358
    _command_span_iterator(syntax, buffer, offset max 0, range => range.stop)
wenzelm@58809
   359
wenzelm@58809
   360
  def command_span_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
wenzelm@58809
   361
      : Iterator[Text.Info[Command_Span.Span]] =
wenzelm@58809
   362
    _command_span_iterator(syntax, buffer,
wenzelm@58809
   363
      (offset min buffer.getLength) - 1, range => range.start - 1)
wenzelm@58809
   364
wenzelm@58802
   365
wenzelm@58694
   366
  /* token marker */
wenzelm@58683
   367
wenzelm@59077
   368
  class Marker(
wenzelm@59077
   369
    protected val mode: String,
wenzelm@59077
   370
    protected val opt_buffer: Option[Buffer]) extends TokenMarker
wenzelm@43452
   371
  {
wenzelm@59077
   372
    override def hashCode: Int = (mode, opt_buffer).hashCode
wenzelm@59077
   373
    override def equals(that: Any): Boolean =
wenzelm@59077
   374
      that match {
wenzelm@59077
   375
        case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer
wenzelm@59077
   376
        case _ => false
wenzelm@59077
   377
      }
wenzelm@59077
   378
wenzelm@59076
   379
    override def toString: String =
wenzelm@59076
   380
      opt_buffer match {
wenzelm@59076
   381
        case None => "Marker(" + mode + ")"
wenzelm@59076
   382
        case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")"
wenzelm@59076
   383
      }
wenzelm@59076
   384
wenzelm@43452
   385
    override def markTokens(context: TokenMarker.LineContext,
wenzelm@46210
   386
        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
wenzelm@43452
   387
    {
wenzelm@46210
   388
      val line = if (raw_line == null) new Segment else raw_line
wenzelm@63444
   389
      val line_context =
wenzelm@63444
   390
        context match { case c: Line_Context => c case _ => Line_Context.init(mode) }
wenzelm@58748
   391
      val structure = line_context.structure
wenzelm@46210
   392
wenzelm@43553
   393
      val context1 =
wenzelm@44702
   394
      {
wenzelm@59076
   395
        val opt_syntax =
wenzelm@59076
   396
          opt_buffer match {
wenzelm@59076
   397
            case Some(buffer) => Isabelle.buffer_syntax(buffer)
wenzelm@59076
   398
            case None => Isabelle.mode_syntax(mode)
wenzelm@59076
   399
          }
wenzelm@44702
   400
        val (styled_tokens, context1) =
wenzelm@59076
   401
          (line_context.context, opt_syntax) match {
wenzelm@58694
   402
            case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
wenzelm@58694
   403
              val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
wenzelm@64621
   404
              val styled_tokens =
wenzelm@64621
   405
                tokens.map(tok => (JEdit_Rendering.ml_token_markup(tok), tok.source))
wenzelm@63444
   406
              (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure))
wenzelm@58694
   407
wenzelm@58694
   408
            case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
wenzelm@59083
   409
              val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
wenzelm@63603
   410
              val structure1 = structure.update(syntax.keywords, tokens)
wenzelm@58694
   411
              val styled_tokens =
wenzelm@64621
   412
                tokens.map(tok => (JEdit_Rendering.token_markup(syntax, tok), tok.source))
wenzelm@63444
   413
              (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))
wenzelm@58694
   414
wenzelm@58694
   415
            case _ =>
wenzelm@58694
   416
              val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
wenzelm@63444
   417
              (List(styled_token), new Line_Context(line_context.mode, None, structure))
wenzelm@44702
   418
          }
wenzelm@44702
   419
wenzelm@53278
   420
        val extended = extended_styles(line)
wenzelm@44702
   421
wenzelm@44702
   422
        var offset = 0
wenzelm@44702
   423
        for ((style, token) <- styled_tokens) {
wenzelm@55500
   424
          val length = token.length
wenzelm@44702
   425
          val end_offset = offset + length
wenzelm@44702
   426
          if ((offset until end_offset) exists
wenzelm@44702
   427
              (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
wenzelm@44702
   428
            for (i <- offset until end_offset) {
wenzelm@44702
   429
              val style1 =
wenzelm@44702
   430
                extended.get(i) match {
wenzelm@44702
   431
                  case None => style
wenzelm@44702
   432
                  case Some(ext) => ext(style)
wenzelm@44702
   433
                }
wenzelm@44702
   434
              handler.handleToken(line, style1, i, 1, context1)
wenzelm@43553
   435
            }
wenzelm@43553
   436
          }
wenzelm@44702
   437
          else handler.handleToken(line, style, offset, length, context1)
wenzelm@44702
   438
          offset += length
wenzelm@43452
   439
        }
wenzelm@44702
   440
        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
wenzelm@44702
   441
        context1
wenzelm@44702
   442
      }
wenzelm@58694
   443
wenzelm@43452
   444
      val context2 = context1.intern
wenzelm@43452
   445
      handler.setLineContext(context2)
wenzelm@43452
   446
      context2
wenzelm@43452
   447
    }
wenzelm@43452
   448
  }
wenzelm@43452
   449
wenzelm@43416
   450
wenzelm@43452
   451
  /* mode provider */
wenzelm@43452
   452
wenzelm@43452
   453
  class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
wenzelm@43452
   454
  {
wenzelm@43452
   455
    for (mode <- orig_provider.getModes) addMode(mode)
wenzelm@43452
   456
wenzelm@43452
   457
    override def loadMode(mode: Mode, xmh: XModeHandler)
wenzelm@43452
   458
    {
wenzelm@43452
   459
      super.loadMode(mode, xmh)
wenzelm@59076
   460
      Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
wenzelm@63422
   461
      Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
wenzelm@63421
   462
        Untyped.set[java.util.List[IndentRule]](
wenzelm@63421
   463
          mode, "indentRules", WrapAsJava.seqAsJavaList(List(indent_rule))))
wenzelm@53277
   464
    }
wenzelm@44358
   465
  }
wenzelm@43414
   466
}