src/Tools/jEdit/src/proofdocument/ProofDocument.scala
author immler@in.tum.de
Sun Mar 08 23:03:49 2009 +0100 (2009-03-08)
changeset 34532 aaafe9c4180b
parent 34531 db1c28e326fc
child 34538 20bfcca24658
permissions -rw-r--r--
ProofDocument without state
handle text-events via actor
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
wenzelm@34318
    41
}
wenzelm@34318
    42
immler@34532
    43
class ProofDocument(val tokens: LinearSet[Token],
immler@34532
    44
                    val commands: LinearSet[Command],
immler@34532
    45
                    val active: Boolean,
immler@34532
    46
                    is_command_keyword: String => Boolean,
immler@34532
    47
                    structural_changes: EventBus[StructureChange])
wenzelm@34483
    48
{
wenzelm@34485
    49
immler@34532
    50
  def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword, structural_changes)
immler@34532
    51
  def activate: ProofDocument = text_changed(new Text.Change(0, content, content.length)).mark_active
immler@34532
    52
  def set_command_keyword(f: String => Boolean): ProofDocument =
immler@34532
    53
    new ProofDocument(tokens, commands, active, f, structural_changes)
immler@34532
    54
  def set_event_bus(bus: EventBus[StructureChange]): ProofDocument =
immler@34532
    55
    new ProofDocument(tokens, commands, active, is_command_keyword, bus)
wenzelm@34485
    56
immler@34531
    57
  def content = Token.string_from_tokens(List() ++ tokens)
wenzelm@34485
    58
  /** token view **/
wenzelm@34485
    59
immler@34532
    60
  def text_changed(change: Text.Change): ProofDocument = 
wenzelm@34485
    61
  {
immler@34531
    62
    val tokens = List() ++ this.tokens
immler@34526
    63
    val (begin, remaining) = tokens.span(_.stop < change.start)
immler@34531
    64
    val (removed, end_unshifted) = remaining.span(_.start <= change.start + change.removed)
immler@34531
    65
    val end = for (t <- end_unshifted) yield t.shift(change.added.length - change.removed)
wenzelm@34485
    66
immler@34526
    67
    val split_begin = removed.takeWhile(_.start < change.start).
immler@34526
    68
      map (t => new Token(t.start,
immler@34526
    69
                          t.content.substring(0, change.start - t.start),
immler@34526
    70
                          t.kind))
immler@34526
    71
    val split_end = removed.dropWhile(_.stop < change.start + change.removed).
immler@34526
    72
      map (t => new Token(change.start + change.added.length,
immler@34526
    73
                          t.content.substring(change.start + change.removed - t.start),
immler@34526
    74
                          t.kind))
wenzelm@34318
    75
immler@34526
    76
    var invalid_tokens =  split_begin :::
immler@34526
    77
      new Token(change.start, change.added, Token.Kind.OTHER) :: split_end ::: end
immler@34526
    78
    var new_tokens = Nil: List[Token]
immler@34526
    79
    var old_suffix = Nil: List[Token]
wenzelm@34318
    80
immler@34526
    81
    val match_start = invalid_tokens.first.start
immler@34526
    82
    val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens))
immler@34526
    83
immler@34526
    84
    while (matcher.find() && invalid_tokens != Nil) {
wenzelm@34485
    85
			val kind =
wenzelm@34505
    86
        if (is_command_keyword(matcher.group))
wenzelm@34485
    87
          Token.Kind.COMMAND_START
wenzelm@34494
    88
        else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
wenzelm@34485
    89
          Token.Kind.COMMENT
wenzelm@34485
    90
        else
wenzelm@34485
    91
          Token.Kind.OTHER
immler@34526
    92
      val new_token = new Token(match_start + matcher.start, matcher.group, kind)
immler@34526
    93
      new_tokens ::= new_token
wenzelm@34318
    94
immler@34526
    95
      invalid_tokens = invalid_tokens dropWhile (_.stop < new_token.stop)
immler@34526
    96
      invalid_tokens match {
immler@34526
    97
        case t::ts => if(t.start == new_token.start &&
immler@34526
    98
                         t.start > change.start + change.added.length) {
immler@34526
    99
          old_suffix = ts
immler@34526
   100
          invalid_tokens = Nil
immler@34526
   101
        }
immler@34526
   102
        case _ =>
wenzelm@34318
   103
      }
wenzelm@34318
   104
    }
immler@34526
   105
    val insert = new_tokens.reverse
immler@34532
   106
    val new_tokenset = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]]
immler@34526
   107
immler@34526
   108
    token_changed(begin.lastOption,
immler@34526
   109
                  insert,
immler@34526
   110
                  removed,
immler@34532
   111
                  new_tokenset,
immler@34526
   112
                  old_suffix.firstOption)
wenzelm@34318
   113
  }
wenzelm@34318
   114
  
wenzelm@34485
   115
  /** command view **/
wenzelm@34485
   116
wenzelm@34496
   117
  def find_command_at(pos: Int): Command = {
wenzelm@34485
   118
    for (cmd <- commands) { if (pos < cmd.stop) return cmd }
wenzelm@34485
   119
    return null
wenzelm@34485
   120
  }
wenzelm@34485
   121
immler@34526
   122
  private def token_changed(before_change: Option[Token],
immler@34526
   123
                            inserted_tokens: List[Token],
immler@34526
   124
                            removed_tokens: List[Token],
immler@34532
   125
                            new_tokenset: LinearSet[Token],
immler@34532
   126
                            after_change: Option[Token]): ProofDocument =
wenzelm@34485
   127
  {
immler@34531
   128
    val commands = List() ++ this.commands
immler@34526
   129
    val (begin, remaining) =
immler@34526
   130
      before_change match {
immler@34526
   131
        case None => (Nil, commands)
immler@34526
   132
        case Some(bc) => commands.break(_.tokens.contains(bc))
immler@34526
   133
      }
immler@34526
   134
    val (_removed, _end) =
immler@34526
   135
      after_change match {
immler@34526
   136
        case None => (remaining, Nil)
immler@34526
   137
        case Some(ac) => remaining.break(_.tokens.contains(ac))
immler@34526
   138
      }
immler@34526
   139
    val (removed, end) = _end match {
immler@34526
   140
      case Nil => (_removed, Nil)
immler@34526
   141
      case acc::end => if (after_change.isDefined && after_change.get.kind == Token.Kind.COMMAND_START)
immler@34526
   142
          (_removed, _end)
immler@34526
   143
        else (_removed ::: List(acc), end)
wenzelm@34485
   144
    }
immler@34526
   145
    val all_removed_tokens = for(c <- removed; t <- c.tokens) yield t
immler@34526
   146
    val (pseudo_new_pre, rest) =
immler@34526
   147
      if (! before_change.isDefined) (Nil, all_removed_tokens)
immler@34526
   148
      else {
immler@34526
   149
        val (a, b) = all_removed_tokens.span (_ != before_change.get)
immler@34526
   150
        b match {
immler@34526
   151
          case Nil => (a, Nil)
immler@34526
   152
          case bc::rest => (a ::: List(bc), b)
immler@34526
   153
        }
wenzelm@34485
   154
      }
immler@34526
   155
    val pseudo_new_post = rest.dropWhile(Some(_) != after_change)
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@34526
   166
    System.err.println("ins_tokens: " + inserted_tokens)
immler@34526
   167
    val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
immler@34526
   168
    System.err.println("new_commands: " + new_commands)
wenzelm@34485
   169
immler@34532
   170
    val new_commandset = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
immler@34526
   171
    val before = begin match {case Nil => None case _ => Some (begin.last)}
immler@34526
   172
    structural_changes.event(new StructureChange(before, new_commands, removed))
immler@34532
   173
    new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword, structural_changes)
wenzelm@34485
   174
  }
wenzelm@34318
   175
}