# HG changeset patch
# User wenzelm
# Date 1232404184 -3600
# Node ID 6475bfb4ff99c3725ed391de23852069668dec32
# Parent  920ff05ca3f348dd9c67d545f4a7c15aa888c03f
joined Document with ProofDocument;
misc tuning;

diff -r 920ff05ca3f3 -r 6475bfb4ff99 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Mon Jan 19 21:58:38 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Mon Jan 19 23:29:44 2009 +0100
@@ -32,7 +32,7 @@
     val prover_setup = Isabelle.plugin.prover_setup(buffer)
     if(prover_setup.isDefined){
         val document = prover_setup.get.prover.document
-        val commands = document.commands()
+        val commands = document.commands
         while (!stopped && commands.hasNext) {
           data.root.add(commands.next.root_node.swing_node)
         }
diff -r 920ff05ca3f3 -r 6475bfb4ff99 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Jan 19 21:58:38 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Jan 19 23:29:44 2009 +0100
@@ -1,18 +1,25 @@
 /*
- * Document as list of tokens
+ * Document as list of commands, consisting of lists of tokens
  *
  * @author Johannes Hölzl, TU Munich
+ * @author Makarius
  */
 
 package isabelle.proofdocument
 
 
 import java.util.regex.Pattern
+import isabelle.prover.{Prover, Command}
 
 
+class StructureChange(
+  val beforeChange: Command,
+  val addedCommands: List[Command],
+  val removedCommands: List[Command])
+
 object ProofDocument
 {
-  // Be carefully when changeing this regex. Not only must it handle the 
+  // Be carefully 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
@@ -27,60 +34,59 @@
       "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
       "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
       "[()\\[\\]{}:;]", Pattern.MULTILINE)
+
 }
 
-abstract class ProofDocument(text: Text)
+class ProofDocument(text: Text, prover: Prover)
 {
-  protected var firstToken: Token = null
-  protected var lastToken: Token = null
   private var active = false 
-  
-  text.changes += (e => textChanged(e.start, e.added, e.removed))
-	
   def activate() {
     if (!active) {
       active = true
-      textChanged(0, text.length, 0)
+      text_changed(0, text.length, 0)
     }
   }
+
+  text.changes += (changed => text_changed(changed.start, changed.added, changed.removed))
+
+
+
+  /** token view **/
+
+  protected var firstToken: Token = null
+  protected var lastToken: Token = null
   
-  protected def tokens(start: Token, stop: Token) =
-    new Iterator[Token] {
+  protected def tokens(start: Token, stop: Token) = new Iterator[Token] {
       var current = start
       def hasNext = current != stop && current != null
       def next() = { val save = current ; current = current.next ; save }
     }
-  
-  protected def tokens(start: Token): Iterator[Token] = 
-    tokens(start, null)
-  
-  protected def tokens() : Iterator[Token] =
-    tokens(firstToken, null)
+  protected def tokens(start: Token): Iterator[Token] = tokens(start, null)
+  protected def tokens() : Iterator[Token] = tokens(firstToken, null)
+
 
-  private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
-    val check_start = Token.check_start _
-    val check_stop = Token.check_stop _
-    val scan = Token.scan _
-    if (active == false)
+  private def text_changed(start: Int, addedLen: Int, removedLen: Int)
+  {
+    if (!active)
       return
-        
+
     var beforeChange = 
-      if (check_stop(firstToken, _ < start)) scan(firstToken, _.stop >= start)
+      if (Token.check_stop(firstToken, _ < start)) Token.scan(firstToken, _.stop >= start)
       else null
     
     var firstRemoved = 
       if (beforeChange != null) beforeChange.next
-      else if (check_start(firstToken, _ <= start + removedLen)) firstToken
+      else if (Token.check_start(firstToken, _ <= start + removedLen)) firstToken
       else null 
 
-    var lastRemoved = scan(firstRemoved, _.start > start + removedLen)
+    var lastRemoved = Token.scan(firstRemoved, _.start > start + removedLen)
 
     var shiftToken = 
       if (lastRemoved != null) lastRemoved
-      else if (check_start(firstToken, _ > start)) firstToken
+      else if (Token.check_start(firstToken, _ > start)) firstToken
       else null
     
-    while(shiftToken != null) {
+    while (shiftToken != null) {
       shiftToken.shift(addedLen - removedLen, start)
       shiftToken = shiftToken.next
     }
@@ -96,13 +102,13 @@
     var position = 0 
     while (matcher.find(position) && ! finished) {
       position = matcher.end()
-			val kind = if(isStartKeyword(matcher.group())) {
-        Token.Kind.COMMAND_START
-      } else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*") {
-        Token.Kind.COMMENT
-      } else {
-        Token.Kind.OTHER
-      }
+			val kind =
+        if (prover.is_command_keyword(matcher.group()))
+          Token.Kind.COMMAND_START
+        else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*")
+          Token.Kind.COMMENT
+        else
+          Token.Kind.OTHER
       val newToken = new Token(matcher.start() + matchStart, matcher.end() + matchStart, kind)
 
       if (firstAdded == null)
@@ -113,12 +119,12 @@
       }
       lastAdded = newToken
       
-      while (check_stop(lastRemoved, _ < newToken.stop) &&
+      while (Token.check_stop(lastRemoved, _ < newToken.stop) &&
               lastRemoved.next != null)	
         lastRemoved = lastRemoved.next
 			
       if (newToken.stop >= start + addedLen && 
-            check_stop(lastRemoved, _ == newToken.stop))
+            Token.check_stop(lastRemoved, _ == newToken.stop))
         finished = true
     }
 
@@ -134,8 +140,6 @@
       }
       else {
         firstRemoved = firstRemoved.next
-        if (firstRemoved == null)
-          System.err.println("ERROR")
         assert(firstRemoved != null)
       }
 
@@ -157,8 +161,6 @@
       }
       else {
         lastRemoved = lastRemoved.prev
-        if (lastRemoved == null)
-          System.err.println("ERROR")
         assert(lastRemoved != null)
       }
       
@@ -218,10 +220,140 @@
         afterChange.prev = beforeChange
     }
     
-    tokenChanged(beforeChange, afterChange, firstRemoved)
+    token_changed(beforeChange, afterChange, firstRemoved)
   }
   
-  protected def isStartKeyword(str: String): Boolean
+
   
-  protected def tokenChanged(start: Token, stop: Token, removed: Token) 
+  /** command view **/
+
+  val structural_changes = new EventBus[StructureChange]
+
+  def commands = new Iterator[Command] {
+    var current = firstToken
+    def hasNext = current != null
+    def next() = { val s = current.command ; current = s.last.next ; s }
+  }
+
+  def getContent(cmd: Command) = text.content(cmd.proper_start, cmd.proper_stop)
+
+  def getNextCommandContaining(pos: Int): Command = {
+    for (cmd <- commands) { if (pos < cmd.stop) return cmd }
+    return null
+  }
+
+  private def token_changed(start: Token, stop: Token, removed: Token)
+  {
+    var removedCommands: List[Command] = Nil
+    var first: Command = null
+    var last: Command = null
+
+    for(t <- tokens(removed)) {
+      if (first == null)
+        first = t.command
+      if (t.command != last)
+        removedCommands = t.command :: removedCommands
+      last = t.command
+    }
+
+    var before: Command = null
+    if (!removedCommands.isEmpty) {
+      if (first.first == removed) {
+        if (start == null)
+          before = null
+        else
+          before = start.command
+      }
+      else
+        before = first.prev
+    }
+
+    var addedCommands: List[Command] = Nil
+    var scan: Token = null
+    if (start != null) {
+      val next = start.next
+      if (first != null && first.first != removed) {
+        scan = first.first
+        if (before == null)
+          before = first.prev
+      }
+      else if (next != null && next != stop) {
+        if (next.kind == Token.Kind.COMMAND_START) {
+          before = start.command
+          scan = next
+        }
+        else if (first == null || first.first == removed) {
+          first = start.command
+          removedCommands = first :: removedCommands
+          scan = first.first
+          if (before == null)
+            before = first.prev
+        }
+        else {
+          scan = first.first
+          if (before == null)
+            before = first.prev
+        }
+      }
+    }
+    else
+      scan = firstToken
+
+    var stopScan: Token = null
+    if (stop != null) {
+      if (stop == stop.command.first)
+        stopScan = stop
+      else
+        stopScan = stop.command.last.next
+    }
+    else if (last != null)
+      stopScan = last.last.next
+    else
+      stopScan = null
+
+    var cmdStart: Token = null
+    var cmdStop: Token = null
+    var overrun = false
+    var finished = false
+    while (scan != null && !finished) {
+      if (scan == stopScan) {
+        if (scan.kind == Token.Kind.COMMAND_START)
+          finished = true
+        else
+          overrun = true
+      }
+
+      if (scan.kind == Token.Kind.COMMAND_START && cmdStart != null && !finished) {
+        if (!overrun) {
+          addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
+          cmdStart = scan
+          cmdStop = scan
+        }
+        else
+          finished = true
+      }
+      else if (!finished) {
+        if (cmdStart == null)
+          cmdStart = scan
+        cmdStop = scan
+      }
+      if (overrun && !finished) {
+        if (scan.command != last)
+          removedCommands = scan.command :: removedCommands
+        last = scan.command
+      }
+
+      if (!finished)
+        scan = scan.next
+    }
+
+    if (cmdStart != null)
+      addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
+
+    // relink commands
+    addedCommands = addedCommands.reverse
+    removedCommands = removedCommands.reverse
+
+    structural_changes.event(new StructureChange(before, addedCommands, removedCommands))
+  }
 }
diff -r 920ff05ca3f3 -r 6475bfb4ff99 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Jan 19 21:58:38 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Mon Jan 19 23:29:44 2009 +0100
@@ -11,7 +11,7 @@
 import javax.swing.text.Position
 import javax.swing.tree.DefaultMutableTreeNode
 
-import isabelle.proofdocument.Token
+import isabelle.proofdocument.{Token, ProofDocument}
 import isabelle.jedit.{Isabelle, Plugin}
 import isabelle.XML
 
@@ -29,7 +29,7 @@
 }
 
 
-class Command(val document: Document, val first: Token, val last: Token)
+class Command(val document: ProofDocument, val first: Token, val last: Token)
 {
   val id = Isabelle.plugin.id()
   
diff -r 920ff05ca3f3 -r 6475bfb4ff99 src/Tools/jEdit/src/prover/Document.scala
--- a/src/Tools/jEdit/src/prover/Document.scala	Mon Jan 19 21:58:38 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,158 +0,0 @@
-/*
- * Document as list of commands
- *
- * @author Johannes Hölzl, TU Munich
- */
-
-package isabelle.prover
-
-import isabelle.proofdocument.{ProofDocument, Token, Text}
-
-
-object Document {
-  class StructureChange(val beforeChange : Command,
-                        val addedCommands : List[Command],
-                        val removedCommands : List[Command])
-}
-
-
-class Document(text : Text, val prover : Prover) extends ProofDocument(text)
-{
-  val structural_changes = new EventBus[Document.StructureChange]
-
-  def isStartKeyword(s : String) = prover.command_decls.contains(s)
-
-  def commands() = new Iterator[Command] {
-    var current = firstToken
-    def hasNext() = current != null
-    def next() = { try {val s = current.command ; current = s.last.next ; s}
-    catch { case error : NullPointerException =>
-      System.err.println("NPE!")
-      throw error
-    }
-    }
-  }
-
-  def getContent(cmd : Command) = text.content(cmd.proper_start, cmd.proper_stop)
-
-  def getNextCommandContaining(pos : Int) : Command = {
-    for( cmd <- commands()) { if (pos < cmd.stop) return cmd }
-    return null
-  }
-
-  override def tokenChanged(start : Token, stop : Token, removed : Token)
-  {
-    var removedCommands : List[Command] = Nil
-    var first : Command = null
-    var last : Command = null
-
-    for(t <- tokens(removed)) {
-      if (first == null)
-        first = t.command
-      if (t.command != last)
-        removedCommands = t.command :: removedCommands
-      last = t.command
-    }
-
-    var before : Command = null
-    if (! removedCommands.isEmpty) {
-      if (first.first == removed) {
-        if (start == null)
-          before = null
-        else
-          before = start.command
-      }
-      else
-        before = first.prev
-    }
-
-    var addedCommands : List[Command] = Nil
-    var scan : Token = null
-    if (start != null) {
-      val next = start.next
-      if (first != null && first.first != removed) {
-        scan = first.first
-        if (before == null)
-          before = first.prev
-      }
-      else if (next != null && next != stop) {
-        if (next.kind == Token.Kind.COMMAND_START) {
-          before = start.command
-          scan = next
-        }
-        else if (first == null || first.first == removed) {
-          first = start.command
-          removedCommands = first :: removedCommands
-          scan = first.first
-          if (before == null)
-            before = first.prev
-        }
-        else {
-          scan = first.first
-          if (before == null)
-            before = first.prev
-        }
-      }
-    }
-    else
-      scan = firstToken
-
-    var stopScan : Token = null
-    if (stop != null) {
-      if (stop == stop.command.first)
-        stopScan = stop
-      else
-        stopScan = stop.command.last.next
-    }
-    else if (last != null)
-      stopScan = last.last.next
-    else
-      stopScan = null
-
-    var cmdStart : Token = null
-    var cmdStop : Token = null
-    var overrun = false
-    var finished = false
-    while (scan != null && !finished) {
-      if (scan == stopScan) {
-        if (scan.kind == Token.Kind.COMMAND_START)
-          finished = true
-        else
-          overrun = true
-      }
-
-      if (scan.kind == Token.Kind.COMMAND_START && cmdStart != null && !finished) {
-        if (!overrun) {
-          addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
-          cmdStart = scan
-          cmdStop = scan
-        }
-        else
-          finished = true
-      }
-      else if (!finished) {
-        if (cmdStart == null)
-          cmdStart = scan
-        cmdStop = scan
-      }
-      if (overrun && !finished) {
-        if (scan.command != last)
-          removedCommands = scan.command :: removedCommands
-        last = scan.command
-      }
-
-      if (!finished)
-        scan = scan.next
-    }
-
-    if (cmdStart != null)
-      addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
-
-    // relink commands
-    addedCommands = addedCommands.reverse
-    removedCommands = removedCommands.reverse
-
-    structural_changes.event(
-      new Document.StructureChange(before, addedCommands, removedCommands))
-  }
-}
diff -r 920ff05ca3f3 -r 6475bfb4ff99 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Jan 19 21:58:38 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Jan 19 23:29:44 2009 +0100
@@ -25,6 +25,9 @@
   private var process: Isar = null
   private var commands = new HashMap[String, Command]
 
+
+  /* outer syntax keywords */
+
   val decl_info = new EventBus[(String, String)]
   val command_decls = new HashMap[String, String] {
     override def +=(entry: (String, String)) = {
@@ -32,6 +35,9 @@
       super.+=(entry)
     }
   }
+  def is_command_keyword(s: String): Boolean = command_decls.contains(s)
+
+
   val keyword_decls = new HashSet[String] {
     override def +=(name: String) = {
       decl_info.event(name, OuterKeyword.MINOR)
@@ -54,7 +60,7 @@
   val activated = new EventBus[Unit]
   val command_info = new EventBus[Command]
   val output_info = new EventBus[String]
-  var document: Document = null
+  var document: ProofDocument = null
 
 
   def command_change(c: Command) = Swing.now { command_info.event(c) }
@@ -97,7 +103,7 @@
                       st.status = Command.Status.FAILED
                       command_change(st)
                     case XML.Elem(Markup.DISPOSED, _, _) =>
-                      document.prover.commands.removeKey(st.id)
+                      commands.removeKey(st.id)
                       st.status = Command.Status.REMOVED
                       command_change(st)
 
@@ -163,7 +169,7 @@
   }
 
   def set_document(text: Text, path: String) {
-    this.document = new Document(text, this)
+    this.document = new ProofDocument(text, this)
     process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
 
     document.structural_changes += (changes => {