# HG changeset patch
# User wenzelm
# Date 1243974718 -7200
# Node ID e8ac8794971fb0cc6a182dc8bced266036132fbf
# Parent  72b02f9c509c983b35ffae91caa75c33dd801cc4
superficial tuning;

diff -r 72b02f9c509c -r e8ac8794971f src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- 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 = {
diff -r 72b02f9c509c -r e8ac8794971f src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- 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, "")
 {
diff -r 72b02f9c509c -r e8ac8794971f src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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) { }
+
 }