src/Pure/PIDE/document.scala
author wenzelm
Mon Aug 30 13:01:32 2010 +0200 (2010-08-30)
changeset 38872 26c505765024
parent 38848 9483bb678d96
child 38879 dde403450419
permissions -rw-r--r--
Command.results: ordered by serial number;
     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 = 0): Iterator[(Command, Text.Offset)] =
    69       command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    70 
    71     def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
    72       command_range(range.start) takeWhile { case (_, start) => start < range.stop }
    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 */
   120 
   121   object History
   122   {
   123     val init = new History(List(Change.init))
   124   }
   125 
   126   // FIXME pruning, purging of state
   127   class History(val undo_list: List[Change])
   128   {
   129     require(!undo_list.isEmpty)
   130 
   131     def tip: Change = undo_list.head
   132     def +(change: Change): History = new History(change :: undo_list)
   133   }
   134 
   135 
   136 
   137   /** global state -- document structure, execution process, editing history **/
   138 
   139   abstract class Snapshot
   140   {
   141     val version: Version
   142     val node: Node
   143     val is_outdated: Boolean
   144     def lookup_command(id: Command_ID): Option[Command]
   145     def state(command: Command): Command.State
   146     def convert(i: Text.Offset): Text.Offset
   147     def convert(range: Text.Range): Text.Range = range.map(convert(_))
   148     def revert(i: Text.Offset): Text.Offset
   149     def revert(range: Text.Range): Text.Range = range.map(revert(_))
   150     def select_markup[A](range: Text.Range)
   151       (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
   152   }
   153 
   154   object State
   155   {
   156     class Fail(state: State) extends Exception
   157 
   158     val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
   159 
   160     class Assignment(former_assignment: Map[Command, Exec_ID])
   161     {
   162       @volatile private var tmp_assignment = former_assignment
   163       private val promise = Future.promise[Map[Command, Exec_ID]]
   164       def is_finished: Boolean = promise.is_finished
   165       def join: Map[Command, Exec_ID] = promise.join
   166       def get_finished: Map[Command, Exec_ID] = promise.get_finished
   167       def assign(command_execs: List[(Command, Exec_ID)])
   168       {
   169         promise.fulfill(tmp_assignment ++ command_execs)
   170         tmp_assignment = Map()
   171       }
   172     }
   173   }
   174 
   175   case class State(
   176     val versions: Map[Version_ID, Version] = Map(),
   177     val commands: Map[Command_ID, Command.State] = Map(),
   178     val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
   179     val assignments: Map[Version, State.Assignment] = Map(),
   180     val disposed: Set[ID] = Set(),  // FIXME unused!?
   181     val history: History = History.init)
   182   {
   183     private def fail[A]: A = throw new State.Fail(this)
   184 
   185     def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
   186     {
   187       val id = version.id
   188       if (versions.isDefinedAt(id) || disposed(id)) fail
   189       copy(versions = versions + (id -> version),
   190         assignments = assignments + (version -> new State.Assignment(former_assignment)))
   191     }
   192 
   193     def define_command(command: Command): State =
   194     {
   195       val id = command.id
   196       if (commands.isDefinedAt(id) || disposed(id)) fail
   197       copy(commands = commands + (id -> command.empty_state))
   198     }
   199 
   200     def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
   201 
   202     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
   203     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
   204     def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
   205     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
   206 
   207     def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
   208       execs.get(id) match {
   209         case Some((st, occs)) =>
   210           val new_st = st.accumulate(message)
   211           (new_st, copy(execs = execs + (id -> (new_st, occs))))
   212         case None =>
   213           commands.get(id) match {
   214             case Some(st) =>
   215               val new_st = st.accumulate(message)
   216               (new_st, copy(commands = commands + (id -> new_st)))
   217             case None => fail
   218           }
   219       }
   220 
   221     def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
   222     {
   223       val version = the_version(id)
   224       val occs = Set(version)  // FIXME unused (!?)
   225 
   226       var new_execs = execs
   227       val assigned_execs =
   228         for ((cmd_id, exec_id) <- edits) yield {
   229           val st = the_command(cmd_id)
   230           if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
   231           new_execs += (exec_id -> (st, occs))
   232           (st.command, exec_id)
   233         }
   234       the_assignment(version).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
   235       copy(execs = new_execs)
   236     }
   237 
   238     def is_assigned(version: Version): Boolean =
   239       assignments.get(version) match {
   240         case Some(assgn) => assgn.is_finished
   241         case None => false
   242       }
   243 
   244     def extend_history(previous: Future[Version],
   245         edits: List[Node_Text_Edit],
   246         result: Future[(List[Edit[Command]], Version)]): (Change, State) =
   247     {
   248       val change = new Change(previous, edits, result)
   249       (change, copy(history = history + change))
   250     }
   251 
   252 
   253     // persistent user-view
   254     def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
   255     {
   256       val found_stable = history.undo_list.find(change =>
   257         change.is_finished && is_assigned(change.current.get_finished))
   258       require(found_stable.isDefined)
   259       val stable = found_stable.get
   260       val latest = history.undo_list.head
   261 
   262       val edits =
   263         (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
   264             (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
   265       lazy val reverse_edits = edits.reverse
   266 
   267       new Snapshot
   268       {
   269         val version = stable.current.get_finished
   270         val node = version.nodes(name)
   271         val is_outdated = !(pending_edits.isEmpty && latest == stable)
   272 
   273         def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
   274 
   275         def state(command: Command): Command.State =
   276           try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) }
   277           catch { case _: State.Fail => command.empty_state }
   278 
   279         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
   280         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   281 
   282         def select_markup[A](range: Text.Range)
   283           (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
   284         {
   285           val former_range = revert(range)
   286           for {
   287             (command, command_start) <- node.command_range(former_range)
   288             Text.Info(r0, x) <- state(command).markup.
   289               select((former_range - command_start).restrict(command.range)) {
   290                 case Text.Info(r0, info)
   291                 if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
   292                   result(Text.Info(convert(r0 + command_start), info))
   293               } { default }
   294             val r = convert(r0 + command_start)
   295             if !r.is_singularity
   296           } yield Text.Info(r, x)
   297         }
   298       }
   299     }
   300   }
   301 }
   302