src/Pure/PIDE/document.scala
author wenzelm
Sun Aug 15 22:48:56 2010 +0200 (2010-08-15)
changeset 38426 2858ec7b6dd8
parent 38425 e467db701d78
child 38427 7066fbd315ae
permissions -rw-r--r--
specific types Text.Offset and Text.Range;
minor tuning;
     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, associated with asynchronous execution process.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.mutable
    12 
    13 
    14 object Document
    15 {
    16   /* formal identifiers */
    17 
    18   type ID = Long
    19 
    20   object ID {
    21     def apply(id: ID): String = Markup.Long.apply(id)
    22     def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
    23   }
    24 
    25   type Version_ID = ID
    26   type Command_ID = ID
    27   type Exec_ID = ID
    28 
    29   val NO_ID: ID = 0
    30 
    31 
    32 
    33   /** document structure **/
    34 
    35   /* named nodes -- development graph */
    36 
    37   type Node_Text_Edit = (String, List[Text.Edit])  // FIXME None: remove
    38 
    39   type Edit[C] =
    40    (String,  // node name
    41     Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
    42 
    43   object Node
    44   {
    45     val empty: Node = new Node(Linear_Set())
    46 
    47     // FIXME not scalable
    48     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    49       : Iterator[(Command, Text.Offset)] =
    50     {
    51       var i = offset
    52       for (command <- commands) yield {
    53         val start = i
    54         i += command.length
    55         (command, start)
    56       }
    57     }
    58   }
    59 
    60   class Node(val commands: Linear_Set[Command])
    61   {
    62     def command_starts: Iterator[(Command, Text.Offset)] =
    63       Node.command_starts(commands.iterator)
    64 
    65     def command_start(cmd: Command): Option[Text.Offset] =
    66       command_starts.find(_._1 == cmd).map(_._2)
    67 
    68     def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
    69       command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    70 
    71     def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
    72       command_range(i) takeWhile { case (_, start) => start < j }
    73 
    74     def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
    75     {
    76       val range = command_range(i)
    77       if (range.hasNext) Some(range.next) else None
    78     }
    79 
    80     def proper_command_at(i: Text.Offset): Option[Command] =
    81       command_at(i) match {
    82         case Some((command, _)) =>
    83           commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
    84         case None => None
    85       }
    86   }
    87 
    88 
    89 
    90   /** versioning **/
    91 
    92   /* particular document versions */
    93 
    94   object Version
    95   {
    96     val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
    97   }
    98 
    99   class Version(val id: Version_ID, val nodes: Map[String, Node])
   100 
   101 
   102   /* changes of plain text, eventually resulting in document edits */
   103 
   104   object Change
   105   {
   106     val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
   107   }
   108 
   109   class Change(
   110     val previous: Future[Version],
   111     val edits: List[Node_Text_Edit],
   112     val result: Future[(List[Edit[Command]], Version)])
   113   {
   114     val current: Future[Version] = result.map(_._2)
   115     def is_finished: Boolean = previous.is_finished && current.is_finished
   116   }
   117 
   118 
   119   /* history navigation and persistent snapshots */
   120 
   121   abstract class Snapshot
   122   {
   123     val version: Version
   124     val node: Node
   125     val is_outdated: Boolean
   126     def convert(i: Text.Offset): Text.Offset
   127     def revert(i: Text.Offset): Text.Offset
   128     def lookup_command(id: Command_ID): Option[Command]
   129     def state(command: Command): Command.State
   130   }
   131 
   132   object History
   133   {
   134     val init = new History(List(Change.init))
   135   }
   136 
   137   // FIXME pruning, purging of state
   138   class History(undo_list: List[Change])
   139   {
   140     require(!undo_list.isEmpty)
   141 
   142     def tip: Change = undo_list.head
   143     def +(ch: Change): History = new History(ch :: undo_list)
   144 
   145     def snapshot(name: String, pending_edits: List[Text.Edit], state_snapshot: State): Snapshot =
   146     {
   147       val found_stable = undo_list.find(change =>
   148         change.is_finished && state_snapshot.is_assigned(change.current.join))
   149       require(found_stable.isDefined)
   150       val stable = found_stable.get
   151       val latest = undo_list.head
   152 
   153       val edits =
   154         (pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) =>
   155             (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
   156       lazy val reverse_edits = edits.reverse
   157 
   158       new Snapshot
   159       {
   160         val version = stable.current.join
   161         val node = version.nodes(name)
   162         val is_outdated = !(pending_edits.isEmpty && latest == stable)
   163 
   164         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
   165         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   166 
   167         def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
   168         def state(command: Command): Command.State =
   169           try { state_snapshot.command_state(version, command) }
   170           catch { case _: State.Fail => command.empty_state }
   171       }
   172     }
   173   }
   174 
   175 
   176 
   177   /** global state -- document structure and execution process **/
   178 
   179   object State
   180   {
   181     class Fail(state: State) extends Exception
   182 
   183     val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
   184 
   185     class Assignment(former_assignment: Map[Command, Exec_ID])
   186     {
   187       @volatile private var tmp_assignment = former_assignment
   188       private val promise = Future.promise[Map[Command, Exec_ID]]
   189       def is_finished: Boolean = promise.is_finished
   190       def join: Map[Command, Exec_ID] = promise.join
   191       def assign(command_execs: List[(Command, Exec_ID)])
   192       {
   193         promise.fulfill(tmp_assignment ++ command_execs)
   194         tmp_assignment = Map()
   195       }
   196     }
   197   }
   198 
   199   case class State(
   200     val versions: Map[Version_ID, Version] = Map(),
   201     val commands: Map[Command_ID, Command.State] = Map(),
   202     val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
   203     val assignments: Map[Version, State.Assignment] = Map(),
   204     val disposed: Set[ID] = Set())  // FIXME unused!?
   205   {
   206     private def fail[A]: A = throw new State.Fail(this)
   207 
   208     def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
   209     {
   210       val id = version.id
   211       if (versions.isDefinedAt(id) || disposed(id)) fail
   212       copy(versions = versions + (id -> version),
   213         assignments = assignments + (version -> new State.Assignment(former_assignment)))
   214     }
   215 
   216     def define_command(command: Command): State =
   217     {
   218       val id = command.id
   219       if (commands.isDefinedAt(id) || disposed(id)) fail
   220       copy(commands = commands + (id -> command.empty_state))
   221     }
   222 
   223     def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
   224 
   225     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
   226     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
   227     def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
   228     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
   229 
   230     def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
   231       execs.get(id) match {
   232         case Some((st, occs)) =>
   233           val new_st = st.accumulate(message)
   234           (new_st, copy(execs = execs + (id -> (new_st, occs))))
   235         case None =>
   236           commands.get(id) match {
   237             case Some(st) =>
   238               val new_st = st.accumulate(message)
   239               (new_st, copy(commands = commands + (id -> new_st)))
   240             case None => fail
   241           }
   242       }
   243 
   244     def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
   245     {
   246       val version = the_version(id)
   247       val occs = Set(version)  // FIXME unused (!?)
   248 
   249       var new_execs = execs
   250       val assigned_execs =
   251         for ((cmd_id, exec_id) <- edits) yield {
   252           val st = the_command(cmd_id)
   253           if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
   254           new_execs += (exec_id -> (st, occs))
   255           (st.command, exec_id)
   256         }
   257       the_assignment(version).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
   258       copy(execs = new_execs)
   259     }
   260 
   261     def is_assigned(version: Version): Boolean =
   262       assignments.get(version) match {
   263         case Some(assgn) => assgn.is_finished
   264         case None => false
   265       }
   266 
   267     def command_state(version: Version, command: Command): Command.State =
   268     {
   269       val assgn = the_assignment(version)
   270       require(assgn.is_finished)
   271       the_exec_state(assgn.join.getOrElse(command, fail))
   272     }
   273   }
   274 }
   275