# HG changeset patch
# User wenzelm
# Date 1308148203 -7200
# Node ID c2b0cfeaa5abf72fe83362c346ea08f4f32576fb
# Parent  b35ff420d72094399f9ce14ecfc0306da23fc20a# Parent  c3e2a361b4185783bb4fa549a150613b29bedc71
merged

diff -r b35ff420d720 -r c2b0cfeaa5ab src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Jun 15 15:11:18 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Jun 15 16:30:03 2011 +0200
@@ -197,7 +197,7 @@
 if [ "$OUTDATED" = true ]
 then
   [ "${#UPDATED[@]}" -gt 0 ] && {
-    echo "Rebuild due to updated file dependencies:"
+    echo "Rebuild due changed files:"
     for FILE in "${UPDATED[@]}"
     do
       echo "  $FILE"
@@ -224,10 +224,14 @@
   cp -a "${RESOURCES[@]}" dist/classes/.
   cp src/jEdit.props dist/properties/.
   cp -a src/modes/. dist/modes/.
+  cp -a "$SCALA_HOME/misc/scala-tool-support/jedit/modes/scala.xml" dist/modes/.
 
-  perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
-    print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
-    print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
+  perl -i -e 'while (<>) {
+    if (m/NAME="javacc"/) {
+      print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
+      print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
+    elsif (m/NAME="scheme"/) {
+      print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
     print; }' dist/modes/catalog
 
   cp -a "${JEDIT_JARS[@]}" "${SCALA_JARS[@]}" "$ISABELLE_HOME/lib/classes/Pure.jar" \
diff -r b35ff420d720 -r c2b0cfeaa5ab src/Tools/jEdit/patches/scriptstyles
--- a/src/Tools/jEdit/patches/scriptstyles	Wed Jun 15 15:11:18 2011 +0200
+++ b/src/Tools/jEdit/patches/scriptstyles	Wed Jun 15 16:30:03 2011 +0200
@@ -1,30 +1,71 @@
-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);
-> 
+diff -ru jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+--- jEdit/org/gjt/sp/jedit/syntax/Token.java	2010-05-09 14:29:24.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2011-06-15 13:48:42.000000000 +0200
+@@ -57,7 +57,7 @@
+ 	 */
+ 	public static String tokenToString(byte token)
+ 	{
+-		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
++		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
+ 	} //}}}
+ 
+ 	//{{{ Token types
+diff -ru jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- jEdit/org/gjt/sp/util/SyntaxUtilities.java	2010-05-09 14:29:29.000000000 +0200
++++ jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2011-06-15 14:11:30.000000000 +0200
+@@ -26,6 +26,7 @@
+ //{{{ Imports
+ import java.awt.Color;
+ import java.awt.Font;
++import java.awt.font.TextAttribute;
+ import java.util.Locale;
+ import java.util.StringTokenizer;
+ import org.gjt.sp.jedit.syntax.SyntaxStyle;
+@@ -194,6 +195,17 @@
+ 	}
+ 	
+ 	/**
++	 * Style with sub/superscript font attribute.
++	 */
++	public static SyntaxStyle scriptStyle(SyntaxStyle style, int script)
++	{
++		java.util.Map attributes = new java.util.HashMap();
++		attributes.put(TextAttribute.SUPERSCRIPT, new Integer(script));
++		return new SyntaxStyle(style.getForegroundColor(), style.getBackgroundColor(),
++                  style.getFont().deriveFont(attributes));
++	}
++	
++	/**
+ 	 * Loads the syntax styles from the properties, giving them the specified
+ 	 * base font family and size.
+ 	 * @param family The font family
+@@ -203,10 +215,10 @@
+ 	 */
+ 	public static SyntaxStyle[] loadStyles(String family, int size, boolean color)
+ 	{
+-		SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT];
++		SyntaxStyle[] styles = new SyntaxStyle[3 * Token.ID_COUNT + 1];
+ 
+ 		// start at 1 not 0 to skip Token.NULL
+-		for(int i = 1; i < styles.length; i++)
++		for(int i = 1; i < Token.ID_COUNT; i++)
+ 		{
+ 			try
+ 			{
+@@ -223,6 +235,16 @@
+ 			}
+ 		}
+ 
++		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
++		for(int i = 0; i < Token.ID_COUNT; i++)
++		{
++			styles[i + Token.ID_COUNT] = scriptStyle(styles[i], -1);
++			styles[i + 2 * Token.ID_COUNT] = scriptStyle(styles[i], 1);
++		}
++		styles[0] = null;
++		styles[3 * Token.ID_COUNT] =
++			new SyntaxStyle(Color.black, null, new Font(family, 0, 1));
++
+ 		return styles;
+ 	} //}}}
+ 	
diff -r b35ff420d720 -r c2b0cfeaa5ab src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jun 15 15:11:18 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jun 15 16:30:03 2011 +0200
@@ -25,6 +25,16 @@
 {
   object Token_Markup
   {
+    /* extended token styles */
+
+    private val plain_range: Int = Token.ID_COUNT
+    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 }
+    val hidden: Byte = (3 * plain_range).toByte
+
+
     /* line context */
 
     private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
@@ -46,15 +56,6 @@
 
   private val key = "isabelle.document_model"
 
-  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
-  {
-    Swing_Thread.require()
-    val model = new Document_Model(session, buffer, thy_name)
-    buffer.setProperty(key, model)
-    model.activate()
-    model
-  }
-
   def apply(buffer: Buffer): Option[Document_Model] =
   {
     Swing_Thread.require()
@@ -74,6 +75,15 @@
         buffer.unsetProperty(key)
     }
   }
+
+  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
+  {
+    exit(buffer)
+    val model = new Document_Model(session, buffer, thy_name)
+    buffer.setProperty(key, model)
+    model.activate()
+    model
+  }
 }
 
 
diff -r b35ff420d720 -r c2b0cfeaa5ab src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 15:11:18 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 15 16:30:03 2011 +0200
@@ -31,15 +31,6 @@
 
   private val key = new Object
 
-  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
-  {
-    Swing_Thread.require()
-    val doc_view = new Document_View(model, text_area)
-    text_area.putClientProperty(key, doc_view)
-    doc_view.activate()
-    doc_view
-  }
-
   def apply(text_area: JEditTextArea): Option[Document_View] =
   {
     Swing_Thread.require()
@@ -59,6 +50,15 @@
         text_area.putClientProperty(key, null)
     }
   }
+
+  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
+  {
+    exit(text_area)
+    val doc_view = new Document_View(model, text_area)
+    text_area.putClientProperty(key, doc_view)
+    doc_view.activate()
+    doc_view
+  }
 }
 
 
diff -r b35ff420d720 -r c2b0cfeaa5ab src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Wed Jun 15 15:11:18 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Wed Jun 15 16:30:03 2011 +0200
@@ -185,8 +185,6 @@
   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,
diff -r b35ff420d720 -r c2b0cfeaa5ab src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 15:11:18 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 15 16:30:03 2011 +0200
@@ -9,12 +9,16 @@
 
 import isabelle._
 
-import java.awt.Graphics2D
+import java.awt.{Graphics2D, Shape}
+import java.awt.font.TextAttribute
+import java.text.AttributedString
 import java.util.ArrayList
 
+import org.gjt.sp.util.Log
+
 import org.gjt.sp.jedit.Debug
 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
-import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
 
 
 class Text_Area_Painter(doc_view: Document_View)
@@ -23,9 +27,20 @@
   private val buffer = model.buffer
   private val text_area = doc_view.text_area
 
-  private val orig_text_painter: TextAreaExtension =
+  private def painter_body(body: => Unit)
   {
-    val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
+    if (buffer == text_area.getBuffer)
+      Swing_Thread.now {
+        try { Isabelle.buffer_lock(buffer) { body } }
+        catch { case t: Throwable => Log.log(Log.ERROR, this, t) }
+      }
+  }
+
+
+  /* original painters */
+
+  private def pick_extension(name: String): TextAreaExtension =
+  {
     text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
     match {
       case List(x) => x
@@ -33,34 +48,34 @@
     }
   }
 
+  private val orig_text_painter =
+    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
 
-  /* painter snapshot */
-
-  @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
 
-  private def painter_snapshot(): Document.Snapshot =
-    _painter_snapshot match {
-      case Some(snapshot) => snapshot
-      case None => error("Missing document snapshot for text area painter")
-    }
+  /* common painter state */
 
-  private val set_snapshot = new TextAreaExtension
+  @volatile private var painter_snapshot: Document.Snapshot = null
+  @volatile private var painter_clip: Shape = null
+
+  private val set_state = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      _painter_snapshot = Some(model.snapshot())
+      painter_snapshot = model.snapshot()
+      painter_clip = gfx.getClip
     }
   }
 
-  private val reset_snapshot = new TextAreaExtension
+  private val reset_state = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      _painter_snapshot = None
+      painter_snapshot = null
+      painter_clip = null
     }
   }
 
@@ -73,8 +88,8 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      Isabelle.swing_buffer_lock(buffer) {
-        val snapshot = painter_snapshot()
+      painter_body {
+        val snapshot = painter_snapshot
         val ascent = text_area.getPainter.getFontMetrics.getAscent
 
         for (i <- 0 until physical_lines.length) {
@@ -148,6 +163,14 @@
 
   /* text */
 
+  def char_width(): Int =
+  {
+    val painter = text_area.getPainter
+    val font = painter.getFont
+    val font_context = painter.getFontRenderContext
+    font.getStringBounds(" ", font_context).getWidth.round.toInt
+  }
+
   private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
   {
     val painter = text_area.getPainter
@@ -161,7 +184,7 @@
       else {
         val max = buffer.getIntegerProperty("maxLineLen", 0)
         if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
-        else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3
+        else painter.getWidth - char_width() * 3
       }.toFloat
 
     val out = new ArrayList[Chunk]
@@ -183,10 +206,11 @@
   }
 
   private def paint_chunk_list(gfx: Graphics2D,
-    offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+    offset: Text.Offset, caret_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
     val clip_rect = gfx.getClipBounds
-    val font_context = text_area.getPainter.getFontRenderContext
+    val painter = text_area.getPainter
+    val font_context = painter.getFontRenderContext
 
     var w = 0.0f
     var chunk_offset = offset
@@ -206,7 +230,8 @@
 
         gfx.setFont(chunk_font)
         if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
-            markup.forall(info => info.info.isEmpty)) {
+            markup.forall(info => info.info.isEmpty) &&
+            !chunk_range.contains(caret_offset)) {
           gfx.setColor(chunk_color)
           gfx.drawGlyphVector(chunk.gv, x + w, y)
         }
@@ -215,7 +240,17 @@
           for (Text.Info(range, info) <- markup) {
             val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
             gfx.setColor(info.getOrElse(chunk_color))
-            gfx.drawString(str, x1.toInt, y.toInt)
+            if (range.contains(caret_offset)) {
+              val astr = new AttributedString(str)
+              val i = caret_offset - range.start
+              astr.addAttribute(TextAttribute.FONT, chunk_font)
+              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, i + 1)
+              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, i + 1)
+              gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
+            }
+            else {
+              gfx.drawString(str, x1.toInt, y.toInt)
+            }
             x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
           }
         }
@@ -233,24 +268,31 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      Isabelle.swing_buffer_lock(buffer) {
+      painter_body {
         val clip = gfx.getClip
         val x0 = text_area.getHorizontalOffset
         val fm = text_area.getPainter.getFontMetrics
         var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
 
+        val caret_offset =
+          if (text_area.hasFocus) text_area.getCaretPosition
+          else -1
+
         val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
-            infos.get(start(i)) match {
-              case Some(chunk) =>
-                val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
-                gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
-                orig_text_painter.paintValidLine(gfx,
-                  first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
-                gfx.setClip(clip)
-              case None =>
-            }
+            val x1 =
+              infos.get(start(i)) match {
+                case None => x0
+                case Some(chunk) =>
+                  gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
+                  val w = paint_chunk_list(gfx, start(i), caret_offset, chunk, x0, y0).toInt
+                  x0 + w.toInt
+              }
+            gfx.clipRect(x1, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
+            orig_text_painter.paintValidLine(gfx,
+              first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
+            gfx.setClip(clip)
           }
           y0 += line_height
         }
@@ -259,15 +301,60 @@
   }
 
 
+  /* caret -- outside of text range */
+
+  private class Caret_Painter(before: Boolean) extends TextAreaExtension
+  {
+    override def paintValidLine(gfx: Graphics2D,
+      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+    {
+      if (before) gfx.clipRect(0, 0, 0, 0)
+      else gfx.setClip(painter_clip)
+    }
+  }
+
+  private val before_caret_painter1 = new Caret_Painter(true)
+  private val after_caret_painter1 = new Caret_Painter(false)
+  private val before_caret_painter2 = new Caret_Painter(true)
+  private val after_caret_painter2 = new Caret_Painter(false)
+
+  private val caret_painter = new TextAreaExtension
+  {
+    override def paintValidLine(gfx: Graphics2D,
+      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+    {
+      painter_body {
+        if (text_area.hasFocus) {
+          val caret = text_area.getCaretPosition
+          if (start <= caret && caret == end - 1) {
+            val painter = text_area.getPainter
+            val fm = painter.getFontMetrics
+
+            val offset = caret - text_area.getLineStartOffset(physical_line)
+            val x = text_area.offsetToXY(physical_line, offset).x
+            gfx.setColor(painter.getCaretColor)
+            gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
+          }
+        }
+      }
+    }
+  }
+
+
   /* activation */
 
   def activate()
   {
     val painter = text_area.getPainter
-    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
+    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
-    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
+    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
+    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
+    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
+    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
+    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
+    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
     painter.removeExtension(orig_text_painter)
   }
 
@@ -275,10 +362,15 @@
   {
     val painter = text_area.getPainter
     painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
-    painter.removeExtension(reset_snapshot)
+    painter.removeExtension(reset_state)
+    painter.removeExtension(caret_painter)
+    painter.removeExtension(after_caret_painter2)
+    painter.removeExtension(before_caret_painter2)
+    painter.removeExtension(after_caret_painter1)
+    painter.removeExtension(before_caret_painter1)
     painter.removeExtension(text_painter)
     painter.removeExtension(background_painter)
-    painter.removeExtension(set_snapshot)
+    painter.removeExtension(set_state)
   }
 }