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