--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 21:20:22 2009 +0200
@@ -71,9 +71,9 @@
class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker {
override def markTokens(prev: TokenMarker.LineContext,
- handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
+ handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
val previous = prev.asInstanceOf[IndexLineContext]
- val line = if(prev == null) 0 else previous.line + 1
+ val line = if (prev == null) 0 else previous.line + 1
val context = new IndexLineContext(line, previous)
val start = buffer.getLineStartOffset(line)
val stop = start + line_segment.count
@@ -85,15 +85,18 @@
var next_x = start
for {
- command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop))
+ command <- document.commands.
+ dropWhile(_.stop(document) <= from(start)).
+ takeWhile(_.start(document) < from(stop))
markup <- command.highlight_node.flatten
- if(to(markup.abs_stop(document)) > start)
- if(to(markup.abs_start(document)) < stop)
+ if (to(markup.abs_stop(document)) > start)
+ if (to(markup.abs_start(document)) < stop)
byte = DynamicTokenMarker.choose_byte(markup.info.toString)
token_start = to(markup.abs_start(document)) - start max 0
- token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
- (start - to(markup.abs_start(document)) max 0) -
- (to(markup.abs_stop(document)) - stop max 0)
+ token_length =
+ to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
+ (start - to(markup.abs_start(document)) max 0) -
+ (to(markup.abs_stop(document)) - stop max 0)
} {
if (start + token_start > next_x)
handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Tue Jun 02 21:20:22 2009 +0200
@@ -23,7 +23,7 @@
class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
extends AbstractHyperlink(start, end, line, "")
{
- override def click(view: View) = {
+ override def click(view: View) {
view.getTextArea.moveCaretPosition(ref_offset)
}
}
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jun 02 21:20:22 2009 +0200
@@ -40,9 +40,11 @@
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)
+ if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length)
+ else path)
theory_view.activate
- prover ! new isabelle.proofdocument.Text.Change(Isabelle.plugin.id(), 0,buffer.getText(0, buffer.getLength),0)
+ prover ! new isabelle.proofdocument.Text.Change(
+ Isabelle.plugin.id(), 0, buffer.getText(0, buffer.getLength), 0)
//register output-view
prover.output_info += (text =>
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 21:20:22 2009 +0200
@@ -9,6 +9,7 @@
package isabelle.jedit
import scala.actors.Actor
+import scala.actors.Actor._
import isabelle.proofdocument.Text
import isabelle.prover.{Prover, Command}
@@ -44,7 +45,7 @@
class TheoryView (text_area: JEditTextArea, document_actor: Actor)
extends TextAreaExtension with BufferListener {
- def id() = Isabelle.plugin.id();
+ def id() = Isabelle.plugin.id()
private val buffer = text_area.getBuffer
private val prover = Isabelle.prover_setup(buffer).get.prover
@@ -76,14 +77,14 @@
}
}
- def activate() = {
+ def activate() {
text_area.addCaretListener(selected_state_controller)
text_area.addLeftOfScrollBar(phase_overview)
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
}
- def deactivate() = {
+ def deactivate() {
text_area.getPainter.removeExtension(this)
text_area.removeLeftOfScrollBar(phase_overview)
text_area.removeCaretListener(selected_state_controller)
@@ -94,10 +95,10 @@
val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
- val change_receiver = scala.actors.Actor.actor {
- scala.actors.Actor.loop {
- scala.actors.Actor.react {
- case _ => {
+ val change_receiver = actor {
+ loop {
+ react {
+ case _ => { // FIXME potentially blocking within loop/react!?!?!?!
Swing.now {
repaint_delay.delay_or_ignore()
phase_overview.repaint_delay.delay_or_ignore()
@@ -111,7 +112,8 @@
changes match {
case Nil => pos
case Text.Change(id, start, added, removed) :: rest_changes => {
- val shifted = if (start <= pos)
+ val shifted =
+ if (start <= pos)
if (pos < start + added.length) start
else pos - added.length + removed
else pos
@@ -223,10 +225,10 @@
private def commit: Unit = synchronized {
if (col != null) {
def split_changes(c: Text.Change): List[Text.Change] = {
- val MCL = TheoryView.MAX_CHANGE_LENGTH
- if (c.added.length <= MCL) List(c)
- else Text.Change(c.id, c.start, c.added.substring(0, MCL), c.removed) ::
- split_changes(new Text.Change(id(), c.start + MCL, c.added.substring(MCL), c.removed))
+ val MAX = TheoryView.MAX_CHANGE_LENGTH
+ if (c.added.length <= MAX) List(c)
+ else Text.Change(c.id, c.start, c.added.substring(0, MAX), c.removed) ::
+ split_changes(new Text.Change(id(), c.start + MAX, c.added.substring(MAX), c.removed))
}
val new_changes = split_changes(col)
changes = new_changes.reverse ::: changes
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 21:20:22 2009 +0200
@@ -22,7 +22,7 @@
object ProofDocument
{
- // Be carefully when changing this regex. Not only must it handle the
+ // Be careful when changing this regex. Not only must it handle the
// spurious end of a token but also:
// Bug ID: 5050507 Pattern.matches throws StackOverflow Error
// http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
@@ -39,16 +39,18 @@
"[()\\[\\]{}:;]", Pattern.MULTILINE)
val empty =
- new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), LinearSet(), Map(), LinearSet(), false, _ => false)
+ new ProofDocument(isabelle.jedit.Isabelle.plugin.id(),
+ LinearSet(), Map(), LinearSet(), false, _ => false)
}
-class ProofDocument(val id: String,
- val tokens: LinearSet[Token],
- val token_start: Map[Token, Int],
- val commands: LinearSet[Command],
- val active: Boolean,
- is_command_keyword: String => Boolean)
+class ProofDocument(
+ val id: String,
+ val tokens: LinearSet[Token],
+ val token_start: Map[Token, Int],
+ val commands: LinearSet[Command],
+ val active: Boolean,
+ is_command_keyword: String => Boolean)
{
def mark_active: ProofDocument =
@@ -61,7 +63,7 @@
def set_command_keyword(f: String => Boolean): ProofDocument =
new ProofDocument(id, tokens, token_start, commands, active, f)
- def content = Token.string_from_tokens(List() ++ tokens, token_start)
+ def content = Token.string_from_tokens(Nil ++ tokens, token_start)
/** token view **/
def text_changed(change: Text.Change): (ProofDocument, StructureChange) =
@@ -70,11 +72,12 @@
var start: Map[Token, Int] = token_start
def stop(t: Token) = start(t) + t.length
// split old token lists
- val tokens = List() ++ this.tokens
+ val tokens = Nil ++ this.tokens
val (begin, remaining) = tokens.span(stop(_) < change.start)
val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed)
// update indices
- start = end.foldLeft (start) ((s, t) => s + (t -> (s(t) + change.added.length - change.removed)))
+ start = end.foldLeft(start)((s, t) =>
+ s + (t -> (s(t) + change.added.length - change.removed)))
val split_begin = removed.takeWhile(start(_) < change.start).
map (t => {
@@ -85,8 +88,8 @@
val split_end = removed.dropWhile(stop(_) < change.start + change.removed).
map (t => {
- val split_tok = new Token(t.content.substring(change.start + change.removed - start(t)),
- t.kind)
+ val split_tok =
+ new Token(t.content.substring(change.start + change.removed - start(t)), t.kind)
start += (split_tok -> start(t))
split_tok
})
@@ -98,13 +101,13 @@
val ins = new Token(change.added, Token.Kind.OTHER)
start += (ins -> change.start)
- var invalid_tokens = split_begin :::
- ins :: split_end ::: end
- var new_tokens = Nil: List[Token]
- var old_suffix = Nil: List[Token]
+ var invalid_tokens = split_begin ::: ins :: split_end ::: end
+ var new_tokens: List[Token] = Nil
+ var old_suffix: List[Token] = Nil
val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
- val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
+ val matcher =
+ ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
while (matcher.find() && invalid_tokens != Nil) {
val kind =
@@ -120,8 +123,9 @@
invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
invalid_tokens match {
- case t::ts => if(start(t) == start(new_token) &&
- start(t) > change.start + change.added.length) {
+ case t :: ts =>
+ if (start(t) == start(new_token) &&
+ start(t) > change.start + change.added.length) {
old_suffix = ts
invalid_tokens = Nil
}
@@ -131,13 +135,10 @@
val insert = new_tokens.reverse
val new_token_list = begin ::: insert ::: old_suffix
val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
- token_changed(change.id,
- begin.lastOption,
- insert,
- old_suffix.firstOption,
- new_tokenset,
- start)
+ token_changed(change.id, begin.lastOption, insert,
+ old_suffix.firstOption, new_tokenset, start)
}
+
/** command view **/
@@ -146,12 +147,13 @@
return null
}
- private def token_changed(new_id: String,
- before_change: Option[Token],
- inserted_tokens: List[Token],
- after_change: Option[Token],
- new_tokenset: LinearSet[Token],
- new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
+ private def token_changed(
+ new_id: String,
+ before_change: Option[Token],
+ inserted_tokens: List[Token],
+ after_change: Option[Token],
+ new_tokenset: LinearSet[Token],
+ new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
{
val cmd_first_changed =
if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get))
@@ -174,16 +176,18 @@
def tokens_to_commands(tokens: List[Token]): List[Command]= {
tokens match {
case Nil => Nil
- case t::ts =>
- val (cmd,rest) = ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
- new Command(t::cmd, new_token_start) :: tokens_to_commands (rest)
+ case t :: ts =>
+ val (cmd, rest) =
+ ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
+ new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest)
}
}
val split_begin_tokens =
if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil
else {
- cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) ::: List(before_change.get)
+ cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) :::
+ List(before_change.get)
}
val split_end_tokens =
if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil
@@ -191,7 +195,8 @@
cmd_last_changed.get.tokens.dropWhile(_ != after_change.get)
}
- val rescanning_tokens = split_begin_tokens ::: inserted_tokens ::: split_end_tokens
+ val rescanning_tokens =
+ split_begin_tokens ::: inserted_tokens ::: split_end_tokens
val inserted_commands = tokens_to_commands(rescanning_tokens)
val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList)
@@ -200,7 +205,8 @@
insert_after(cmd_before_change, inserted_commands)
val doc =
- new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword)
+ new ProofDocument(new_id, new_tokenset, new_token_start,
+ new_commandset, active, is_command_keyword)
return (doc, change)
}
}
--- a/src/Tools/jEdit/src/prover/Command.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Tue Jun 02 21:20:22 2009 +0200
@@ -38,7 +38,7 @@
override def toString = name
val name = tokens.head.content
- val content:String = Token.string_from_tokens(tokens, starts)
+ val content: String = Token.string_from_tokens(tokens, starts)
def start(doc: ProofDocument) = doc.token_start(tokens.first)
def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
@@ -81,8 +81,8 @@
/* markup */
val empty_root_node =
- new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil,
- id, content, RootInfo())
+ new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
+ Nil, id, content, RootInfo())
var markup_root = empty_root_node
@@ -96,19 +96,20 @@
def markup_node(begin: Int, end: Int, info: MarkupInfo) =
new MarkupNode(this, begin, end, Nil, id,
- if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??",
- info)
+ if (end <= content.length && begin >= 0) content.substring(begin, end)
+ else "wrong indices??",
+ info)
def type_at(pos: Int): String = {
- val types = markup_root.filter(_.info match {case TypeInfo(_) => true case _ => false})
+ val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
types.flatten(_.flatten).
find(t => t.start <= pos && t.stop > pos).
- map(t => "\"" + t.content + "\" : " + (t.info match {case TypeInfo(i) => i case _ => ""})).
+ map(t => "\"" + t.content + "\" : " + (t.info match { case TypeInfo(i) => i case _ => "" })).
getOrElse(null)
}
def ref_at(pos: Int): Option[MarkupNode] =
- markup_root.filter(_.info match {case RefInfo(_,_,_,_) => true case _ => false}).
+ markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
flatten(_.flatten).
find(t => t.start <= pos && t.stop > pos)
}
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 21:20:22 2009 +0200
@@ -15,31 +15,35 @@
abstract class MarkupInfo
case class RootInfo() extends MarkupInfo
-case class OuterInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
-case class HighlightInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
-case class TypeInfo(type_kind: String) extends MarkupInfo {override def toString = type_kind}
+case class OuterInfo(highlight: String) extends
+ MarkupInfo { override def toString = highlight }
+case class HighlightInfo(highlight: String) extends
+ MarkupInfo { override def toString = highlight }
+case class TypeInfo(type_kind: String) extends
+ MarkupInfo { override def toString = type_kind }
case class RefInfo(file: Option[String], line: Option[Int],
- command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
- override def toString = (file, line, command_id, offset).toString
-}
+ command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
+ override def toString = (file, line, command_id, offset).toString
+ }
object MarkupNode {
- def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = {
+ def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument)
+ : DefaultMutableTreeNode = {
implicit def int2pos(offset: Int): Position =
- new Position { def getOffset = offset; override def toString = offset.toString}
+ new Position { def getOffset = offset; override def toString = offset.toString }
object RelativeAsset extends IAsset {
- override def getIcon : Icon = null
- override def getShortString : String = node.content
- override def getLongString : String = node.info.toString
- override def getName : String = node.id
- override def setName (name : String) = ()
- override def setStart(start : Position) = ()
- override def getStart : Position = node.abs_start(doc)
- override def setEnd(end : Position) = ()
- override def getEnd : Position = node.abs_stop(doc)
+ override def getIcon: Icon = null
+ override def getShortString: String = node.content
+ override def getLongString: String = node.info.toString
+ override def getName: String = node.id
+ override def setName(name: String) = ()
+ override def setStart(start: Position) = ()
+ override def getStart: Position = node.abs_start(doc)
+ override def setEnd(end: Position) = ()
+ override def getEnd: Position = node.abs_stop(doc)
override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
}
@@ -47,11 +51,11 @@
}
}
-class MarkupNode (val base: Command, val start: Int, val stop: Int,
- val children: List[MarkupNode],
- val id: String, val content: String, val info: MarkupInfo) {
-
- def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
+class MarkupNode(val base: Command, val start: Int, val stop: Int,
+ val children: List[MarkupNode],
+ val id: String, val content: String, val info: MarkupInfo)
+{
+ def swing_node(doc: ProofDocument): DefaultMutableTreeNode = {
val node = MarkupNode.markup2default_node (this, base, doc)
children.map(node add _.swing_node(doc))
node
@@ -63,11 +67,12 @@
def set_children(newchildren: List[MarkupNode]): MarkupNode =
new MarkupNode(base, start, stop, newchildren, id, content, info)
- def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start))
+ def add(child: MarkupNode) =
+ set_children ((child :: children) sort ((a, b) => a.start < b.start))
- def remove(nodes : List[MarkupNode]) = set_children(children diff nodes)
+ def remove(nodes: List[MarkupNode]) = set_children(children diff nodes)
- def dfs : List[MarkupNode] = {
+ def dfs: List[MarkupNode] = {
var all = Nil : List[MarkupNode]
for (child <- children)
all = child.dfs ::: all
@@ -86,41 +91,48 @@
else {
val filled_gaps = for {
child <- children
- markups = if (next_x < child.start) {
- new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten
- } else child.flatten
+ markups =
+ if (next_x < child.start) {
+ new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten
+ } else child.flatten
update = (next_x = child.stop)
markup <- markups
} yield markup
- if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info)
+ if (next_x < stop)
+ filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info)
else filled_gaps
}
}
- def filter(p: (MarkupNode => Boolean)): List[MarkupNode] = {
+ def filter(p: MarkupNode => Boolean): List[MarkupNode] = {
val filtered = children.flatMap(_.filter(p))
if (p(this)) List(this set_children(filtered))
else filtered
}
- def +(new_child : MarkupNode) : MarkupNode = {
+ 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)
+ 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
+ // 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 {
- error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.info.toString
- + "(" +new_child.start + ", "+ new_child.stop + ")")
+ error("ignored nonfitting markup " + new_child.id + new_child.content +
+ new_child.info.toString + "(" +new_child.start + ", "+ new_child.stop + ")")
}
}
// does this fit into node?
- def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop
+ def fitting_into(node: MarkupNode) = node.start <= this.start && node.stop >= this.stop
- override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
+ override def toString =
+ "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Jun 02 21:20:22 2009 +0200
@@ -88,20 +88,20 @@
if (map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
}
*/
- decl_info += (k_v => _completions += k_v._1)
+ decl_info += (p => _completions += p._1)
/* event handling */
val activated = new EventBus[Unit]
val output_info = new EventBus[String]
- var change_receiver = null: Actor
+ var change_receiver: Actor = null
private def handle_result(result: IsabelleProcess.Result)
{
// helper-function (move to XML?)
def get_attr(attributes: List[(String, String)], attr: String): Option[String] =
- attributes.find(kv => kv._1 == attr).map(_._2)
+ attributes.find(p => p._1 == attr).map(_._2)
def command_change(c: Command) = this ! c
val (running, command) =
@@ -149,7 +149,7 @@
// document edits
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
- if document_versions.exists(dv => doc_id == dv.id) =>
+ if document_versions.exists(_.id == doc_id) =>
output_info.event(result.toString)
for {
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
@@ -194,9 +194,9 @@
case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
command.markup_root += command.markup_node(begin.get, end.get,
RefInfo(get_attr(attr, Markup.FILE),
- get_attr(attr, Markup.LINE).map(Integer.parseInt),
+ get_attr(attr, Markup.LINE).map(_.toInt),
get_attr(attr, Markup.ID),
- get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
+ get_attr(attr, Markup.OFFSET).map(_.toInt)))
case _ =>
}
} else {