src/Pure/PIDE/document.scala
author wenzelm
Wed Aug 11 22:41:26 2010 +0200 (2010-08-11)
changeset 38355 8cb265fb12fe
parent 38227 6bbb42843b6e
child 38356 443fb83a21e8
permissions -rw-r--r--
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
     1 /*  Title:      Pure/PIDE/document.scala
     2     Author:     Makarius
     3 
     4 Document as collection of named nodes, each consisting of an editable
     5 list of commands.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.mutable
    12 import scala.annotation.tailrec
    13 
    14 
    15 object Document
    16 {
    17   /* formal identifiers */
    18 
    19   type Version_ID = Long
    20   type Command_ID = Long
    21   type State_ID = Long
    22 
    23   val NO_ID = 0L
    24 
    25   def parse_id(s: String): Long = java.lang.Long.parseLong(s)
    26   def print_id(id: Long): String = id.toString
    27 
    28 
    29 
    30   /** named document nodes **/
    31 
    32   object Node
    33   {
    34     val empty: Node = new Node(Linear_Set())
    35 
    36     def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
    37     {
    38       var i = offset
    39       for (command <- commands) yield {
    40         val start = i
    41         i += command.length
    42         (command, start)
    43       }
    44     }
    45   }
    46 
    47   class Node(val commands: Linear_Set[Command])
    48   {
    49     /* command ranges */
    50 
    51     def command_starts: Iterator[(Command, Int)] =
    52       Node.command_starts(commands.iterator)
    53 
    54     def command_start(cmd: Command): Option[Int] =
    55       command_starts.find(_._1 == cmd).map(_._2)
    56 
    57     def command_range(i: Int): Iterator[(Command, Int)] =
    58       command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    59 
    60     def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
    61       command_range(i) takeWhile { case (_, start) => start < j }
    62 
    63     def command_at(i: Int): Option[(Command, Int)] =
    64     {
    65       val range = command_range(i)
    66       if (range.hasNext) Some(range.next) else None
    67     }
    68 
    69     def proper_command_at(i: Int): Option[Command] =
    70       command_at(i) match {
    71         case Some((command, _)) =>
    72           commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
    73         case None => None
    74       }
    75   }
    76 
    77 
    78   /* initial document */
    79 
    80   val init: Document =
    81   {
    82     val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
    83     doc.assign_states(Nil)
    84     doc
    85   }
    86 
    87 
    88 
    89   /** changes of plain text, eventually resulting in document edits **/
    90 
    91   type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
    92 
    93   type Edit[C] =
    94    (String,  // node name
    95     Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
    96 
    97   abstract class Snapshot
    98   {
    99     val document: Document
   100     val node: Document.Node
   101     val is_outdated: Boolean
   102     def convert(offset: Int): Int
   103     def revert(offset: Int): Int
   104   }
   105 
   106   object Change
   107   {
   108     val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
   109   }
   110 
   111   class Change(
   112     val id: Version_ID,
   113     val parent: Option[Change],
   114     val edits: List[Node_Text_Edit],
   115     val result: Future[(List[Edit[Command]], Document)])
   116   {
   117     def ancestors: Iterator[Change] = new Iterator[Change]
   118     {
   119       private var state: Option[Change] = Some(Change.this)
   120       def hasNext = state.isDefined
   121       def next =
   122         state match {
   123           case Some(change) => state = change.parent; change
   124           case None => throw new NoSuchElementException("next on empty iterator")
   125         }
   126     }
   127 
   128     def join_document: Document = result.join._2
   129     def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
   130 
   131     def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot =
   132     {
   133       val latest = Change.this
   134       val stable = latest.ancestors.find(_.is_assigned)
   135       require(stable.isDefined)
   136 
   137       val edits =
   138         (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
   139             (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
   140       lazy val reverse_edits = edits.reverse
   141 
   142       new Snapshot {
   143         val document = stable.get.join_document
   144         val node = document.nodes(name)
   145         val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
   146         def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
   147         def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   148       }
   149     }
   150   }
   151 
   152 
   153 
   154   /** editing **/
   155 
   156   def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
   157       edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
   158   {
   159     require(old_doc.assignment.is_finished)
   160 
   161 
   162     /* unparsed dummy commands */
   163 
   164     def unparsed(source: String) =
   165       new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source)))
   166 
   167     def is_unparsed(command: Command) = command.id == NO_ID
   168 
   169 
   170     /* phase 1: edit individual command source */
   171 
   172     @tailrec def edit_text(eds: List[Text_Edit],
   173         commands: Linear_Set[Command]): Linear_Set[Command] =
   174     {
   175       eds match {
   176         case e :: es =>
   177           Node.command_starts(commands.iterator).find {
   178             case (cmd, cmd_start) =>
   179               e.can_edit(cmd.source, cmd_start) ||
   180                 e.is_insert && e.start == cmd_start + cmd.length
   181           } match {
   182             case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
   183               val (rest, text) = e.edit(cmd.source, cmd_start)
   184               val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
   185               edit_text(rest.toList ::: es, new_commands)
   186 
   187             case Some((cmd, cmd_start)) =>
   188               edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
   189 
   190             case None =>
   191               require(e.is_insert && e.start == 0)
   192               edit_text(es, commands.insert_after(None, unparsed(e.text)))
   193           }
   194         case Nil => commands
   195       }
   196     }
   197 
   198 
   199     /* phase 2: recover command spans */
   200 
   201     @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
   202     {
   203       commands.iterator.find(is_unparsed) match {
   204         case Some(first_unparsed) =>
   205           val first =
   206             commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
   207           val last =
   208             commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
   209           val range =
   210             commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
   211 
   212           val sources = range.flatMap(_.span.map(_.source))
   213           val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
   214 
   215           val (before_edit, spans1) =
   216             if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
   217               (Some(first), spans0.tail)
   218             else (commands.prev(first), spans0)
   219 
   220           val (after_edit, spans2) =
   221             if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
   222               (Some(last), spans1.take(spans1.length - 1))
   223             else (commands.next(last), spans1)
   224 
   225           val inserted = spans2.map(span => new Command(session.create_id(), span))
   226           val new_commands =
   227             commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
   228           parse_spans(new_commands)
   229 
   230         case None => commands
   231       }
   232     }
   233 
   234 
   235     /* phase 3: resulting document edits */
   236 
   237     {
   238       val doc_edits = new mutable.ListBuffer[Edit[Command]]
   239       var nodes = old_doc.nodes
   240       var former_states = old_doc.assignment.join
   241 
   242       for ((name, text_edits) <- edits) {
   243         val commands0 = nodes(name).commands
   244         val commands1 = edit_text(text_edits, commands0)
   245         val commands2 = parse_spans(commands1)   // FIXME somewhat slow
   246 
   247         val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
   248         val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
   249 
   250         val cmd_edits =
   251           removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
   252           inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
   253 
   254         doc_edits += (name -> Some(cmd_edits))
   255         nodes += (name -> new Node(commands2))
   256         former_states --= removed_commands
   257       }
   258       (doc_edits.toList, new Document(new_id, nodes, former_states))
   259     }
   260   }
   261 }
   262 
   263 
   264 class Document(
   265     val id: Document.Version_ID,
   266     val nodes: Map[String, Document.Node],
   267     former_states: Map[Command, Command])  // FIXME !?
   268 {
   269   /* command state assignment */
   270 
   271   val assignment = Future.promise[Map[Command, Command]]
   272   def await_assignment { assignment.join }
   273 
   274   @volatile private var tmp_states = former_states
   275 
   276   def assign_states(new_states: List[(Command, Command)])
   277   {
   278     assignment.fulfill(tmp_states ++ new_states)
   279     tmp_states = Map()
   280   }
   281 
   282   def current_state(cmd: Command): State =
   283   {
   284     require(assignment.is_finished)
   285     (assignment.join).get(cmd) match {
   286       case Some(cmd_state) => cmd_state.current_state
   287       case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
   288     }
   289   }
   290 }