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