--- a/src/Tools/jEdit/build.xml Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/build.xml Thu Mar 19 16:48:29 2009 +0100
@@ -66,11 +66,16 @@
nbproject/build-impl.xml file.
-->
+ <target name="run" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.run">
+ </target>
+ <target name="debug" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.debug">
+ </target>
<target name="-pre-jar">
<copy file="plugin/services.xml" todir="${build.classes.dir}" />
<copy file="plugin/dockables.xml" todir="${build.classes.dir}" />
<copy file="plugin/actions.xml" todir="${build.classes.dir}" />
<copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
+ <copy file="plugin/styles.props" todir="${build.classes.dir}" />
</target>
<target name="-post-jar">
<!-- jars -->
--- a/src/Tools/jEdit/nbproject/build-impl.xml Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/nbproject/build-impl.xml Thu Mar 19 16:48:29 2009 +0100
@@ -173,6 +173,9 @@
<javac debug="@{debug}" deprecation="${javac.deprecation}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includeantruntime="false" includes="@{includes}" source="${javac.source}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="${javac.target}">
<classpath>
<path path="@{classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
</classpath>
<compilerarg line="${javac.compilerargs} ${javac.compilerargs.jaxws}"/>
<customize/>
@@ -398,6 +401,7 @@
</target>
<target depends="init,deps-jar,-pre-pre-compile,-pre-compile,-compile-depend" if="have.sources" name="-do-compile">
<scalaProject1:scalac/>
+ <scalaProject1:javac/>
<copy todir="${build.classes.dir}">
<fileset dir="${src.dir}" excludes="${build.classes.excludes},${excludes}" includes="${includes}"/>
</copy>
--- a/src/Tools/jEdit/nbproject/genfiles.properties Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/nbproject/genfiles.properties Thu Mar 19 16:48:29 2009 +0100
@@ -4,5 +4,5 @@
# This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
# Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
nbproject/build-impl.xml.data.CRC32=8f41dcce
-nbproject/build-impl.xml.script.CRC32=828f71d1
-nbproject/build-impl.xml.stylesheet.CRC32=2aa5193a
+nbproject/build-impl.xml.script.CRC32=87cef431
+nbproject/build-impl.xml.stylesheet.CRC32=371897b9
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/styles.props Thu Mar 19 16:48:29 2009 +0100
@@ -0,0 +1,11 @@
+#syntax styles
+options.isabelle.styles.command.foreground=#000080
+options.isabelle.styles.keyword.foreground=#008000
+options.isabelle.styles.fixed_decl.foreground=#080808
+options.isabelle.styles.local_fact_decl.foreground=#080808
+options.isabelle.styles.fact.foreground=#080808
+options.isabelle.styles.method.foreground=#101010
+options.isabelle.styles.literal.foreground=#808000
+options.isabelle.styles.ident.foreground=#C0C000
+options.isabelle.styles.doc_source.foreground=#C00000
+options.isabelle.styles.ML_source.foreground=#C00000
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Thu Mar 19 16:48:29 2009 +0100
@@ -7,8 +7,7 @@
package isabelle.jedit
-import isabelle.proofdocument.ProofDocument
-import isabelle.prover.{Command, MarkupNode}
+import isabelle.prover.{Command, MarkupNode, Prover}
import isabelle.Markup
import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -20,59 +19,55 @@
object DynamicTokenMarker {
- def styles: Array[SyntaxStyle] = {
- val array = new Array[SyntaxStyle](256)
- // array(0) won't be used: reserved for global default-font
- array(1) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
- array(2) = new SyntaxStyle(new Color(255, 0, 255), Color.white, Isabelle.plugin.font)
- array(3) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
- array(4) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font)
- array(5) = new SyntaxStyle(new Color(255, 128, 128), Color.white,Isabelle.plugin.font)
- array(6) = new SyntaxStyle(Color.yellow, Color.white, Isabelle.plugin.font)
- array(7) = new SyntaxStyle( new Color(0, 192, 0), Color.white, Isabelle.plugin.font)
- array(8) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
- array(9) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font)
- array(10) = new SyntaxStyle(Color.gray, Color.white, Isabelle.plugin.font)
- array(11) = new SyntaxStyle(Color.white, Color.white, Isabelle.plugin.font)
- array(12) = new SyntaxStyle(Color.red, Color.white, Isabelle.plugin.font)
- array(13) = new SyntaxStyle(Color.orange, Color.white, Isabelle.plugin.font)
- return array
+ var styles : Array[SyntaxStyle] = null
+ def reload_styles: Array[SyntaxStyle] = {
+ styles = new Array[SyntaxStyle](256)
+ //jEdit styles
+ for(i <- 0 to Token.ID_COUNT) styles(i) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
+ //isabelle styles
+ def from_property(kind : String, spec : String, default : Color) : Color =
+ try {Color.decode(Isabelle.Property("styles." + kind + "." + spec))} catch {case _ => default}
+
+ for((kind, i) <- kinds) styles(i + FIRST_BYTE) = new SyntaxStyle(
+ from_property(kind, "foreground", Color.black),
+ from_property(kind, "background", Color.white),
+ Isabelle.plugin.font)
+ return styles
}
- def choose_byte(kind: String): Byte = {
- // TODO: as properties
- kind match {
- // logical entities
- case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
- | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
- | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => 2
- // inner syntax
- case Markup.TFREE | Markup.FREE => 3
- case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => 4
- case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
- | Markup.INNER_COMMENT => 5
- case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
- | Markup.ATTRIBUTE | Markup.METHOD => 6
- // embedded source text
- case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
- | Markup.DOC_ANTIQ => 7
- // outer syntax
- case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => 8
- case Markup.VERBATIM => 9
- case Markup.COMMENT => 10
- case Markup.CONTROL => 11
- case Markup.MALFORMED => 12
- case Markup.STRING | Markup.ALTSTRING => 13
- // other
- case _ => 1
- }
+ private final val FIRST_BYTE : Byte = 30
+ val kinds = List(// TODO Markups as Enumeration?
+ // default style
+ null,
+ // logical entities
+ Markup.TCLASS, Markup.TYCON, Markup.FIXED_DECL, Markup.FIXED, Markup.CONST_DECL,
+ Markup.CONST, Markup.FACT_DECL, Markup.FACT, Markup.DYNAMIC_FACT,
+ Markup.LOCAL_FACT_DECL, Markup.LOCAL_FACT,
+ // inner syntax
+ Markup.TFREE, Markup.FREE,
+ Markup.TVAR, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
+ Markup.NUM, Markup.FLOAT, Markup.XNUM, Markup.XSTR, Markup.LITERAL,
+ Markup.INNER_COMMENT,
+ Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP,
+ Markup.ATTRIBUTE, Markup.METHOD,
+ // embedded source text
+ Markup.ML_SOURCE, Markup.DOC_SOURCE, Markup.ANTIQ, Markup.ML_ANTIQ,
+ Markup.DOC_ANTIQ,
+ // outer syntax
+ Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT,
+ Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING
+ ).zipWithIndex
+
+ def choose_byte(kind : String) : Byte = (kinds.find (k => kind == k._1)) match {
+ case Some((kind, index)) => (index + FIRST_BYTE).asInstanceOf[Byte]
+ case _ => FIRST_BYTE
}
def choose_color(kind : String) : Color = styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
}
-class DynamicTokenMarker(buffer: JEditBuffer, document: ProofDocument) extends TokenMarker {
+class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker {
override def markTokens(prev: TokenMarker.LineContext,
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
@@ -85,30 +80,25 @@
def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
- val commands = document.commands.dropWhile(_.stop <= from(start))
- if(commands.hasNext) {
- var next_x = start
- for {
- command <- commands.takeWhile(_.start < from(stop))
- markup <- command.root_node.flatten
- if(to(markup.abs_stop) > start)
- if(to(markup.abs_start) < stop)
- byte = DynamicTokenMarker.choose_byte(markup.kind)
- token_start = to(markup.abs_start) - start max 0
- token_length = to(markup.abs_stop) - to(markup.abs_start) -
- (start - to(markup.abs_start) max 0) -
- (to(markup.abs_stop) - stop max 0)
- } {
- if (start + token_start > next_x)
- handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
- handler.handleToken(line_segment, byte, token_start, token_length, context)
- next_x = start + token_start + token_length
- }
- if (next_x < stop)
- handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
- } else {
- handler.handleToken(line_segment, 1, 0, line_segment.count, context)
+ var next_x = start
+ for {
+ command <- prover.document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
+ markup <- command.root_node.flatten
+ if(to(markup.abs_stop) > start)
+ if(to(markup.abs_start) < stop)
+ byte = DynamicTokenMarker.choose_byte(markup.kind)
+ token_start = to(markup.abs_start) - start max 0
+ token_length = to(markup.abs_stop) - to(markup.abs_start) -
+ (start - to(markup.abs_start) max 0) -
+ (to(markup.abs_stop) - stop max 0)
+ } {
+ if (start + token_start > next_x)
+ handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
+ handler.handleToken(line_segment, byte, token_start, token_length, context)
+ next_x = start + token_start + token_length
}
+ if (next_x < stop)
+ handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
handler.handleToken(line_segment,Token.END, line_segment.count, 0, context)
handler.setLineContext(context)
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Mar 19 16:48:29 2009 +0100
@@ -32,10 +32,9 @@
val prover_setup = Isabelle.plugin.prover_setup(buffer)
if (prover_setup.isDefined) {
val document = prover_setup.get.prover.document
- val commands = document.commands
- while (!stopped && commands.hasNext) {
- data.root.add(commands.next.root_node.swing_node)
- }
+ for (command <- document.commands)
+ data.root.add(command.root_node.swing_node)
+
if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
} else {
data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
@@ -51,7 +50,7 @@
override def canCompleteAnywhere = true
override def getInstantCompletionTriggers = "\\"
- override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
+ override def complete(pane: EditPane, caret: Int): SideKickCompletion = null /*{
val buffer = pane.getBuffer
val ps = Isabelle.prover_setup(buffer)
if (ps.isDefined) {
@@ -83,7 +82,7 @@
}
return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
} else return null
- }
+ }*/
}
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Thu Mar 19 16:48:29 2009 +0100
@@ -24,7 +24,6 @@
var textarea : JEditTextArea = null
val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
- prover.command_info += (_ => repaint_delay.delay_or_ignore())
setRequestFocusEnabled(false);
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Mar 19 16:48:29 2009 +0100
@@ -10,7 +10,6 @@
import isabelle.prover.{Prover, Command}
import isabelle.renderer.UserAgent
-
import org.w3c.dom.Document
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, View}
@@ -35,12 +34,12 @@
def activate(view: View) {
prover = new Prover(Isabelle.system, Isabelle.default_logic)
-
+ prover.start() //start actor
val buffer = view.getBuffer
val path = buffer.getPath
- theory_view = new TheoryView(view.getTextArea)
- prover.set_document(theory_view,
+ theory_view = new TheoryView(view.getTextArea, prover)
+ prover.set_document(theory_view.change_receiver,
if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path)
theory_view.activate
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Mar 19 16:48:29 2009 +0100
@@ -8,6 +8,7 @@
package isabelle.jedit
+import scala.actors.Actor
import isabelle.proofdocument.Text
import isabelle.prover.{Prover, Command}
@@ -38,15 +39,15 @@
}
-class TheoryView (text_area: JEditTextArea)
- extends TextAreaExtension with Text with BufferListener {
+class TheoryView (text_area: JEditTextArea, document_actor: Actor)
+ extends TextAreaExtension with BufferListener {
private val buffer = text_area.getBuffer
private val prover = Isabelle.prover_setup(buffer).get.prover
buffer.addBufferListener(this)
- private var col: Text.Changed = null
+ private var col: Text.Change = null
private val col_timer = new Timer(300, new ActionListener() {
override def actionPerformed(e: ActionEvent) = commit
@@ -66,7 +67,7 @@
private def update_styles = {
if (text_area != null) {
if (Isabelle.plugin.font != null) {
- text_area.getPainter.setStyles(DynamicTokenMarker.styles)
+ text_area.getPainter.setStyles(DynamicTokenMarker.reload_styles)
repaint_all
}
}
@@ -86,8 +87,9 @@
phase_overview.textarea = text_area
text_area.addLeftOfScrollBar(phase_overview)
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
- buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
+ buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
update_styles
+ document_actor ! new Text.Change(0,buffer.getText(0, buffer.getLength),0)
}
def deactivate() = {
@@ -100,18 +102,28 @@
/* painting */
val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
- prover.command_info += (_ => repaint_delay.delay_or_ignore())
+
+ val change_receiver = scala.actors.Actor.actor {
+ scala.actors.Actor.loop {
+ scala.actors.Actor.react {
+ case _ => {
+ repaint_delay.delay_or_ignore()
+ phase_overview.repaint_delay.delay_or_ignore()
+ }
+ }
+ }
+ }.start
def from_current (pos: Int) =
if (col != null && col.start <= pos)
- if (pos < col.start + col.added) col.start
- else pos - col.added + col.removed
+ if (pos < col.start + col.added.length) col.start
+ else pos - col.added.length + col.removed
else pos
def to_current (pos : Int) =
if (col != null && col.start <= pos)
if (pos < col.start + col.removed) col.start
- else pos + col.added - col.removed
+ else pos + col.added.length - col.removed
else pos
def repaint(cmd: Command) =
@@ -162,9 +174,10 @@
val metrics = text_area.getPainter.getFontMetrics
var e = prover.document.find_command_at(from_current(start))
-
+ val commands = prover.document.commands.dropWhile(_.stop <= from_current(start)).
+ takeWhile(c => to_current(c.start) < end)
// encolor phase
- while (e != null && to_current(e.start) < end) {
+ for (e <- commands) {
val begin = start max to_current(e.start)
val finish = end - 1 min to_current(e.stop)
encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
@@ -178,25 +191,16 @@
DynamicTokenMarker.choose_color(node.kind), true)
}
}
- e = e.next
}
gfx.setColor(saved_color)
}
-
- /* Text methods */
-
- def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
- def length = buffer.getLength
- val changes = new EventBus[Text.Changed]
-
-
/* BufferListener methods */
private def commit {
if (col != null)
- changes.event(col)
+ document_actor ! col
col = null
if (col_timer.isRunning())
col_timer.stop()
@@ -211,51 +215,50 @@
override def contentInserted(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int)
+ start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+ override def contentRemoved(buffer: JEditBuffer,
+ 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) =
{
-/*
+ val text = buffer.getText(offset, length)
if (col == null)
- col = new Text.Changed(offset, length, 0)
- else if (col.start <= offset && offset <= col.start + col.added)
- col = new Text.Changed(col.start, col.added + length, col.removed)
+ col = new Text.Change(offset, text, 0)
+ else if (col.start <= offset && offset <= col.start + col.added.length)
+ col = new Text.Change(col.start, col.added + text, col.removed)
else {
commit
- col = new Text.Changed(offset, length, 0)
+ col = new Text.Change(offset, text, 0)
}
delay_commit
-*/
- changes.event(new Text.Changed(offset, length, 0))
}
override def preContentRemoved(buffer: JEditBuffer,
start_line: Int, start: Int, num_lines: Int, removed: Int) =
{
-/*
if (col == null)
- col = new Text.Changed(start, 0, removed)
- else if (col.start > start + removed || start > col.start + col.added) {
+ col = new Text.Change(start, "", removed)
+ else if (col.start > start + removed || start > col.start + col.added.length) {
commit
- col = new Text.Changed(start, 0, removed)
+ col = new Text.Change(start, "", removed)
}
else {
- val offset = start - col.start
- val diff = col.added - removed
+/* val offset = start - col.start
+ val diff = col.added.length - removed
val (added, add_removed) =
if (diff < offset)
(offset max 0, diff - (offset max 0))
else
(diff - (offset min 0), offset min 0)
- col = new Text.Changed(start min col.start, added, col.removed - add_removed)
+ col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
+ commit
+ col = new Text.Change(start, "", removed)
}
delay_commit
-*/
- changes.event(new Text.Changed(start, 0, removed))
}
- override def contentRemoved(buffer: JEditBuffer,
- 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) { }
override def bufferLoaded(buffer: JEditBuffer) { }
override def foldHandlerChanged(buffer: JEditBuffer) { }
override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Mar 19 16:48:29 2009 +0100
@@ -2,18 +2,21 @@
* Document as list of commands, consisting of lists of tokens
*
* @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
* @author Makarius
*/
package isabelle.proofdocument
-
+import scala.collection.mutable.ListBuffer
+import scala.actors.Actor
+import scala.actors.Actor._
import java.util.regex.Pattern
import isabelle.prover.{Prover, Command}
-
+import isabelle.utils.LinearSet
case class StructureChange(
- val before_change: Command,
+ val before_change: Option[Command],
val added_commands: List[Command],
val removed_commands: List[Command])
@@ -35,73 +38,52 @@
"`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
"[()\\[\\]{}:;]", Pattern.MULTILINE)
+ val empty = new ProofDocument(LinearSet.empty, LinearSet.empty, false, _ => false)
+
}
-class ProofDocument(text: Text, is_command_keyword: String => Boolean)
+class ProofDocument(val tokens: LinearSet[Token],
+ val commands: LinearSet[Command],
+ val active: Boolean,
+ is_command_keyword: String => Boolean)
{
- private var active = false
- def activate() {
- if (!active) {
- active = true
- text_changed(0, text.length, 0)
- }
+
+ def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword)
+ def activate: (ProofDocument, StructureChange) = {
+ val (doc, change) = text_changed(new Text.Change(0, content, content.length))
+ return (doc.mark_active, change)
}
-
- text.changes += (changed => text_changed(changed.start, changed.added, changed.removed))
+ def set_command_keyword(f: String => Boolean): ProofDocument =
+ new ProofDocument(tokens, commands, active, f)
-
-
+ def content = Token.string_from_tokens(List() ++ tokens)
/** token view **/
- private var first_token: Token = null
- private var last_token: Token = null
-
- private def tokens(start: Token, stop: Token) = new Iterator[Token] {
- var current = start
- def hasNext = current != stop && current != null
- def next() = { val save = current; current = current.next; save }
- }
- private def tokens(start: Token): Iterator[Token] = tokens(start, null)
- private def tokens(): Iterator[Token] = tokens(first_token, null)
-
-
- private def text_changed(start: Int, added_len: Int, removed_len: Int)
+ def text_changed(change: Text.Change): (ProofDocument, StructureChange) =
{
- if (!active)
- return
+ val tokens = List() ++ this.tokens
+ val (begin, remaining) = tokens.span(_.stop < change.start)
+ val (removed, end_unshifted) = remaining.span(_.start <= change.start + change.removed)
+ val end = for (t <- end_unshifted) yield t.shift(change.added.length - change.removed)
- var before_change =
- if (Token.check_stop(first_token, _ < start)) Token.scan(first_token, _.stop >= start)
- else null
-
- var first_removed =
- if (before_change != null) before_change.next
- else if (Token.check_start(first_token, _ <= start + removed_len)) first_token
- else null
-
- var last_removed = Token.scan(first_removed, _.start > start + removed_len)
+ val split_begin = removed.takeWhile(_.start < change.start).
+ map (t => new Token(t.start,
+ t.content.substring(0, change.start - t.start),
+ t.kind))
+ val split_end = removed.dropWhile(_.stop < change.start + change.removed).
+ map (t => new Token(change.start + change.added.length,
+ t.content.substring(change.start + change.removed - t.start),
+ t.kind))
- var shift_token =
- if (last_removed != null) last_removed
- else if (Token.check_start(first_token, _ > start)) first_token
- else null
-
- while (shift_token != null) {
- shift_token.shift(added_len - removed_len, start)
- shift_token = shift_token.next
- }
-
- // scan changed tokens until the end of the text or a matching token is
- // found which is beyond the changed area
- val match_start = if (before_change == null) 0 else before_change.stop
- var first_added: Token = null
- var last_added: Token = null
+ var invalid_tokens = split_begin :::
+ new Token(change.start, change.added, Token.Kind.OTHER) :: split_end ::: end
+ var new_tokens = Nil: List[Token]
+ var old_suffix = Nil: List[Token]
- val matcher = ProofDocument.token_pattern.matcher(text.content(match_start, text.length))
- var finished = false
- var position = 0
- while (matcher.find(position) && !finished) {
- position = matcher.end
+ val match_start = invalid_tokens.first.start
+ val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens))
+
+ while (matcher.find() && invalid_tokens != Nil) {
val kind =
if (is_command_keyword(matcher.group))
Token.Kind.COMMAND_START
@@ -109,252 +91,87 @@
Token.Kind.COMMENT
else
Token.Kind.OTHER
- val new_token = new Token(matcher.start + match_start, matcher.end + match_start, kind)
-
- if (first_added == null)
- first_added = new_token
- else {
- new_token.prev = last_added
- last_added.next = new_token
- }
- last_added = new_token
-
- while (Token.check_stop(last_removed, _ < new_token.stop) &&
- last_removed.next != null)
- last_removed = last_removed.next
-
- if (new_token.stop >= start + added_len &&
- Token.check_stop(last_removed, _ == new_token.stop))
- finished = true
- }
+ val new_token = new Token(match_start + matcher.start, matcher.group, kind)
+ new_tokens ::= new_token
- var after_change = if (last_removed != null) last_removed.next else null
-
- // remove superflous first token-change
- if (first_added != null && first_added == first_removed &&
- first_added.stop < start) {
- before_change = first_removed
- if (last_removed == first_removed) {
- last_removed = null
- first_removed = null
- }
- else {
- first_removed = first_removed.next
- assert(first_removed != null)
- }
-
- if (last_added == first_added) {
- last_added = null
- first_added = null
- }
- if (first_added != null)
- first_added = first_added.next
- }
-
- // remove superflous last token-change
- if (last_added != null && last_added == last_removed &&
- last_added.start > start + added_len) {
- after_change = last_removed
- if (first_removed == last_removed) {
- first_removed = null
- last_removed = null
- }
- else {
- last_removed = last_removed.prev
- assert(last_removed != null)
+ invalid_tokens = invalid_tokens dropWhile (_.stop < new_token.stop)
+ invalid_tokens match {
+ case t::ts => if(t.start == new_token.start &&
+ t.start > change.start + change.added.length) {
+ old_suffix = ts
+ invalid_tokens = Nil
+ }
+ case _ =>
}
-
- if (last_added == first_added) {
- last_added = null
- first_added = null
- }
- else
- last_added = last_added.prev
}
-
- if (first_removed == null && first_added == null)
- return
-
- if (first_token == null) {
- first_token = first_added
- last_token = last_added
- }
- else {
- // cut removed tokens out of list
- if (first_removed != null)
- first_removed.prev = null
- if (last_removed != null)
- last_removed.next = null
-
- if (first_token == first_removed)
- if (first_added != null)
- first_token = first_added
- else
- first_token = after_change
-
- if (last_token == last_removed)
- if (last_added != null)
- last_token = last_added
- else
- last_token = before_change
-
- // insert new tokens into list
- if (first_added != null) {
- first_added.prev = before_change
- if (before_change != null)
- before_change.next = first_added
- else
- first_token = first_added
- }
- else if (before_change != null)
- before_change.next = after_change
-
- if (last_added != null) {
- last_added.next = after_change
- if (after_change != null)
- after_change.prev = last_added
- else
- last_token = last_added
- }
- else if (after_change != null)
- after_change.prev = before_change
- }
+ val insert = new_tokens.reverse
+ val new_tokenset = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]]
- System.err.println("token_changed: " + before_change + " " + after_change + " " + first_removed)
- token_changed(before_change, after_change, first_removed)
+ token_changed(begin.lastOption,
+ insert,
+ removed,
+ new_tokenset,
+ old_suffix.firstOption)
}
-
-
/** command view **/
- val structural_changes = new EventBus[StructureChange]
-
- def commands_from(start: Token) = new Iterator[Command] {
- var current = start
- def hasNext = current != null
- def next = { val s = current.command ; current = s.last.next ; s }
- }
- def commands_from(start: Command): Iterator[Command] = commands_from(start.first)
- def commands = commands_from(first_token)
-
def find_command_at(pos: Int): Command = {
for (cmd <- commands) { if (pos < cmd.stop) return cmd }
return null
}
- private def token_changed(start: Token, stop: Token, removed: Token)
+ private def token_changed(before_change: Option[Token],
+ inserted_tokens: List[Token],
+ removed_tokens: List[Token],
+ new_tokenset: LinearSet[Token],
+ after_change: Option[Token]): (ProofDocument, StructureChange) =
{
- var removed_commands: List[Command] = Nil
- var first: Command = null
- var last: Command = null
-
- for (t <- tokens(removed)) {
- if (first == null)
- first = t.command
- if (t.command != last)
- removed_commands = t.command :: removed_commands
- last = t.command
+ val commands = List() ++ this.commands
+ val (begin, remaining) =
+ before_change match {
+ case None => (Nil, commands)
+ case Some(bc) => commands.break(_.tokens.contains(bc))
+ }
+ val (_removed, _end) =
+ after_change match {
+ case None => (remaining, Nil)
+ case Some(ac) => remaining.break(_.tokens.contains(ac))
+ }
+ val (removed, end) = _end match {
+ case Nil => (_removed, Nil)
+ case acc::end => if (after_change.isDefined && after_change.get.kind == Token.Kind.COMMAND_START)
+ (_removed, _end)
+ else (_removed ::: List(acc), end)
}
-
- var before: Command = null
- if (!removed_commands.isEmpty) {
- if (first.first == removed) {
- if (start == null)
- before = null
- else
- before = start.command
+ val all_removed_tokens = for(c <- removed; t <- c.tokens) yield t
+ val (pseudo_new_pre, rest) =
+ if (! before_change.isDefined) (Nil, all_removed_tokens)
+ else {
+ val (a, b) = all_removed_tokens.span (_ != before_change.get)
+ b match {
+ case Nil => (a, Nil)
+ case bc::rest => (a ::: List(bc), b)
+ }
}
- else
- before = first.prev
- }
+ val pseudo_new_post = rest.dropWhile(Some(_) != after_change)
- var added_commands: List[Command] = Nil
- var scan: Token = null
- if (start != null) {
- val next = start.next
- if (first != null && first.first != removed) {
- scan = first.first
- if (before == null)
- before = first.prev
- }
- else if (next != null && next != stop) {
- if (next.kind == Token.Kind.COMMAND_START) {
- before = start.command
- scan = next
- }
- else if (first == null || first.first == removed) {
- first = start.command
- removed_commands = first :: removed_commands
- scan = first.first
- if (before == null)
- before = first.prev
- }
- else {
- scan = first.first
- if (before == null)
- before = first.prev
- }
+ def tokens_to_commands(tokens: List[Token]): List[Command]= {
+ tokens match {
+ case Nil => Nil
+ case t::ts =>
+ val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
+ new Command(t::cmd) :: tokens_to_commands (rest)
}
}
- else
- scan = first_token
- var stop_scan: Token = null
- if (stop != null) {
- if (stop == stop.command.first)
- stop_scan = stop
- else
- stop_scan = stop.command.last.next
- }
- else if (last != null)
- stop_scan = last.last.next
- else
- stop_scan = null
-
- var cmd_start: Token = null
- var cmd_stop: Token = null
- var overrun = false
- var finished = false
- while (scan != null && !finished) {
- if (scan == stop_scan) {
- if (scan.kind == Token.Kind.COMMAND_START)
- finished = true
- else
- overrun = true
- }
+ val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
- if (scan.kind == Token.Kind.COMMAND_START && cmd_start != null && !finished) {
- if (!overrun) {
- added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
- cmd_start = scan
- cmd_stop = scan
- }
- else
- finished = true
- }
- else if (!finished) {
- if (cmd_start == null)
- cmd_start = scan
- cmd_stop = scan
- }
- if (overrun && !finished) {
- if (scan.command != last)
- removed_commands = scan.command :: removed_commands
- last = scan.command
- }
+ val new_commandset = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
+ val before = begin match {case Nil => None case _ => Some (begin.last)}
- if (!finished)
- scan = scan.next
- }
-
- if (cmd_start != null)
- added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
-
- // relink commands
- added_commands = added_commands.reverse
- removed_commands = removed_commands.reverse
-
- structural_changes.event(new StructureChange(before, added_commands, removed_commands))
+ val change = new StructureChange(before, new_commands, removed)
+ val doc = new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword)
+ return (doc, change)
}
}
--- a/src/Tools/jEdit/src/proofdocument/Text.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Thu Mar 19 16:48:29 2009 +0100
@@ -8,11 +8,7 @@
object Text {
- case class Changed(val start: Int, val added: Int, val removed: Int)
-}
-
-trait Text {
- def content(start: Int, stop: Int): String
- def length: Int
- def changes: EventBus[Text.Changed]
-}
+ case class Change(start: Int, val added: String, val removed: Int) {
+ override def toString = "start: " + start + " added: " + added + " removed: " + removed
+ }
+}
\ No newline at end of file
--- a/src/Tools/jEdit/src/proofdocument/Token.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Thu Mar 19 16:48:29 2009 +0100
@@ -18,44 +18,30 @@
val OTHER = Value("OTHER")
}
- def check_start(t: Token, P: Int => Boolean) = { t != null && P(t.start) }
- def check_stop(t: Token, P: Int => Boolean) = { t != null && P(t.stop) }
+ def check_start(t: Token, P: Int => Boolean) = t != null && P(t.start)
+ def check_stop(t: Token, P: Int => Boolean) = t != null && P(t.stop)
- def scan(s: Token, f: Token => Boolean): Token =
- {
- var current = s
- while (current != null) {
- val next = current.next
- if (next == null || f(next)) return current
- current = next
+ private def fill(n: Int) = {
+ val blanks = new Array[Char](n)
+ for(i <- 0 to n - 1) blanks(i) = ' '
+ new String(blanks)
+ }
+ def string_from_tokens (tokens: List[Token]): String = {
+ tokens match {
+ case Nil => ""
+ case t::tokens => (tokens.foldLeft
+ (t.content, t.stop)
+ ((a, token) => (a._1 + fill(token.start - a._2) + token.content, token.stop))
+ )._1
}
- return null
}
+
}
-class Token(var start: Int, var stop: Int, val kind: Token.Kind.Value)
-{
- var next: Token = null
- var prev: Token = null
- var command: Command = null
-
- def length = stop - start
-
- def shift(offset: Int, bottom_clamp: Int) {
- start = bottom_clamp max (start + offset)
- stop = bottom_clamp max (stop + offset)
- }
-
- override def toString: String = "[" + start + ":" + stop + "]"
+class Token(val start: Int, val content: String, val kind: Token.Kind.Value) {
+ val length = content.length
+ val stop = start + length
+ override def toString = content + "(" + kind + ")"
override def hashCode: Int = (31 + start) * 31 + stop
-
- override def equals(obj: Any): Boolean =
- {
- if (super.equals(obj)) return true
- if (null == obj) return false
- obj match {
- case other: Token => (start == other.start) && (stop == other.stop)
- case other: Any => false
- }
- }
+ def shift(i: Int) = new Token(start + i, content, kind)
}
--- a/src/Tools/jEdit/src/prover/Command.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Thu Mar 19 16:48:29 2009 +0100
@@ -29,40 +29,19 @@
}
-class Command(text: Text, val first: Token, val last: Token)
+class Command(val tokens: List[Token])
{
val id = Isabelle.plugin.id()
-
/* content */
- {
- var t = first
- while (t != null) {
- t.command = this
- t = if (t == last) null else t.next
- }
- }
-
override def toString = name
- val name = text.content(first.start, first.stop)
- val content = text.content(proper_start, proper_stop)
-
- def next = if (last.next != null) last.next.command else null
- def prev = if (first.prev != null) first.prev.command else null
-
- def start = first.start
- def stop = last.stop
+ val name = tokens.head.content
+ val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT))
- def proper_start = start
- def proper_stop = {
- var i = last
- while (i != first && i.kind == Token.Kind.COMMENT)
- i = i.prev
- i.stop
- }
-
+ def start = tokens.first.start
+ def stop = tokens.last.stop
/* command status */
--- a/src/Tools/jEdit/src/prover/Prover.scala Mon Mar 02 19:27:06 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Mar 19 16:48:29 2009 +0100
@@ -12,17 +12,26 @@
import scala.collection.mutable
import scala.collection.immutable.{TreeSet}
+import scala.actors.Actor
+import scala.actors.Actor._
+
import org.gjt.sp.util.Log
import isabelle.jedit.Isabelle
import isabelle.proofdocument.{StructureChange, ProofDocument, Text, Token}
import isabelle.IsarDocument
+object ProverEvents {
+ case class Activate
+ case class SetEventBus(bus: EventBus[StructureChange])
+ case class SetIsCommandKeyword(is_command_keyword: String => Boolean)
+}
-class Prover(isabelle_system: IsabelleSystem, logic: String)
+class Prover(isabelle_system: IsabelleSystem, logic: String) extends Actor
{
/* prover process */
+
private val process =
{
val results = new EventBus[IsabelleProcess.Result] + handle_result
@@ -40,8 +49,10 @@
private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
private val document_id0 = Isabelle.plugin.id()
- private var document_id = document_id0
- private var document_versions = Set(document_id)
+ private var document_versions = List((document_id0, ProofDocument.empty))
+
+ def document_id = document_versions.head._1
+ def document = document_versions.head._2
private var initialized = false
@@ -83,14 +94,12 @@
/* event handling */
val activated = new EventBus[Unit]
- val command_info = new EventBus[Command]
val output_info = new EventBus[String]
- var document: ProofDocument = null
-
-
- private def handle_result(result: IsabelleProcess.Result): Unit = Swing.now
+ var change_receiver = null: Actor
+
+ private def handle_result(result: IsabelleProcess.Result)
{
- def command_change(c: Command) = command_info.event(c)
+ def command_change(c: Command) = this ! c
val (running, command) =
result.props.find(p => p._1 == Markup.ID) match {
case None => (false, null)
@@ -104,21 +113,21 @@
output_info.event(result.toString)
else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) { // FIXME !?
initialized = true
- if (document != null) {
- document.activate()
- activated.event(())
- }
+ Swing.now { this ! ProverEvents.Activate }
}
else {
result.kind match {
case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
- | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR
- if command != null =>
- if (result.kind == IsabelleProcess.Kind.ERROR)
- command.status = Command.Status.FAILED
- command.add_result(running, process.parse_message(result))
- command_change(command)
+ | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR =>
+ if (command != null) {
+ if (result.kind == IsabelleProcess.Kind.ERROR)
+ command.status = Command.Status.FAILED
+ command.add_result(running, process.parse_message(result))
+ command_change(command)
+ } else {
+ output_info.event(result.toString)
+ }
case IsabelleProcess.Kind.STATUS =>
//{{{ handle all kinds of status messages here
@@ -145,13 +154,13 @@
if (commands.contains(cmd_id)) {
val cmd = commands(cmd_id)
if (cmd.state_id != null) states -= cmd.state_id
- states(state_id) = cmd
+ states(cmd_id) = cmd
cmd.state_id = state_id
cmd.status = Command.Status.UNPROCESSED
command_change(cmd)
}
+
}
-
// command status
case XML.Elem(Markup.UNPROCESSED, _, _)
if command != null =>
@@ -181,9 +190,10 @@
if (command == null) commands.getOrElse(markup_id, null)
// inner syntax: id from props
else command
- if (cmd != null)
+ if (cmd != null) {
cmd.root_node.insert(cmd.node_from(kind, begin, end))
-
+ command_change(cmd)
+ }
case _ =>
//}}}
}
@@ -197,36 +207,58 @@
}
}
- def set_document(text: Text, path: String): Unit = Swing.now
- {
- document = new ProofDocument(text, command_decls.contains(_))
+ def act() {
+ import ProverEvents._
+ loop {
+ react {
+ case Activate => {
+ val (doc, structure_change) = document.activate
+ val old_id = document_id
+ val doc_id = Isabelle.plugin.id()
+ document_versions ::= (doc_id, doc)
+ edit_document(old_id, doc_id, structure_change)
+ }
+ case SetIsCommandKeyword(f) => {
+ val old_id = document_id
+ val doc_id = Isabelle.plugin.id()
+ document_versions ::= (doc_id, document.set_command_keyword(f))
+ edit_document(old_id, doc_id, StructureChange(None, Nil, Nil))
+ }
+ case change: Text.Change => {
+ val (doc, structure_change) = document.text_changed(change)
+ val old_id = document_id
+ val doc_id = Isabelle.plugin.id()
+ document_versions ::= (doc_id, doc)
+ edit_document(old_id, doc_id, structure_change)
+ }
+ case command: Command => {
+ //state of command has changed
+ change_receiver ! command
+ }
+ }
+ }
+ }
+
+ def set_document(change_receiver: Actor, path: String) {
+ this.change_receiver = change_receiver
+ this ! ProverEvents.SetIsCommandKeyword(command_decls.contains)
process.ML("()") // FIXME force initial writeln
process.begin_document(document_id0, path)
- document.structural_changes += edit_document
- // FIXME !?
- if (initialized) {
- document.activate()
- activated.event(())
- }
}
- private def edit_document(changes: StructureChange) = Swing.now
+ private def edit_document(old_id: String, document_id: String, changes: StructureChange) = Swing.now
{
- val old_id = document_id
- document_id = Isabelle.plugin.id()
- document_versions += document_id
-
val removes =
for (cmd <- changes.removed_commands) yield {
commands -= cmd.id
if (cmd.state_id != null) states -= cmd.state_id
- (if (cmd.prev == null) document_id0 else cmd.prev.id) -> None
+ (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> None
}
val inserts =
for (cmd <- changes.added_commands) yield {
commands += (cmd.id -> cmd)
process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
- (if (cmd.prev == null) document_id0 else cmd.prev.id) -> Some(cmd.id)
+ (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> Some(cmd.id)
}
process.edit_document(old_id, document_id, removes.reverse ++ inserts)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/utils/LinearSet.scala Thu Mar 19 16:48:29 2009 +0100
@@ -0,0 +1,87 @@
+/* Title: LinearSet.scala
+ Author: Makarius
+
+Sets with canonical linear order, or immutable linked-lists.
+*/
+package isabelle.utils
+
+object LinearSet
+{
+ def empty[A]: LinearSet[A] = new LinearSet[A]
+ def apply[A](elems: A*): LinearSet[A] =
+ (empty[A] /: elems) ((s, elem) => s + elem)
+
+ class Duplicate(s: String) extends Exception(s)
+ class Undefined(s: String) extends Exception(s)
+
+ private def make[A](first: Option[A], last: Option[A], b: Map[A, A]): LinearSet[A] =
+ new LinearSet[A] {
+ override val first_elem = first
+ override val last_elem = last
+ override val body = b
+ }
+}
+
+class LinearSet[A] extends scala.collection.immutable.Set[A]
+{
+ /* representation */
+
+ val first_elem: Option[A] = None
+ val last_elem: Option[A] = None
+ val body: Map[A, A] = Map.empty
+
+
+ /* basic methods */
+
+ def next(elem: A) = body.get(elem)
+ def prev(elem: A) = body.find(_._2 == elem).map(_._1)
+ override def isEmpty: Boolean = !last_elem.isDefined
+ def size: Int = if (isEmpty) 0 else body.size + 1
+
+ def empty[B] = LinearSet.empty[B]
+
+ def contains(elem: A): Boolean =
+ !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem))
+
+ def insert_after(hook: Option[A], elem: A): LinearSet[A] =
+ if (contains(elem)) throw new LinearSet.Duplicate(elem.toString)
+ else hook match {
+ case Some(hook) =>
+ if (!contains(hook)) throw new LinearSet.Undefined(hook.toString)
+ else if (body.isDefinedAt(hook))
+ LinearSet.make(first_elem, last_elem, body - hook + (hook -> elem) + (elem -> body(hook)))
+ else LinearSet.make(first_elem, Some(elem), body + (hook -> elem))
+ case None =>
+ if (isEmpty) LinearSet.make(Some(elem), Some(elem), Map.empty)
+ else LinearSet.make(Some(elem), last_elem, body + (elem -> first_elem.get))
+ }
+
+ def +(elem: A): LinearSet[A] = insert_after(last_elem, elem)
+
+ def delete_after(elem: Option[A]): LinearSet[A] =
+ elem match {
+ case Some(elem) =>
+ if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
+ else if (!body.isDefinedAt(elem)) throw new LinearSet.Undefined(null)
+ else if (body(elem) == last_elem.get) LinearSet.make(first_elem, Some(elem), body - elem)
+ else LinearSet.make(first_elem, last_elem, body - elem - body(elem) + (elem -> body(body(elem))))
+ case None =>
+ if (isEmpty) throw new LinearSet.Undefined(null)
+ else if (size == 1) empty
+ else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get)
+ }
+
+ def -(elem: A): LinearSet[A] =
+ if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
+ else delete_after(body find (p => p._2 == elem) map (p => p._1))
+
+ def elements = new Iterator[A] {
+ private var next_elem = first_elem
+ def hasNext = next_elem.isDefined
+ def next = {
+ val elem = next_elem.get
+ next_elem = if (body.isDefinedAt(elem)) Some(body(elem)) else None
+ elem
+ }
+ }
+}
\ No newline at end of file