# HG changeset patch
# User wenzelm
# Date 1224433942 -7200
# Node ID 3d55eda3d87cdab548e0361ef0b0bccf97a74246
# Parent  883dc8fc3328e641c91ae695045007266cb24841
deactivated tests due to lack of testng installation;

diff -r 883dc8fc3328 -r 3d55eda3d87c src/Tools/jEdit/src/proofdocument/tests/TestProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/tests/TestProofDocument.scala	Sun Oct 19 18:27:30 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,139 +0,0 @@
-package isabelle.proofdocument.tests
-
-import org.testng.annotations._
-import org.testng.Assert._
-  
-import isabelle.proofdocument._
-import isabelle.utils.EventSource
-
-class TextMockup() extends Text {
-  var content = ""
-  val changes = new EventSource[Text.Changed]
-
-  def content(start : Int, stop : Int) = content.substring(start, stop)
-  def length = content.length
-  
-  def change(start : Int, added : String, removed : Int) {
-    content = content.substring(0, start) + added + content.substring(start + removed)
-    changes.fire(new Text.Changed(start, added.length, removed))
-  }
-} 
-
-class ProofDocumentTest(text : Text) extends ProofDocument[String](text) {
-  var start : Token[String] = null
-  var stop : Token[String] = null
-  var removed : Token[String] = null
-
-  def isStartKeyword(s : String) : Boolean = false
-  
-  def tokenChanged(start_ : Token[String], stop_ : Token[String], 
-                   removed_ : Token[String]) {
-    start = start_
-    stop = stop_
-    removed = removed_
-  }
-  
-  override def tokens = super.tokens
-  override def tokens(s : Token[String]) = super.tokens(s)
-  override def tokens(s : Token[String], e : Token[String]) = super.tokens(s, e)
-  
-  def first = firstToken
-  def last = lastToken
-  
-  def checkLinks(first : Token[String], last : Token[String]) {
-    var iter = first
-    var prev : Token[String] = null
-    
-    while(iter != null) {
-      assert(iter.previous == prev)
-      prev = iter
-      iter = iter.next
-    }
-    if (last != null)
-      assert(prev == last)
-  }
-}
-
-class TestProofDocument {
-  private def ranges(ts : Iterator[Token[String]]) =
-    (for (t <- ts) yield (t.start, t.stop)).toList
-  
-  @Test
-  def testParsing() {
-    def check(tokens : String*) = {
-      var content = ""
-      var structure = Nil : List[(Int, Int)]
-    
-      for(tok <- tokens) {
-        if (tok != " ")
-          structure = (content.length, content.length + tok.length) :: structure
-        content = content + tok
-      }
-      
-      val text = new TextMockup()
-      val document = new ProofDocumentTest(text)
-      text.change(0, content, 0)
-      document.checkLinks(document.first, document.last)
-      assertEquals(ranges(document.tokens), structure.reverse)
-    }
-  
-    check("lemma", " " , "fixes", " ", "A", " ", ":", ":", " ", "'a", " ", 
-          "shows", "\"True\"", " ", "using", "`A = A`", "by", "(", "auto", " ", 
-          "simp", " ", "add", ":", "refl", ")")
-  }
-  
-  @Test
-  def testChanging() {
-    val text = new TextMockup()
-    val document = new ProofDocumentTest(text)
-
-    def compare(start : Int, add : String, remove : Int) {
-      val oldDocument = ranges(document.tokens)
-      text.change(start, add, remove)
-      document.checkLinks(document.first, document.last)
-      document.checkLinks(document.removed, null)
-      
-      val offset = remove - add.length
-      val before = if (document.start == null) Nil 
-                   else ranges(document.tokens(document.first, document.start.next))
-      val after = (for(t <- document.tokens(document.stop)) 
-                     yield (t.start + offset, t.stop + offset)).toList
-      val removed = ranges(document.tokens(document.removed))
-      assertEquals((before ++ removed ++ after).length, oldDocument.length, 
-                   "Mismatch on token count")
-      assertEquals(before, oldDocument.take(before.length),
-                   "Tokens before changed part")
-      assertEquals(after, oldDocument.drop(before.length + removed.length),
-                   "Tokens before changed part")
-    
-      val newText = new TextMockup()
-      val newDocument = new ProofDocumentTest(newText)
-      newText.change(0, text.content, 0)
-      newDocument.checkLinks(newDocument.first, newDocument.last)
-
-      assertEquals(ranges(document.tokens), ranges(newDocument.tokens),
-                   "Mismatch on entirely reparsed document")
-    }
-  
-    val s = """lemma fixes a :: nat assumes T: \"A\" shows \"B ==> A\" using `A` by auto"""
-    compare(0, s, text.content.length)
-    compare(0, "(*", 0)
-    compare(text.content.length, "*)", 0)
-    compare(0, "", 2)
-    compare(1, "", 7)
-    
-    compare(0, "test :: 12 34", text.content.length)
-    compare(6, "", 1)
-    compare(6, ":", 0)
-    compare(8, "56", 2)
-    compare(2, "", 4)
-    
-    compare(0, "test  :: 12 34", text.content.length)
-    compare(5, "test 1 2", 0)
-    compare(4, " test 2 3", 0)
-
-    compare(0, "theory Scratch\nimports Main\nbegin\n\nlemma test_x: fixes X :: nat shows \"∃ X. X > 0\" by auto\n\nend", text.content.length)
-    compare(72, "", 11)
-    compare(71, "", 1)
-  }
-}