src/Tools/jEdit/src/proofdocument/proof_document.scala
author wenzelm
Tue Dec 08 14:49:01 2009 +0100 (2009-12-08)
changeset 34759 bfea7839d9e1
parent 34741 src/Tools/jEdit/src/proofdocument/ProofDocument.scala@4431c498726d
child 34760 dc7f5e0d9d27
permissions -rw-r--r--
misc rearrangement of files;
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
wenzelm@34703
    11
import scala.actors.Actor, Actor._
wenzelm@34703
    12
wenzelm@34318
    13
import java.util.regex.Pattern
wenzelm@34703
    14
immler@34674
    15
import isabelle.prover.{Prover, Command, Command_State}
wenzelm@34318
    16
wenzelm@34485
    17
wenzelm@34483
    18
object ProofDocument
wenzelm@34483
    19
{
wenzelm@34582
    20
  // Be careful when changing this regex. Not only must it handle the
wenzelm@34318
    21
  // spurious end of a token but also:  
wenzelm@34318
    22
  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
wenzelm@34318
    23
  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
wenzelm@34318
    24
  
wenzelm@34483
    25
  val token_pattern = 
wenzelm@34318
    26
    Pattern.compile(
wenzelm@34318
    27
      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
wenzelm@34318
    28
      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
wenzelm@34318
    29
      "(\\?'?|')[A-Za-z_0-9.]*|" + 
wenzelm@34318
    30
      "[A-Za-z_0-9.]+|" + 
wenzelm@34318
    31
      "[!#$%&*+-/<=>?@^_|~]+|" +
wenzelm@34318
    32
      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
wenzelm@34318
    33
      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
wenzelm@34318
    34
      "[()\\[\\]{}:;]", Pattern.MULTILINE)
wenzelm@34485
    35
immler@34660
    36
  val empty =
immler@34660
    37
    new ProofDocument(isabelle.jedit.Isabelle.system.id(),
wenzelm@34724
    38
      Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
immler@34660
    39
immler@34660
    40
  type StructureChange = List[(Option[Command], Option[Command])]
immler@34538
    41
wenzelm@34318
    42
}
wenzelm@34318
    43
wenzelm@34582
    44
class ProofDocument(
wenzelm@34582
    45
  val id: String,
wenzelm@34689
    46
  val tokens: Linear_Set[Token],
wenzelm@34582
    47
  val token_start: Map[Token, Int],
wenzelm@34689
    48
  val commands: Linear_Set[Command],
wenzelm@34722
    49
  var states: Map[Command, Command_State],   // FIXME immutable
wenzelm@34724
    50
  is_command_keyword: String => Boolean)
wenzelm@34483
    51
{
immler@34660
    52
  import ProofDocument.StructureChange
immler@34653
    53
immler@34532
    54
  def set_command_keyword(f: String => Boolean): ProofDocument =
wenzelm@34724
    55
    new ProofDocument(id, tokens, token_start, commands, states, f)
wenzelm@34485
    56
wenzelm@34582
    57
  def content = Token.string_from_tokens(Nil ++ tokens, token_start)
wenzelm@34657
    58
wenzelm@34657
    59
wenzelm@34693
    60
  
wenzelm@34485
    61
  /** token view **/
wenzelm@34485
    62
wenzelm@34693
    63
  def text_changed(change: Change): (ProofDocument, StructureChange) =
wenzelm@34485
    64
  {
immler@34660
    65
    def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
immler@34660
    66
      val (doc, chgs) = doc_chgs
wenzelm@34693
    67
      val (new_doc, chg) = doc.text_edit(edit, change.id)
immler@34660
    68
      (new_doc, chgs ++ chg)
immler@34660
    69
    }
wenzelm@34693
    70
    ((this, Nil: StructureChange) /: change.edits)(edit_doc)
immler@34660
    71
  }
immler@34660
    72
wenzelm@34741
    73
  def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
immler@34660
    74
  {
immler@34660
    75
    case class TextChange(start: Int, added: String, removed: String)
immler@34660
    76
    val change = e match {
immler@34660
    77
      case Insert(s, a) => TextChange(s, a, "")
immler@34660
    78
      case Remove(s, r) => TextChange(s, "", r)
immler@34660
    79
    }
immler@34551
    80
    //indices of tokens
immler@34551
    81
    var start: Map[Token, Int] = token_start
immler@34551
    82
    def stop(t: Token) = start(t) + t.length
immler@34551
    83
    // split old token lists
wenzelm@34582
    84
    val tokens = Nil ++ this.tokens
immler@34551
    85
    val (begin, remaining) = tokens.span(stop(_) < change.start)
immler@34648
    86
    val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
immler@34551
    87
    // update indices
wenzelm@34582
    88
    start = end.foldLeft(start)((s, t) =>
immler@34648
    89
      s + (t -> (s(t) + change.added.length - change.removed.length)))
wenzelm@34485
    90
immler@34551
    91
    val split_begin = removed.takeWhile(start(_) < change.start).
immler@34554
    92
      map (t => {
immler@34554
    93
          val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
immler@34554
    94
          start += (split_tok -> start(t))
immler@34554
    95
          split_tok
immler@34554
    96
        })
immler@34554
    97
immler@34648
    98
    val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
immler@34554
    99
      map (t => {
wenzelm@34582
   100
          val split_tok =
immler@34648
   101
            new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
immler@34554
   102
          start += (split_tok -> start(t))
immler@34554
   103
          split_tok
immler@34554
   104
        })
immler@34551
   105
    // update indices
immler@34554
   106
    start = removed.foldLeft (start) ((s, t) => s - t)
immler@34554
   107
    start = split_end.foldLeft (start) ((s, t) =>
immler@34554
   108
    s + (t -> (change.start + change.added.length)))
wenzelm@34318
   109
immler@34551
   110
    val ins = new Token(change.added, Token.Kind.OTHER)
immler@34551
   111
    start += (ins -> change.start)
immler@34551
   112
    
wenzelm@34582
   113
    var invalid_tokens = split_begin ::: ins :: split_end ::: end
wenzelm@34582
   114
    var new_tokens: List[Token] = Nil
wenzelm@34582
   115
    var old_suffix: List[Token] = Nil
wenzelm@34318
   116
immler@34551
   117
    val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
wenzelm@34582
   118
    val matcher =
wenzelm@34582
   119
      ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
immler@34526
   120
immler@34526
   121
    while (matcher.find() && invalid_tokens != Nil) {
wenzelm@34485
   122
			val kind =
wenzelm@34505
   123
        if (is_command_keyword(matcher.group))
wenzelm@34485
   124
          Token.Kind.COMMAND_START
wenzelm@34494
   125
        else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
wenzelm@34485
   126
          Token.Kind.COMMENT
wenzelm@34485
   127
        else
wenzelm@34485
   128
          Token.Kind.OTHER
immler@34551
   129
      val new_token = new Token(matcher.group, kind)
immler@34551
   130
      start += (new_token -> (match_start + matcher.start))
immler@34526
   131
      new_tokens ::= new_token
wenzelm@34318
   132
immler@34660
   133
      invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
immler@34526
   134
      invalid_tokens match {
wenzelm@34582
   135
        case t :: ts =>
wenzelm@34582
   136
          if (start(t) == start(new_token) &&
wenzelm@34582
   137
              start(t) > change.start + change.added.length) {
immler@34597
   138
          old_suffix = t :: ts
immler@34592
   139
          new_tokens = new_tokens.tail
immler@34526
   140
          invalid_tokens = Nil
immler@34526
   141
        }
immler@34526
   142
        case _ =>
wenzelm@34318
   143
      }
wenzelm@34318
   144
    }
immler@34526
   145
    val insert = new_tokens.reverse
immler@34544
   146
    val new_token_list = begin ::: insert ::: old_suffix
immler@34660
   147
    token_changed(id, begin.lastOption, insert,
immler@34597
   148
      old_suffix.firstOption, new_token_list, start)
wenzelm@34318
   149
  }
wenzelm@34582
   150
wenzelm@34318
   151
  
wenzelm@34485
   152
  /** command view **/
wenzelm@34485
   153
wenzelm@34582
   154
  private def token_changed(
wenzelm@34582
   155
    new_id: String,
wenzelm@34582
   156
    before_change: Option[Token],
wenzelm@34582
   157
    inserted_tokens: List[Token],
wenzelm@34582
   158
    after_change: Option[Token],
immler@34597
   159
    new_tokens: List[Token],
immler@34660
   160
    new_token_start: Map[Token, Int]):
immler@34660
   161
  (ProofDocument, StructureChange) =
wenzelm@34485
   162
  {
wenzelm@34689
   163
    val new_tokenset = Linear_Set[Token]() ++ new_tokens
immler@34593
   164
    val cmd_before_change = before_change match {
immler@34593
   165
      case None => None
immler@34593
   166
      case Some(bc) =>
immler@34593
   167
        val cmd_with_bc = commands.find(_.contains(bc)).get
immler@34593
   168
        if (cmd_with_bc.tokens.last == bc) {
immler@34593
   169
          if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
immler@34593
   170
            Some(cmd_with_bc)
immler@34593
   171
          else commands.prev(cmd_with_bc)
immler@34593
   172
        }
immler@34593
   173
        else commands.prev(cmd_with_bc)
immler@34593
   174
    }
immler@34544
   175
immler@34593
   176
    val cmd_after_change = after_change match {
immler@34593
   177
      case None => None
immler@34593
   178
      case Some(ac) =>
immler@34593
   179
        val cmd_with_ac = commands.find(_.contains(ac)).get
immler@34593
   180
        if (ac.is_start)
immler@34593
   181
          Some(cmd_with_ac)
immler@34593
   182
        else
immler@34593
   183
          commands.next(cmd_with_ac)
immler@34593
   184
    }
wenzelm@34485
   185
immler@34593
   186
    val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
immler@34554
   187
      takeWhile(Some(_) != cmd_after_change)
immler@34554
   188
immler@34554
   189
    // calculate inserted commands
immler@34526
   190
    def tokens_to_commands(tokens: List[Token]): List[Command]= {
immler@34526
   191
      tokens match {
immler@34526
   192
        case Nil => Nil
wenzelm@34582
   193
        case t :: ts =>
wenzelm@34582
   194
          val (cmd, rest) =
wenzelm@34582
   195
            ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
wenzelm@34724
   196
          new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest)
wenzelm@34485
   197
      }
wenzelm@34485
   198
    }
wenzelm@34485
   199
immler@34593
   200
    val split_begin =
immler@34593
   201
      if (before_change.isDefined) {
immler@34593
   202
        val changed =
immler@34593
   203
          if (cmd_before_change.isDefined)
immler@34595
   204
            new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
immler@34593
   205
          else new_tokenset
immler@34593
   206
        if (changed.exists(_ == before_change.get))
immler@34597
   207
          changed.takeWhile(_ != before_change.get).toList :::
immler@34597
   208
            List(before_change.get)
immler@34593
   209
        else Nil
immler@34593
   210
      } else Nil
immler@34554
   211
immler@34593
   212
    val split_end =
immler@34667
   213
      if (after_change.isDefined) {
immler@34595
   214
        val unchanged = new_tokens.dropWhile(_ != after_change.get)
immler@34667
   215
        if(cmd_after_change.isDefined) {
immler@34667
   216
          if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
immler@34667
   217
            unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
immler@34667
   218
          else Nil
immler@34667
   219
        } else {
immler@34667
   220
          unchanged
immler@34667
   221
        }
immler@34593
   222
      } else Nil
immler@34593
   223
immler@34597
   224
    val rescan_begin =
immler@34597
   225
      split_begin :::
immler@34597
   226
        before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
wenzelm@34582
   227
    val rescanning_tokens =
immler@34597
   228
      after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
immler@34597
   229
        split_end
immler@34593
   230
    val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
immler@34554
   231
immler@34550
   232
    // build new document
wenzelm@34739
   233
    val new_commandset = commands.
wenzelm@34739
   234
      delete_between(cmd_before_change, cmd_after_change).
wenzelm@34739
   235
      append_after(cmd_before_change, inserted_commands)
wenzelm@34739
   236
immler@34554
   237
immler@34544
   238
    val doc =
immler@34674
   239
      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
wenzelm@34724
   240
        states -- removed_commands, is_command_keyword)
immler@34660
   241
immler@34660
   242
    val removes =
immler@34660
   243
      for (cmd <- removed_commands) yield (cmd_before_change -> None)
immler@34660
   244
    val inserts =
immler@34660
   245
      for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
immler@34660
   246
immler@34660
   247
    return (doc, removes.toList ++ inserts)
wenzelm@34485
   248
  }
immler@34596
   249
immler@34596
   250
  val commands_offsets = {
immler@34596
   251
    var last_stop = 0
immler@34596
   252
    (for (c <- commands) yield {
immler@34596
   253
      val r = c -> (last_stop,c.stop(this))
immler@34596
   254
      last_stop = c.stop(this)
immler@34596
   255
      r
immler@34596
   256
    }).toArray
immler@34596
   257
  }
immler@34596
   258
wenzelm@34712
   259
  def command_at(pos: Int): Option[Command] =
wenzelm@34712
   260
    find_command(pos, 0, commands_offsets.length)
wenzelm@34712
   261
immler@34596
   262
  // use a binary search to find commands for a given offset
wenzelm@34712
   263
  private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
wenzelm@34712
   264
  {
immler@34596
   265
    val middle_index = (array_start + array_stop) / 2
wenzelm@34712
   266
    if (middle_index >= commands_offsets.length) return None
immler@34596
   267
    val (middle, (start, stop)) = commands_offsets(middle_index)
immler@34596
   268
    // does middle contain pos?
wenzelm@34712
   269
    if (start <= pos && pos < stop)
wenzelm@34712
   270
      Some(middle)
immler@34596
   271
    else if (start > pos)
wenzelm@34712
   272
      find_command(pos, array_start, middle_index)
immler@34596
   273
    else if (stop <= pos)
wenzelm@34712
   274
      find_command(pos, middle_index + 1, array_stop)
wenzelm@34712
   275
    else error("impossible")
immler@34596
   276
  }
wenzelm@34318
   277
}