--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:31:58 2009 +0200
@@ -17,11 +17,13 @@
import java.awt.Font
import javax.swing.text.Segment;
-object DynamicTokenMarker {
+
+object DynamicTokenMarker
+{
- // Mapping to jEdits token types
+ // Mapping to jEdit token types
def choose_byte(kind: String): Byte = {
- // TODO: as properties
+ // TODO: as properties or CSS style sheet
kind match {
// logical entities
case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
@@ -63,12 +65,13 @@
List(Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT,
Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING).exists(kind == _)
- def choose_color(kind : String, styles: Array[SyntaxStyle]) : Color =
+ def choose_color(kind : String, styles: Array[SyntaxStyle]): Color =
styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
}
-class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker {
+class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker
+{
override def markTokens(prev: TokenMarker.LineContext,
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Tue Jun 02 22:31:58 2009 +0200
@@ -1,8 +1,7 @@
/*
- * IsabelleHyperlinkSource.scala
+ * Hyperlink setup for Isabelle proof documents
*
- * To change this template, choose Tools | Template Manager
- * and open the template in the editor.
+ * @author Fabian Immler, TU Munich
*/
package isabelle.jedit
@@ -20,6 +19,7 @@
import isabelle.prover.RefInfo
+
class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
extends AbstractHyperlink(start, end, line, "")
{
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:31:58 2009 +0200
@@ -25,7 +25,8 @@
import org.gjt.sp.jedit.syntax.SyntaxStyle
-object TheoryView {
+object TheoryView
+{
val MAX_CHANGE_LENGTH = 1500
@@ -43,7 +44,8 @@
class TheoryView (text_area: JEditTextArea, document_actor: Actor)
- extends TextAreaExtension with BufferListener {
+ extends TextAreaExtension with BufferListener
+{
def id() = Isabelle.plugin.id()
@@ -135,9 +137,9 @@
}
}
- def to_current(from_id: String, pos : Int) =
+ def to_current(from_id: String, pos: Int) =
_to_current(from_id, if (col == null) changes else col :: changes, pos)
- def from_current(to_id: String, pos : Int) =
+ def from_current(to_id: String, pos: Int) =
_from_current(to_id, if (col == null) changes else col :: changes, pos)
def to_current(document: isabelle.proofdocument.ProofDocument, pos: Int): Int =
to_current(document.id, pos)
@@ -157,14 +159,14 @@
}
}
- def repaint_all() =
+ def repaint_all()
{
if (text_area != null)
text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine)
}
def encolor(gfx: Graphics2D,
- y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) =
+ y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
{
val start = text_area.offsetToXY(begin)
val stop =
@@ -187,7 +189,7 @@
/* TextAreaExtension methods */
override def paintValidLine(gfx: Graphics2D,
- screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) =
+ screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
val document = prover.document
def from_current(pos: Int) = this.from_current(document.id, pos)
@@ -254,7 +256,7 @@
start_line: Int, offset: Int, num_lines: Int, length: Int) { }
override def preContentInserted(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int) =
+ start_line: Int, offset: Int, num_lines: Int, length: Int)
{
val text = buffer.getText(offset, length)
if (col == null)
@@ -269,7 +271,7 @@
}
override def preContentRemoved(buffer: JEditBuffer,
- start_line: Int, start: Int, num_lines: Int, removed: Int) =
+ start_line: Int, start: Int, num_lines: Int, removed: Int)
{
if (col == null)
col = new Text.Change(id(), start, "", removed)
@@ -296,4 +298,5 @@
override def foldHandlerChanged(buffer: JEditBuffer) { }
override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
override def transactionComplete(buffer: JEditBuffer) { }
+
}