--- 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
--- 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()
}
-
}
--- 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 @@
}
}
}
-
}
--- 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],
--- 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}
--- 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)
}
--- 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
}
--- 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
{
--- 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
}
-
}