|
/* Title: Tools/jEdit/src-base/syntax_style.scala
Author: Makarius
Extended syntax styles: dummy version.
*/
package isabelle.jedit_base
import isabelle._
import org.gjt.sp.util.SyntaxUtilities
import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
import org.gjt.sp.jedit.jEdit
object Syntax_Style
{
private val plain_range: Int = JEditToken.ID_COUNT
private val full_range = 6 * plain_range + 1
object Dummy_Extender extends SyntaxUtilities.StyleExtender
{
override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
{
val new_styles = new Array[SyntaxStyle](full_range)
for (i <- 0 until full_range) {
new_styles(i) = styles(i % plain_range)
}
new_styles
}
}
def set_style_extender(extender: SyntaxUtilities.StyleExtender)
{
SyntaxUtilities.setStyleExtender(extender)
GUI_Thread.later { jEdit.propertiesChanged }
}
def dummy_style_extender() { set_style_extender(Dummy_Extender) }
}
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
