# HG changeset patch # User wenzelm # Date 1243678300 -7200 # Node ID aaa147cd92f911c273c1d7353ae8d4ca8973b880 # Parent f5c3ad245539efd7db0f6c4d3533ecdb2d4d5f44# Parent 014f67650212da12fee21458c5e7d8d3a3d9c919 merged diff -r 014f67650212 -r aaa147cd92f9 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- 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 diff -r 014f67650212 -r aaa147cd92f9 src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala --- 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 diff -r 014f67650212 -r aaa147cd92f9 src/Tools/jEdit/src/jedit/TheoryView.scala --- 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()) diff -r 014f67650212 -r aaa147cd92f9 src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- 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) } } diff -r 014f67650212 -r aaa147cd92f9 src/Tools/jEdit/src/prover/Command.scala --- 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 } diff -r 014f67650212 -r aaa147cd92f9 src/Tools/jEdit/src/prover/MarkupNode.scala --- 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} diff -r 014f67650212 -r aaa147cd92f9 src/Tools/jEdit/src/prover/Prover.scala --- 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 _ => //}}} }