# 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 _ =>
                   //}}}
                 }