--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sat Sep 05 00:43:59 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sun Sep 06 13:31:22 2009 +0200
@@ -22,8 +22,15 @@
object DynamicTokenMarker
{
- // Mapping to jEdit token types
+ /* line context */
+
+ private class LineContext(val line: Int, prev: LineContext)
+ extends TokenMarker.LineContext(new ParserRuleSet("isabelle", "MAIN"), prev)
+
+
+ /* mapping to jEdit token types */
// TODO: as properties or CSS style sheet
+
private val choose_byte: Map[String, Byte] =
{
import JToken._
@@ -103,9 +110,9 @@
override def markTokens(prev: TokenMarker.LineContext,
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
{
- val previous = prev.asInstanceOf[IndexLineContext]
+ val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext]
val line = if (prev == null) 0 else previous.line + 1
- val context = new IndexLineContext(line, previous)
+ val context = new DynamicTokenMarker.LineContext(line, previous)
val start = buffer.getLineStartOffset(line)
val stop = start + line_segment.count
@@ -125,10 +132,11 @@
if (abs_stop > start)
if (abs_start < stop)
byte = DynamicTokenMarker.choose_byte(markup.info.toString)
- token_start = abs_start - start max 0
- token_length = (abs_stop - abs_start) -
- (start - abs_start max 0) -
- (abs_stop - stop max 0)
+ token_start = (abs_start - start) max 0
+ token_length =
+ (abs_stop - abs_start) -
+ ((start - abs_start) max 0) -
+ ((abs_stop - stop) max 0)
} {
if (start + token_start > next_x)
handler.handleToken(line_segment, 1,
@@ -147,7 +155,3 @@
return context
}
}
-
-
-class IndexLineContext(val line: Int, prev: IndexLineContext)
- extends TokenMarker.LineContext(new ParserRuleSet("isabelle", "MAIN"), prev)
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Sat Sep 05 00:43:59 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Sun Sep 06 13:31:22 2009 +0200
@@ -12,22 +12,21 @@
import javax.swing._
import java.awt.event._
import java.awt._
-import org.gjt.sp.jedit.gui.RolloverButton;
-import org.gjt.sp.jedit.textarea.JEditTextArea;
-import org.gjt.sp.jedit.buffer.JEditBuffer;
+import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit._
class PhaseOverviewPanel(
- prover: Prover,
- textarea: JEditTextArea,
- to_current: (ProofDocument, Int) => Int)
-extends JPanel(new BorderLayout)
+ prover: Prover,
+ textarea: JEditTextArea,
+ to_current: (ProofDocument, Int) => Int)
+ extends JPanel(new BorderLayout)
{
-
private val WIDTH = 10
private val HILITE_HEIGHT = 2
- setRequestFocusEnabled(false);
+ setRequestFocusEnabled(false)
addMouseListener(new MouseAdapter {
override def mousePressed(evt : MouseEvent) {
@@ -38,14 +37,14 @@
})
override def addNotify {
- super.addNotify();
- ToolTipManager.sharedInstance.registerComponent(this);
+ super.addNotify()
+ ToolTipManager.sharedInstance.registerComponent(this)
}
override def removeNotify()
{
super.removeNotify
- ToolTipManager.sharedInstance.unregisterComponent(this);
+ ToolTipManager.sharedInstance.unregisterComponent(this)
}
override def getToolTipText(evt : MouseEvent) : String =
@@ -71,7 +70,7 @@
}
gfx.setColor(light)
- gfx.fillRect(0, y, getWidth - 1, 1 max height)
+ gfx.fillRect(0, y, getWidth - 1, height max 1)
if (height > 2) {
gfx.setColor(dark)
gfx.drawRect(0, y, getWidth - 1, height)
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Sat Sep 05 00:43:59 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Sun Sep 06 13:31:22 2009 +0200
@@ -141,9 +141,9 @@
}
})
- def add_result (result: Result) = {
+ def add_result(result: Result) {
buffer.addUnrendered(buffer.size, result)
- vscroll.setMaximum (Math.max(1, buffer.size * subunits))
+ vscroll.setMaximum ((buffer.size * subunits) max 1)
infopanel.setIndicator(true)
infopanel.setText(buffer.size.toString)
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sat Sep 05 00:43:59 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Sep 06 13:31:22 2009 +0200
@@ -273,7 +273,7 @@
var e = document.find_command_at(from_current(start))
while (e != null && e.start(document) < end) {
val begin = start max to_current(e.start(document))
- val finish = end - 1 min to_current(e.stop(document))
+ val finish = (end - 1) min to_current(e.stop(document))
encolor(gfx, y, metrics.getHeight, begin, finish,
TheoryView.choose_color(e, document), true)
e = document.commands.next(e).getOrElse(null)
--- a/src/Tools/jEdit/src/prover/Prover.scala Sat Sep 05 00:43:59 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sun Sep 06 13:31:22 2009 +0200
@@ -10,15 +10,12 @@
import scala.collection.mutable
-import scala.collection.immutable.{TreeSet}
import scala.actors.Actor, Actor._
-import org.gjt.sp.util.Log
import javax.swing.JTextArea
import isabelle.jedit.Isabelle
import isabelle.proofdocument.{ProofDocument, Change, Token}
-import isabelle.Isar_Document
object ProverEvents
@@ -35,11 +32,12 @@
private val process =
{
val receiver = new Actor {
- def act() = {
+ def act() {
loop { react { case res: Isabelle_Process.Result => handle_result(res) } }
}
}.start
- new Isabelle_Process(isabelle_system, receiver, "-m", "xsymbols", logic) with Isar_Document
+ new Isabelle_Process(isabelle_system, receiver, "-m", "xsymbols", logic)
+ with Isar_Document
}
def stop() { process.kill }
@@ -170,28 +168,27 @@
}
def act() {
- import ProverEvents._
loop {
react {
- case change: Change => {
- val old = document(change.parent.get.id).get
- val (doc, structure_change) = old.text_changed(change)
- document_versions ::= doc
- edit_document(old, doc, structure_change)
- change_receiver ! doc
- }
+ case change: Change =>
+ val old = document(change.parent.get.id).get
+ val (doc, structure_change) = old.text_changed(change)
+ document_versions ::= doc
+ edit_document(old, doc, structure_change)
+ change_receiver ! doc
case x => System.err.println("warning: ignored " + x)
}
}
}
-
+
def set_document(path: String) {
process.begin_document(document_0.id, path)
}
private def edit_document(old: ProofDocument, doc: ProofDocument,
- changes: ProofDocument.StructureChange) = {
- val id_changes = changes map {case (c1, c2) =>
+ changes: ProofDocument.StructureChange) =
+ {
+ val id_changes = changes map { case (c1, c2) =>
(c1.map(_.id).getOrElse(document_0.id),
c2 match {
case None => None
--- a/src/Tools/jEdit/src/prover/State.scala Sat Sep 05 00:43:59 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala Sun Sep 06 13:31:22 2009 +0200
@@ -41,21 +41,21 @@
}).head
}
- lazy private val types =
+ private lazy val types =
markup_root.filter(_.info match {
case Command.TypeInfo(_) => true
case _ => false }).flatten(_.flatten)
def type_at(pos: Int): String =
{
- types.find(t => t.start <= pos && t.stop > pos).map(t =>
+ types.find(t => t.start <= pos && pos < t.stop).map(t =>
t.content + ": " + (t.info match {
case Command.TypeInfo(i) => i
case _ => "" })).
getOrElse(null)
}
- lazy private val refs =
+ private lazy val refs =
markup_root.filter(_.info match {
case Command.RefInfo(_, _, _, _) => true
case _ => false }).flatten(_.flatten)