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