--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/scriptstyles Tue Jun 14 17:24:23 2011 +0200
@@ -0,0 +1,30 @@
+diff -r jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+60c60
+< return (token == Token.END) ? "END" : TOKEN_TYPES[token];
+---
+> return (token == Token.END) ? "END" : TOKEN_TYPES[(token >= ID_COUNT) ? 0 : token];
+diff -r jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+196a197,207
+> * Style with sub/superscript font attribute.
+> */
+> public static SyntaxStyle scriptStyle(String family, int size, int script)
+> {
+> Font font = new Font(family, 0, size);
+> java.util.Map attributes = new java.util.HashMap();
+> attributes.put(java.awt.font.TextAttribute.SUPERSCRIPT, new Integer(script));
+> return new SyntaxStyle(Color.black, null, font.deriveFont(attributes));
+> }
+>
+> /**
+206c217
+< SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT];
+---
+> SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT + 2];
+209c220
+< for(int i = 1; i < styles.length; i++)
+---
+> for(int i = 1; i < Token.ID_COUNT; i++)
+225a237,239
+> styles[Token.ID_COUNT] = scriptStyle(family, size, -1);
+> styles[Token.ID_COUNT + 1] = scriptStyle(family, size, 1);
+>
--- a/src/Tools/jEdit/src/document_model.scala Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Tue Jun 14 17:24:23 2011 +0200
@@ -25,36 +25,6 @@
{
object Token_Markup
{
- /* extended token styles */
-
- private val plain_range: Int = Token.ID_COUNT
- private val full_range: Int = 3 * plain_range
- private def check_range(i: Int) { require(0 <= i && i < plain_range) }
-
- def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
- def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
-
- private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
- {
- import scala.collection.JavaConversions._
- val script_font =
- style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
- new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
- }
-
- def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
- {
- val new_styles = new Array[SyntaxStyle](full_range)
- for (i <- 0 until plain_range) {
- val style = styles(i)
- new_styles(i) = style
- new_styles(subscript(i.toByte)) = script_style(style, -1)
- new_styles(superscript(i.toByte)) = script_style(style, 1)
- }
- new_styles
- }
-
-
/* line context */
private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
@@ -197,12 +167,6 @@
val start = buffer.getLineStartOffset(line)
val stop = start + line_segment.count
- /* FIXME
- for (text_area <- Isabelle.jedit_text_areas(buffer)
- if Document_View(text_area).isDefined)
- Document_View(text_area).get.set_styles()
- */
-
def handle_token(style: Byte, offset: Text.Offset, length: Int) =
handler.handleToken(line_segment, style, offset, length, context)
--- a/src/Tools/jEdit/src/document_view.scala Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Tue Jun 14 17:24:23 2011 +0200
@@ -69,24 +69,6 @@
/** token handling **/
- /* extended token styles */
-
- private var styles: Array[SyntaxStyle] = null // owned by Swing thread
-
- def extend_styles()
- {
- Swing_Thread.require()
- styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
- }
- extend_styles()
-
- def set_styles()
- {
- Swing_Thread.require()
- text_area.getPainter.setStyles(styles)
- }
-
-
/* visible line ranges */
// simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
--- a/src/Tools/jEdit/src/isabelle_markup.scala Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Tue Jun 14 17:24:23 2011 +0200
@@ -185,6 +185,8 @@
private val token_style: Map[String, Byte] =
{
import Token._
+ val SUBSCRIPT: Byte = ID_COUNT
+ val SUPERSCRIPT: Byte = ID_COUNT + 1
Map[String, Byte](
// embedded source text
Markup.ML_SOURCE -> COMMENT3,
--- a/src/Tools/jEdit/src/plugin.scala Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Jun 14 17:24:23 2011 +0200
@@ -373,11 +373,7 @@
}
case msg: PropertiesChanged =>
- Swing_Thread.now {
- Isabelle.setup_tooltips()
- for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
- Document_View(text_area).get.extend_styles()
- }
+ Swing_Thread.now { Isabelle.setup_tooltips() }
Isabelle.session.global_settings.event(Session.Global_Settings)
case _ =>