# HG changeset patch # User wenzelm # Date 1252236682 -7200 # Node ID 2f0c18f9b6c7c96a9c45a347416431c2412dafdf # Parent 611864f2729db32800491e9947d8bcba861e1781 minor tuning; diff -r 611864f2729d -r 2f0c18f9b6c7 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- 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) diff -r 611864f2729d -r 2f0c18f9b6c7 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- 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) diff -r 611864f2729d -r 2f0c18f9b6c7 src/Tools/jEdit/src/jedit/ScrollerDockable.scala --- 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) diff -r 611864f2729d -r 2f0c18f9b6c7 src/Tools/jEdit/src/jedit/TheoryView.scala --- 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) diff -r 611864f2729d -r 2f0c18f9b6c7 src/Tools/jEdit/src/prover/Prover.scala --- 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 diff -r 611864f2729d -r 2f0c18f9b6c7 src/Tools/jEdit/src/prover/State.scala --- 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)