src/Tools/jEdit/src/proofdocument/ProofDocument.scala
author immler@in.tum.de
Wed Apr 22 17:35:49 2009 +0200 (2009-04-22)
changeset 34554 7dc6c231da40
parent 34551 bd2b8fde9e25
child 34575 70d11544685f
permissions -rw-r--r--
abs. stops, markup nodes depend on doc-version;
fixed missing positions in ProofDocument.text_changed;
relink only changed commands in ProofDocument.token_changed
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@34551
    42
  new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), LinearSet(), Map(), LinearSet(), 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@34551
    48
                    val token_start: Map[Token, Int],
immler@34532
    49
                    val commands: LinearSet[Command],
immler@34532
    50
                    val active: Boolean,
immler@34538
    51
                    is_command_keyword: String => Boolean)
wenzelm@34483
    52
{
wenzelm@34485
    53
immler@34544
    54
  def mark_active: ProofDocument =
immler@34551
    55
    new ProofDocument(id, tokens, token_start, commands, true, is_command_keyword)
immler@34538
    56
  def activate: (ProofDocument, StructureChange) = {
immler@34544
    57
    val (doc, change) =
immler@34544
    58
      text_changed(new Text.Change(isabelle.jedit.Isabelle.plugin.id(), 0, content, content.length))
immler@34538
    59
    return (doc.mark_active, change)
wenzelm@34456
    60
  }
immler@34532
    61
  def set_command_keyword(f: String => Boolean): ProofDocument =
immler@34551
    62
    new ProofDocument(id, tokens, token_start, commands, active, f)
wenzelm@34485
    63
immler@34551
    64
  def content = Token.string_from_tokens(List() ++ tokens, token_start)
wenzelm@34485
    65
  /** token view **/
wenzelm@34485
    66
immler@34538
    67
  def text_changed(change: Text.Change): (ProofDocument, StructureChange) =
wenzelm@34485
    68
  {
immler@34551
    69
    //indices of tokens
immler@34551
    70
    var start: Map[Token, Int] = token_start
immler@34551
    71
    def stop(t: Token) = start(t) + t.length
immler@34551
    72
    // split old token lists
immler@34531
    73
    val tokens = List() ++ this.tokens
immler@34551
    74
    val (begin, remaining) = tokens.span(stop(_) < change.start)
immler@34551
    75
    val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed)
immler@34551
    76
    // update indices
immler@34551
    77
    start = end.foldLeft (start) ((s, t) => s + (t -> (s(t) + change.added.length - change.removed)))
wenzelm@34485
    78
immler@34551
    79
    val split_begin = removed.takeWhile(start(_) < change.start).
immler@34554
    80
      map (t => {
immler@34554
    81
          val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
immler@34554
    82
          start += (split_tok -> start(t))
immler@34554
    83
          split_tok
immler@34554
    84
        })
immler@34554
    85
immler@34551
    86
    val split_end = removed.dropWhile(stop(_) < change.start + change.removed).
immler@34554
    87
      map (t => {
immler@34554
    88
          val split_tok = new Token(t.content.substring(change.start + change.removed - start(t)),
immler@34554
    89
                          t.kind)
immler@34554
    90
          start += (split_tok -> start(t))
immler@34554
    91
          split_tok
immler@34554
    92
        })
immler@34551
    93
    // update indices
immler@34554
    94
    start = removed.foldLeft (start) ((s, t) => s - t)
immler@34554
    95
    start = split_end.foldLeft (start) ((s, t) =>
immler@34554
    96
    s + (t -> (change.start + change.added.length)))
wenzelm@34318
    97
immler@34551
    98
    val ins = new Token(change.added, Token.Kind.OTHER)
immler@34551
    99
    start += (ins -> change.start)
immler@34551
   100
    
immler@34526
   101
    var invalid_tokens =  split_begin :::
immler@34551
   102
       ins :: split_end ::: end
immler@34526
   103
    var new_tokens = Nil: List[Token]
immler@34526
   104
    var old_suffix = Nil: List[Token]
wenzelm@34318
   105
immler@34551
   106
    val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
immler@34551
   107
    val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
immler@34526
   108
immler@34526
   109
    while (matcher.find() && invalid_tokens != Nil) {
wenzelm@34485
   110
			val kind =
wenzelm@34505
   111
        if (is_command_keyword(matcher.group))
wenzelm@34485
   112
          Token.Kind.COMMAND_START
wenzelm@34494
   113
        else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
wenzelm@34485
   114
          Token.Kind.COMMENT
wenzelm@34485
   115
        else
wenzelm@34485
   116
          Token.Kind.OTHER
immler@34551
   117
      val new_token = new Token(matcher.group, kind)
immler@34551
   118
      start += (new_token -> (match_start + matcher.start))
immler@34526
   119
      new_tokens ::= new_token
wenzelm@34318
   120
immler@34551
   121
      invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
immler@34526
   122
      invalid_tokens match {
immler@34551
   123
        case t::ts => if(start(t) == start(new_token) &&
immler@34551
   124
                         start(t) > change.start + change.added.length) {
immler@34526
   125
          old_suffix = ts
immler@34526
   126
          invalid_tokens = Nil
immler@34526
   127
        }
immler@34526
   128
        case _ =>
wenzelm@34318
   129
      }
wenzelm@34318
   130
    }
immler@34526
   131
    val insert = new_tokens.reverse
immler@34544
   132
    val new_token_list = begin ::: insert ::: old_suffix
immler@34554
   133
    val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
immler@34544
   134
    token_changed(change.id,
immler@34550
   135
                  begin.lastOption,
immler@34526
   136
                  insert,
immler@34550
   137
                  old_suffix.firstOption,
immler@34554
   138
                  new_tokenset,
immler@34551
   139
                  start)
wenzelm@34318
   140
  }
wenzelm@34318
   141
  
wenzelm@34485
   142
  /** command view **/
wenzelm@34485
   143
wenzelm@34496
   144
  def find_command_at(pos: Int): Command = {
immler@34554
   145
    for (cmd <- commands) { if (pos < cmd.stop(this)) return cmd }
wenzelm@34485
   146
    return null
wenzelm@34485
   147
  }
wenzelm@34485
   148
immler@34544
   149
  private def token_changed(new_id: String,
immler@34550
   150
                            before_change: Option[Token],
immler@34526
   151
                            inserted_tokens: List[Token],
immler@34550
   152
                            after_change: Option[Token],
immler@34554
   153
                            new_tokenset: LinearSet[Token],
immler@34551
   154
                            new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
wenzelm@34485
   155
  {
immler@34554
   156
    val cmd_first_changed =
immler@34554
   157
      if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get))
immler@34554
   158
      else None
immler@34554
   159
    val cmd_last_changed =
immler@34554
   160
      if (after_change.isDefined) commands.find(_.tokens.contains(after_change.get))
immler@34554
   161
      else None
immler@34544
   162
immler@34554
   163
    val cmd_before_change =
immler@34554
   164
      if (cmd_first_changed.isDefined) commands.prev(cmd_first_changed.get)
immler@34554
   165
      else None
immler@34554
   166
    val cmd_after_change =
immler@34554
   167
      if (cmd_last_changed.isDefined) commands.next(cmd_last_changed.get)
immler@34554
   168
      else None
wenzelm@34485
   169
immler@34554
   170
    val removed_commands = commands.dropWhile(Some(_) != cmd_first_changed).
immler@34554
   171
      takeWhile(Some(_) != cmd_after_change)
immler@34554
   172
immler@34554
   173
    // calculate inserted commands
immler@34526
   174
    def tokens_to_commands(tokens: List[Token]): List[Command]= {
immler@34526
   175
      tokens match {
immler@34526
   176
        case Nil => Nil
immler@34526
   177
        case t::ts =>
immler@34526
   178
          val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
immler@34554
   179
          new Command(t::cmd, new_token_start) :: tokens_to_commands (rest)
wenzelm@34485
   180
      }
wenzelm@34485
   181
    }
wenzelm@34485
   182
immler@34554
   183
    val split_begin_tokens =
immler@34554
   184
      if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil
immler@34554
   185
      else {
immler@34554
   186
        cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) ::: List(before_change.get)
immler@34554
   187
      }
immler@34554
   188
    val split_end_tokens =
immler@34554
   189
      if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil
immler@34554
   190
      else {
immler@34554
   191
        cmd_last_changed.get.tokens.dropWhile(_ != after_change.get)
immler@34554
   192
      }
immler@34554
   193
immler@34554
   194
    val rescanning_tokens = split_begin_tokens ::: inserted_tokens ::: split_end_tokens
immler@34554
   195
    val inserted_commands = tokens_to_commands(rescanning_tokens)
immler@34554
   196
immler@34554
   197
    val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList)
immler@34550
   198
    // build new document
immler@34554
   199
    val new_commandset = commands.delete_between(cmd_before_change, cmd_after_change).
immler@34554
   200
        insert_after(cmd_before_change, inserted_commands)
immler@34554
   201
immler@34544
   202
    val doc =
immler@34551
   203
      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword)
immler@34538
   204
    return (doc, change)
wenzelm@34485
   205
  }
wenzelm@34318
   206
}