src/Tools/jEdit/src/proofdocument/ProofDocument.scala
author immler@in.tum.de
Thu Apr 16 13:38:03 2009 +0200 (2009-04-16)
changeset 34550 171c8c6e5707
parent 34544 56217d219e27
child 34551 bd2b8fde9e25
permissions -rw-r--r--
prepared proofdocument for only needed changes
wenzelm@34407
     1
/*
wenzelm@34485
     2
 * Document as list of commands, consisting of lists of tokens
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Johannes Hölzl, TU Munich
immler@34532
     5
 * @author Fabian Immler, TU Munich
wenzelm@34485
     6
 * @author Makarius
wenzelm@34407
     7
 */
wenzelm@34407
     8
wenzelm@34318
     9
package isabelle.proofdocument
wenzelm@34318
    10
immler@34526
    11
import scala.collection.mutable.ListBuffer
immler@34532
    12
import scala.actors.Actor
immler@34532
    13
import scala.actors.Actor._
wenzelm@34318
    14
import java.util.regex.Pattern
wenzelm@34485
    15
import isabelle.prover.{Prover, Command}
immler@34531
    16
import isabelle.utils.LinearSet
wenzelm@34318
    17
wenzelm@34494
    18
case class StructureChange(
immler@34526
    19
  val before_change: Option[Command],
wenzelm@34494
    20
  val added_commands: List[Command],
wenzelm@34494
    21
  val removed_commands: List[Command])
wenzelm@34485
    22
wenzelm@34483
    23
object ProofDocument
wenzelm@34483
    24
{
wenzelm@34485
    25
  // Be carefully when changing this regex. Not only must it handle the 
wenzelm@34318
    26
  // spurious end of a token but also:  
wenzelm@34318
    27
  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
wenzelm@34318
    28
  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
wenzelm@34318
    29
  
wenzelm@34483
    30
  val token_pattern = 
wenzelm@34318
    31
    Pattern.compile(
wenzelm@34318
    32
      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
wenzelm@34318
    33
      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
wenzelm@34318
    34
      "(\\?'?|')[A-Za-z_0-9.]*|" + 
wenzelm@34318
    35
      "[A-Za-z_0-9.]+|" + 
wenzelm@34318
    36
      "[!#$%&*+-/<=>?@^_|~]+|" +
wenzelm@34318
    37
      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
wenzelm@34318
    38
      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
wenzelm@34318
    39
      "[()\\[\\]{}:;]", Pattern.MULTILINE)
wenzelm@34485
    40
immler@34544
    41
 val empty =
immler@34544
    42
  new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), LinearSet.empty, LinearSet.empty, false, _ => false)
immler@34538
    43
wenzelm@34318
    44
}
wenzelm@34318
    45
immler@34544
    46
class ProofDocument(val id: String,
immler@34544
    47
                    val tokens: LinearSet[Token],
immler@34532
    48
                    val commands: LinearSet[Command],
immler@34532
    49
                    val active: Boolean,
immler@34538
    50
                    is_command_keyword: String => Boolean)
wenzelm@34483
    51
{
wenzelm@34485
    52
immler@34544
    53
  def mark_active: ProofDocument =
immler@34544
    54
    new ProofDocument(id, tokens, commands, true, is_command_keyword)
immler@34538
    55
  def activate: (ProofDocument, StructureChange) = {
immler@34544
    56
    val (doc, change) =
immler@34544
    57
      text_changed(new Text.Change(isabelle.jedit.Isabelle.plugin.id(), 0, content, content.length))
immler@34538
    58
    return (doc.mark_active, change)
wenzelm@34456
    59
  }
immler@34532
    60
  def set_command_keyword(f: String => Boolean): ProofDocument =
immler@34544
    61
    new ProofDocument(id, tokens, commands, active, f)
wenzelm@34485
    62
immler@34531
    63
  def content = Token.string_from_tokens(List() ++ tokens)
wenzelm@34485
    64
  /** token view **/
wenzelm@34485
    65
immler@34538
    66
  def text_changed(change: Text.Change): (ProofDocument, StructureChange) =
wenzelm@34485
    67
  {
immler@34531
    68
    val tokens = List() ++ this.tokens
immler@34526
    69
    val (begin, remaining) = tokens.span(_.stop < change.start)
immler@34531
    70
    val (removed, end_unshifted) = remaining.span(_.start <= change.start + change.removed)
immler@34531
    71
    val end = for (t <- end_unshifted) yield t.shift(change.added.length - change.removed)
wenzelm@34485
    72
immler@34526
    73
    val split_begin = removed.takeWhile(_.start < change.start).
immler@34526
    74
      map (t => new Token(t.start,
immler@34526
    75
                          t.content.substring(0, change.start - t.start),
immler@34526
    76
                          t.kind))
immler@34526
    77
    val split_end = removed.dropWhile(_.stop < change.start + change.removed).
immler@34526
    78
      map (t => new Token(change.start + change.added.length,
immler@34526
    79
                          t.content.substring(change.start + change.removed - t.start),
immler@34526
    80
                          t.kind))
wenzelm@34318
    81
immler@34526
    82
    var invalid_tokens =  split_begin :::
immler@34526
    83
      new Token(change.start, change.added, Token.Kind.OTHER) :: split_end ::: end
immler@34526
    84
    var new_tokens = Nil: List[Token]
immler@34526
    85
    var old_suffix = Nil: List[Token]
wenzelm@34318
    86
immler@34526
    87
    val match_start = invalid_tokens.first.start
immler@34526
    88
    val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens))
immler@34526
    89
immler@34526
    90
    while (matcher.find() && invalid_tokens != Nil) {
wenzelm@34485
    91
			val kind =
wenzelm@34505
    92
        if (is_command_keyword(matcher.group))
wenzelm@34485
    93
          Token.Kind.COMMAND_START
wenzelm@34494
    94
        else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
wenzelm@34485
    95
          Token.Kind.COMMENT
wenzelm@34485
    96
        else
wenzelm@34485
    97
          Token.Kind.OTHER
immler@34526
    98
      val new_token = new Token(match_start + matcher.start, matcher.group, kind)
immler@34526
    99
      new_tokens ::= new_token
wenzelm@34318
   100
immler@34526
   101
      invalid_tokens = invalid_tokens dropWhile (_.stop < new_token.stop)
immler@34526
   102
      invalid_tokens match {
immler@34526
   103
        case t::ts => if(t.start == new_token.start &&
immler@34526
   104
                         t.start > change.start + change.added.length) {
immler@34526
   105
          old_suffix = ts
immler@34526
   106
          invalid_tokens = Nil
immler@34526
   107
        }
immler@34526
   108
        case _ =>
wenzelm@34318
   109
      }
wenzelm@34318
   110
    }
immler@34526
   111
    val insert = new_tokens.reverse
immler@34544
   112
    val new_token_list = begin ::: insert ::: old_suffix
immler@34544
   113
    token_changed(change.id,
immler@34550
   114
                  begin.lastOption,
immler@34526
   115
                  insert,
immler@34526
   116
                  removed,
immler@34550
   117
                  old_suffix.firstOption,
immler@34544
   118
                  new_token_list)
wenzelm@34318
   119
  }
wenzelm@34318
   120
  
wenzelm@34485
   121
  /** command view **/
wenzelm@34485
   122
wenzelm@34496
   123
  def find_command_at(pos: Int): Command = {
wenzelm@34485
   124
    for (cmd <- commands) { if (pos < cmd.stop) return cmd }
wenzelm@34485
   125
    return null
wenzelm@34485
   126
  }
wenzelm@34485
   127
immler@34544
   128
  private def token_changed(new_id: String,
immler@34550
   129
                            before_change: Option[Token],
immler@34526
   130
                            inserted_tokens: List[Token],
immler@34526
   131
                            removed_tokens: List[Token],
immler@34550
   132
                            after_change: Option[Token],
immler@34544
   133
                            new_token_list: List[Token]): (ProofDocument, StructureChange) =
wenzelm@34485
   134
  {
immler@34544
   135
    val commands = List[Command]() ++ this.commands
immler@34544
   136
immler@34544
   137
    // calculate removed commands
immler@34544
   138
    val first_removed = removed_tokens.firstOption
immler@34544
   139
    val last_removed = removed_tokens.lastOption
immler@34544
   140
immler@34526
   141
    val (begin, remaining) =
immler@34544
   142
      first_removed match {
immler@34544
   143
        case None => (Nil: List[Command], commands)
immler@34544
   144
        case Some(fr) => commands.break(_.tokens.contains(fr))
immler@34526
   145
      }
immler@34550
   146
    val removed_commands: List[Command]=
immler@34544
   147
      last_removed match {
immler@34544
   148
        case None => Nil
immler@34544
   149
        case Some(lr) =>
immler@34544
   150
          remaining.takeWhile(!_.tokens.contains(lr)) ++
immler@34544
   151
          (remaining.find(_.tokens.contains(lr)) match {
immler@34544
   152
            case None => Nil
immler@34544
   153
            case Some(x) => List(x)
immler@34544
   154
          })
wenzelm@34485
   155
      }
wenzelm@34485
   156
immler@34526
   157
    def tokens_to_commands(tokens: List[Token]): List[Command]= {
immler@34526
   158
      tokens match {
immler@34526
   159
        case Nil => Nil
immler@34526
   160
        case t::ts =>
immler@34526
   161
          val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
immler@34526
   162
          new Command(t::cmd) :: tokens_to_commands (rest)
wenzelm@34485
   163
      }
wenzelm@34485
   164
    }
wenzelm@34485
   165
immler@34544
   166
    // calculate inserted commands
immler@34544
   167
    val new_commands = tokens_to_commands(new_token_list)
immler@34544
   168
    val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
immler@34544
   169
    val new_commandset = (LinearSet() ++ (new_commands)).asInstanceOf[LinearSet[Command]]
immler@34550
   170
    // drop known commands from the beginning
immler@34550
   171
    val first_changed = before_change match {
immler@34550
   172
      case None => new_tokenset.first_elem
immler@34550
   173
      case Some(bc) => new_tokenset.next(bc)
immler@34550
   174
    }
immler@34550
   175
    val changed_commands = first_changed match {
immler@34550
   176
      case None => Nil
immler@34550
   177
      case Some(fc) => new_commands.dropWhile(!_.tokens.contains(fc))
immler@34550
   178
    }
immler@34550
   179
    val inserted_commands = after_change match {
immler@34550
   180
      case None => changed_commands
immler@34550
   181
      case Some(ac) => changed_commands.takeWhile(!_.tokens.contains(ac))
immler@34550
   182
    }
immler@34550
   183
    //val change = new StructureChange(new_commands.find(_.tokens.contains(before_change)),
immler@34550
   184
    //                                 inserted_commands, removed_commands)
immler@34550
   185
    // TODO: revert to upper change, when commands and tokens are ok
immler@34550
   186
    val change = new StructureChange(None, List() ++ new_commandset, commands)
immler@34550
   187
    // build new document
immler@34544
   188
    val doc =
immler@34544
   189
      new ProofDocument(new_id, new_tokenset, new_commandset, active, is_command_keyword)
immler@34538
   190
    return (doc, change)
wenzelm@34485
   191
  }
wenzelm@34318
   192
}