--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sat May 30 12:11:03 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sat May 30 12:11:40 2009 +0200
@@ -59,6 +59,10 @@
}
}
+ def is_outer(kind: String) =
+ List(Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT,
+ Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING).exists(kind == _)
+
def choose_color(kind : String, styles: Array[SyntaxStyle]) : Color =
styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Sat May 30 12:11:03 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Sat May 30 12:11:40 2009 +0200
@@ -31,28 +31,21 @@
class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
extends AbstractHyperlink(start, end, line, "")
{
- val srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src"),
- new File(Isabelle.system.getenv("ML_SOURCES")))
-
- def find_file(file: File, filename: String): Option[File] =
- {
- if (file.getName == new File(filename).getName) Some(file)
- else if (file.isDirectory) file.listFiles.map(find_file(_, filename)).find(_.isDefined).getOrElse(None)
- else None
+ def subdirs(file: File): List[File] = {
+ val subs = file.listFiles.filter(_.isDirectory).toList
+ subs ::: subs.flatMap(subdirs)
}
- override def click(view: View) = {
- srcs.find(src =>
- find_file(src, ref_file) match {
- case None => false
- case Some(file) =>
- jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
- true})
- match {
- case None => System.err.println("Could not find file " + ref_file)
- case _ =>
- }
- }
+ val srcs = List(new File(Isabelle.system.getenv("ML_SOURCES")))
+ val rec_srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src"))
+
+ override def click(view: View) =
+ (srcs ::: rec_srcs.flatMap(subdirs)).find(new File(_, ref_file).exists) match {
+ case None => System.err.println("Could not find file " + ref_file)
+ case Some(dir) =>
+ val file = new File(dir, ref_file)
+ jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
+ }
}
class IsabelleHyperlinkSource extends HyperlinkSource
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sat May 30 12:11:03 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sat May 30 12:11:40 2009 +0200
@@ -26,6 +26,8 @@
object TheoryView {
+ val MAX_CHANGE_LENGTH = 1500
+
def choose_color(state: Command): Color = {
if (state == null) Color.red
else
@@ -220,8 +222,15 @@
private def commit: Unit = synchronized {
if (col != null) {
- changes = col :: changes
- document_actor ! col
+ 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 new_changes = split_changes(col)
+ changes = new_changes.reverse ::: changes
+ new_changes map (document_actor ! _)
}
col = null
if (col_timer.isRunning())
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sat May 30 12:11:03 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sat May 30 12:11:40 2009 +0200
@@ -175,7 +175,7 @@
tokens match {
case Nil => Nil
case t::ts =>
- val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
+ 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)
}
}
--- a/src/Tools/jEdit/src/prover/Command.scala Sat May 30 12:11:03 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Sat May 30 12:11:40 2009 +0200
@@ -38,7 +38,7 @@
override def toString = name
val name = tokens.head.content
- val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT), 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
@@ -53,10 +53,10 @@
if (st == Command.Status.UNPROCESSED) {
state_results.clear
// delete markup
- markup_root.filter(_.info match {
+ markup_root = markup_root.filter(_.info match {
case RootInfo() | OuterInfo(_) => true
case _ => false
- })
+ }).head
}
_status = st
}
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sat May 30 12:11:03 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Sat May 30 12:11:40 2009 +0200
@@ -14,7 +14,7 @@
import javax.swing.tree._
abstract class MarkupInfo
-case class RootInfo extends 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}
--- a/src/Tools/jEdit/src/prover/Prover.scala Sat May 30 12:11:03 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sat May 30 12:11:40 2009 +0200
@@ -183,25 +183,25 @@
command_change(command)
case XML.Elem(kind, attr, body)
if command != null =>
- // TODO: assuming that begin, end, id are present in attributes
- val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
- val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
- val markup_id = get_attr(attr, Markup.ID).get
- if (kind == Markup.ML_TYPING) {
- val info = body.first.asInstanceOf[XML.Text].content
- command.markup_root += command.markup_node(begin, end, TypeInfo(info))
- } else if (kind == Markup.ML_REF) {
- body match {
- case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
- command.markup_root += command.markup_node(begin, end,
- RefInfo(get_attr(attr, Markup.FILE),
- get_attr(attr, Markup.LINE).map(Integer.parseInt),
- get_attr(attr, Markup.ID),
- get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
- case _ =>
+ val begin = get_attr(attr, Markup.OFFSET).map(_.toInt - 1)
+ val end = get_attr(attr, Markup.END_OFFSET).map(_.toInt - 1)
+ if (begin.isDefined && end.isDefined) {
+ if (kind == Markup.ML_TYPING) {
+ val info = body.first.asInstanceOf[XML.Text].content
+ command.markup_root += command.markup_node(begin.get, end.get, TypeInfo(info))
+ } else if (kind == Markup.ML_REF) {
+ body match {
+ 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.ID),
+ get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
+ case _ =>
+ }
+ } else {
+ command.markup_root += command.markup_node(begin.get, end.get, HighlightInfo(kind))
}
- } else {
- command.markup_root += command.markup_node(begin, end, HighlightInfo(kind))
}
command_change(command)
case XML.Elem(kind, attr, body)
@@ -211,13 +211,12 @@
val begin = get_attr(attr, Markup.OFFSET).map(_.toInt - 1)
val end = get_attr(attr, Markup.END_OFFSET).map(_.toInt - 1)
val markup_id = get_attr(attr, Markup.ID)
- if (!running && begin.isDefined && end.isDefined && markup_id.isDefined)
+ val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
+ if (outer && !running && begin.isDefined && end.isDefined && markup_id.isDefined)
commands.get(markup_id.get).map (cmd => {
cmd.markup_root += cmd.markup_node(begin.get, end.get, OuterInfo(kind))
command_change(cmd)
})
- else
- command_change(command)
case _ =>
//}}}
}