# HG changeset patch # User wenzelm # Date 1252098260 -7200 # Node ID ff037c17332a3ce909a8d945df37d915b95cef54 # Parent efa196219dd3febbd49a26695be7c4fd9cdaa310 minor tuning; diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Fri Sep 04 23:04:20 2009 +0200 @@ -82,7 +82,7 @@ val text = buffer.getSegment(start, caret - start) val completion = - Isabelle.prover_setup(buffer).map(_.prover.completion) getOrElse Isabelle.completion + Isabelle.prover_setup(buffer).map(_.prover.completion).getOrElse(Isabelle.completion) completion.complete(text) match { case None => null diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/jedit/Plugin.scala --- a/src/Tools/jEdit/src/jedit/Plugin.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/Plugin.scala Fri Sep 04 23:04:20 2009 +0200 @@ -66,7 +66,8 @@ def default_logic(): String = { val logic = Isabelle.Property("logic") - if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC") + if (logic != null) logic + else system.getenv_strict("ISABELLE_LOGIC") } @@ -96,12 +97,14 @@ font_changed.event(font) } + /* event buses */ val state_update = new EventBus[Command] val command_change = new EventBus[Command] val document_change = new EventBus[ProofDocument] + /* selected state */ private var _selected_state: Command = null @@ -165,5 +168,4 @@ Isabelle.plugin = null scala.actors.Scheduler.shutdown() } - } diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Fri Sep 04 23:04:20 2009 +0200 @@ -8,17 +8,13 @@ package isabelle.jedit -import scala.actors.Actor -import scala.actors.Actor._ +import scala.actors.Actor, Actor._ import scala.collection.mutable import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove} import isabelle.prover.{Prover, ProverEvents, Command} -import java.awt.Graphics2D -import java.awt.event.{ActionEvent, ActionListener} -import java.awt.Color -import javax.swing.Timer +import java.awt.{Color, Graphics2D} import javax.swing.event.{CaretListener, CaretEvent} import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer} @@ -148,7 +144,7 @@ invalidate_all() phase_overview.repaint() - //track changes in buffer + // track changes in buffer buffer.addBufferListener(this) } @@ -326,5 +322,4 @@ } } } - } diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/proofdocument/Change.scala --- a/src/Tools/jEdit/src/proofdocument/Change.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/Change.scala Fri Sep 04 23:04:20 2009 +0200 @@ -1,5 +1,5 @@ /* - * Changes in text + * Changes of plain text * * @author Johannes Hölzl, TU Munich * @author Fabian Immler, TU Munich @@ -7,6 +7,7 @@ package isabelle.proofdocument + sealed abstract class Edit { val start: Int @@ -14,6 +15,7 @@ def after(offset: Int): Int } + case class Insert(start: Int, text: String) extends Edit { def before(offset: Int): Int = @@ -24,6 +26,7 @@ if (start <= offset) offset + text.length else offset } + case class Remove(start: Int, text: String) extends Edit { def before(offset: Int): Int = @@ -35,6 +38,7 @@ } // TODO: merge multiple inserts? + class Change( val id: String, val parent: Option[Change], diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Fri Sep 04 23:04:20 2009 +0200 @@ -8,10 +8,11 @@ package isabelle.proofdocument -import scala.actors.Actor -import scala.actors.Actor._ +import scala.actors.Actor, Actor._ import scala.collection.mutable.ListBuffer + import java.util.regex.Pattern + import isabelle.prover.{Prover, Command, Command_State} diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Command.scala Fri Sep 04 23:04:20 2009 +0200 @@ -83,9 +83,9 @@ def markup_node(begin: Int, end: Int, info: MarkupInfo): MarkupNode = { - new MarkupNode(this, symbol_index.decode(begin), symbol_index.decode(end), Nil, id, - content.substring(symbol_index.decode(begin), symbol_index.decode(end)), - info) + val start = symbol_index.decode(begin) + val stop = symbol_index.decode(end) + new MarkupNode(this, start, stop, Nil, id, content.substring(start, stop), info) } diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Fri Sep 04 23:04:20 2009 +0200 @@ -49,6 +49,31 @@ def remove(nodes: List[MarkupNode]) = set_children(children diff nodes) + def fits_into(node: MarkupNode): Boolean = + node.start <= this.start && this.stop <= node.stop + + def + (new_child: MarkupNode): MarkupNode = + { + if (new_child fits_into this) { + var inserted = false + val new_children = + children.map(c => + if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child} + else c) + if (!inserted) { + // new_child did not fit into children of this + // -> insert new_child between this and its children + val fitting = children filter(_ fits_into new_child) + (this remove fitting) add ((new_child /: fitting) (_ + _)) + } + else this set_children new_children + } + else { + System.err.println("ignored nonfitting markup: " + new_child) + this + } + } + def dfs: List[MarkupNode] = { var all = Nil : List[MarkupNode] for (child <- children) @@ -59,13 +84,13 @@ def leafs: List[MarkupNode] = { - if (children == Nil) return List(this) + if (children.isEmpty) return List(this) else return children flatMap (_.leafs) } def flatten: List[MarkupNode] = { var next_x = start - if(children.length == 0) List(this) + if (children.isEmpty) List(this) else { val filled_gaps = for { child <- children @@ -89,31 +114,6 @@ else filtered } - def + (new_child: MarkupNode): MarkupNode = - { - if (new_child fitting_into this) { - var inserted = false - val new_children = - children.map(c => - if ((new_child fitting_into c) && !inserted) {inserted = true; c + new_child} - else c) - if (!inserted) { - // new_child did not fit into children of this - // -> insert new_child between this and its children - val fitting = children filter(_ fitting_into new_child) - (this remove fitting) add ((new_child /: fitting) (_ + _)) - } - else this set_children new_children - } - else { - System.err.println("ignored nonfitting markup: " + new_child) - this - } - } - - // does this fit into node? - def fitting_into(node: MarkupNode) = node.start <= this.start && node.stop >= this.stop - override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString } diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Fri Sep 04 23:04:20 2009 +0200 @@ -11,9 +11,7 @@ import scala.collection.mutable import scala.collection.immutable.{TreeSet} - -import scala.actors.Actor -import scala.actors.Actor._ +import scala.actors.Actor, Actor._ import org.gjt.sp.util.Log import javax.swing.JTextArea @@ -22,10 +20,13 @@ import isabelle.proofdocument.{ProofDocument, Change, Token} import isabelle.Isar_Document -object ProverEvents { + +object ProverEvents +{ case class Activate } + class Prover(isabelle_system: Isabelle_System, logic: String, change_receiver: Actor) extends Actor { diff -r efa196219dd3 -r ff037c17332a src/Tools/jEdit/src/prover/State.scala --- a/src/Tools/jEdit/src/prover/State.scala Thu Sep 03 20:10:23 2009 +0200 +++ b/src/Tools/jEdit/src/prover/State.scala Fri Sep 04 23:04:20 2009 +0200 @@ -61,7 +61,7 @@ case _ => false }).flatten(_.flatten) def ref_at(pos: Int): Option[MarkupNode] = - refs.find(t => t.start <= pos && t.stop > pos) + refs.find(t => t.start <= pos && pos < t.stop) @@ -70,56 +70,55 @@ def + (message: XML.Tree): State = { val changed: State = - message match { - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WRITELN) :: _, _) - | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.PRIORITY) :: _, _) - | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WARNING) :: _, _) => - add_result(message) - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.ERROR) :: _, _) => - set_status(Command.Status.FAILED).add_result(message) - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => - (this /: elems) ((st, e) => - e match { - // command status - case XML.Elem(Markup.UNPROCESSED, _, _) => - st.set_status(Command.Status.UNPROCESSED) - case XML.Elem(Markup.FINISHED, _, _) => - st.set_status(Command.Status.FINISHED) - case XML.Elem(Markup.FAILED, _, _) => - st.set_status(Command.Status.FAILED) - case XML.Elem(kind, attr, body) => - val (begin, end) = Position.offsets_of(attr) - if (begin.isDefined && end.isDefined) { - if (kind == Markup.ML_TYPING) { - val info = body.first.asInstanceOf[XML.Text].content - st.add_markup(command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info))) - } - else if (kind == Markup.ML_REF) { - body match { - case List(XML.Elem(Markup.ML_DEF, attr, _)) => - st.add_markup(command.markup_node( - begin.get - 1, end.get - 1, - RefInfo( - Position.file_of(attr), - Position.line_of(attr), - Position.id_of(attr), - Position.offset_of(attr)))) - case _ => st + message match { + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WRITELN) :: _, _) + | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.PRIORITY) :: _, _) + | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WARNING) :: _, _) => + add_result(message) + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.ERROR) :: _, _) => + set_status(Command.Status.FAILED).add_result(message) + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => + (this /: elems) ((st, e) => + e match { + // command status + case XML.Elem(Markup.UNPROCESSED, _, _) => + st.set_status(Command.Status.UNPROCESSED) + case XML.Elem(Markup.FINISHED, _, _) => + st.set_status(Command.Status.FINISHED) + case XML.Elem(Markup.FAILED, _, _) => + st.set_status(Command.Status.FAILED) + case XML.Elem(kind, attr, body) => + val (begin, end) = Position.offsets_of(attr) + if (begin.isDefined && end.isDefined) { + if (kind == Markup.ML_TYPING) { + val info = body.first.asInstanceOf[XML.Text].content + st.add_markup(command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info))) + } + else if (kind == Markup.ML_REF) { + body match { + case List(XML.Elem(Markup.ML_DEF, attr, _)) => + st.add_markup(command.markup_node( + begin.get - 1, end.get - 1, + RefInfo( + Position.file_of(attr), + Position.line_of(attr), + Position.id_of(attr), + Position.offset_of(attr)))) + case _ => st + } + } + else { + st.add_markup(command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind))) } } - else { - st.add_markup(command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind))) - } - } - else st - case _ => st - }) - case _ => - System.err.println("ignored: " + message) - this - } + else st + case _ => st + }) + case _ => + System.err.println("ignored: " + message) + this + } command.changed() changed } - }