src/Pure/PIDE/document.scala
author wenzelm
Tue Aug 07 15:01:48 2012 +0200 (2012-08-07 ago)
changeset 48707 ba531af91148
parent 48706 e2b512024eab
child 48793 2d6691085b8d
permissions -rw-r--r--
simplified Document.Node.Header -- internalized errors;
     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   val ID = Properties.Value.Long
    20 
    21   type Version_ID = ID
    22   type Command_ID = ID
    23   type Exec_ID = ID
    24 
    25   val no_id: ID = 0
    26   val new_id = Counter()
    27 
    28 
    29 
    30   /** document structure **/
    31 
    32   /* individual nodes */
    33 
    34   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
    35   type Edit_Text = Edit[Text.Edit, Text.Perspective]
    36   type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
    37 
    38   object Node
    39   {
    40     sealed case class Header(
    41       imports: List[Name],
    42       keywords: Thy_Header.Keywords,
    43       uses: List[(String, Boolean)],
    44       errors: List[String] = Nil)
    45     {
    46       def error(msg: String): Header = copy(errors = errors ::: List(msg))
    47     }
    48 
    49     def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
    50 
    51     object Name
    52     {
    53       val empty = Name("", "", "")
    54       def apply(path: Path): Name =
    55       {
    56         val node = path.implode
    57         val dir = path.dir.implode
    58         val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
    59         Name(node, dir, theory)
    60       }
    61 
    62       object Ordering extends scala.math.Ordering[Name]
    63       {
    64         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
    65       }
    66     }
    67     sealed case class Name(node: String, dir: String, theory: String)
    68     {
    69       override def hashCode: Int = node.hashCode
    70       override def equals(that: Any): Boolean =
    71         that match {
    72           case other: Name => node == other.node
    73           case _ => false
    74         }
    75       override def toString: String = theory
    76     }
    77 
    78     sealed abstract class Edit[A, B]
    79     {
    80       def foreach(f: A => Unit)
    81       {
    82         this match {
    83           case Edits(es) => es.foreach(f)
    84           case _ =>
    85         }
    86       }
    87     }
    88     case class Clear[A, B]() extends Edit[A, B]
    89     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    90     case class Deps[A, B](header: Header) extends Edit[A, B]
    91     case class Perspective[A, B](perspective: B) extends Edit[A, B]
    92 
    93     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    94       : Iterator[(Command, Text.Offset)] =
    95     {
    96       var i = offset
    97       for (command <- commands) yield {
    98         val start = i
    99         i += command.length
   100         (command, start)
   101       }
   102     }
   103 
   104     private val block_size = 1024
   105 
   106     val empty: Node = new Node()
   107   }
   108 
   109   final class Node private(
   110     val header: Node.Header = Node.bad_header("Bad theory header"),
   111     val perspective: Command.Perspective = Command.Perspective.empty,
   112     val blobs: Map[String, Blob] = Map.empty,
   113     val commands: Linear_Set[Command] = Linear_Set.empty)
   114   {
   115     def clear: Node = new Node(header = header)
   116 
   117     def update_header(new_header: Node.Header): Node =
   118       new Node(new_header, perspective, blobs, commands)
   119 
   120     def update_perspective(new_perspective: Command.Perspective): Node =
   121       new Node(header, new_perspective, blobs, commands)
   122 
   123     def update_blobs(new_blobs: Map[String, Blob]): Node =
   124       new Node(header, perspective, new_blobs, commands)
   125 
   126     def update_commands(new_commands: Linear_Set[Command]): Node =
   127       new Node(header, perspective, blobs, new_commands)
   128 
   129 
   130     /* commands */
   131 
   132     private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
   133     {
   134       val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
   135       var next_block = 0
   136       var last_stop = 0
   137       for ((command, start) <- Node.command_starts(commands.iterator)) {
   138         last_stop = start + command.length
   139         while (last_stop + 1 > next_block) {
   140           blocks += (command -> start)
   141           next_block += Node.block_size
   142         }
   143       }
   144       (blocks.toArray, Text.Range(0, last_stop))
   145     }
   146 
   147     def full_range: Text.Range = full_index._2
   148 
   149     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
   150     {
   151       if (!commands.isEmpty && full_range.contains(i)) {
   152         val (cmd0, start0) = full_index._1(i / Node.block_size)
   153         Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
   154           case (cmd, start) => start + cmd.length <= i }
   155       }
   156       else Iterator.empty
   157     }
   158 
   159     def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
   160       command_range(range.start) takeWhile { case (_, start) => start < range.stop }
   161 
   162     def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
   163     {
   164       val range = command_range(i)
   165       if (range.hasNext) Some(range.next) else None
   166     }
   167 
   168     def command_start(cmd: Command): Option[Text.Offset] =
   169       Node.command_starts(commands.iterator).find(_._1 == cmd).map(_._2)
   170   }
   171 
   172 
   173   /* development graph */
   174 
   175   object Nodes
   176   {
   177     val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering))
   178   }
   179 
   180   final class Nodes private(graph: Graph[Node.Name, Node])
   181   {
   182     def get_name(s: String): Option[Node.Name] =
   183       graph.keys.find(name => name.node == s)
   184 
   185     def apply(name: Node.Name): Node =
   186       graph.default_node(name, Node.empty).get_node(name)
   187 
   188     def + (entry: (Node.Name, Node)): Nodes =
   189     {
   190       val (name, node) = entry
   191       val imports = node.header.imports
   192       val graph1 =
   193         (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
   194       val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
   195       val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
   196       new Nodes(graph3.map_node(name, _ => node))
   197     }
   198 
   199     def entries: Iterator[(Node.Name, Node)] =
   200       graph.entries.map({ case (name, (node, _)) => (name, node) })
   201 
   202     def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
   203     def topological_order: List[Node.Name] = graph.topological_order
   204   }
   205 
   206 
   207 
   208   /** versioning **/
   209 
   210   /* particular document versions */
   211 
   212   object Version
   213   {
   214     val init: Version = new Version()
   215 
   216     def make(syntax: Outer_Syntax, nodes: Nodes): Version =
   217       new Version(new_id(), syntax, nodes)
   218   }
   219 
   220   final class Version private(
   221     val id: Version_ID = no_id,
   222     val syntax: Outer_Syntax = Outer_Syntax.empty,
   223     val nodes: Nodes = Nodes.empty)
   224   {
   225     def is_init: Boolean = id == no_id
   226   }
   227 
   228 
   229   /* changes of plain text, eventually resulting in document edits */
   230 
   231   object Change
   232   {
   233     val init: Change = new Change()
   234 
   235     def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
   236       new Change(Some(previous), edits, version)
   237   }
   238 
   239   final class Change private(
   240     val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
   241     val edits: List[Edit_Text] = Nil,
   242     val version: Future[Version] = Future.value(Version.init))
   243   {
   244     def is_finished: Boolean =
   245       (previous match { case None => true case Some(future) => future.is_finished }) &&
   246       version.is_finished
   247 
   248     def truncate: Change = new Change(None, Nil, version)
   249   }
   250 
   251 
   252   /* history navigation */
   253 
   254   object History
   255   {
   256     val init: History = new History()
   257   }
   258 
   259   final class History private(
   260     val undo_list: List[Change] = List(Change.init))  // non-empty list
   261   {
   262     def tip: Change = undo_list.head
   263     def + (change: Change): History = new History(change :: undo_list)
   264 
   265     def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] =
   266     {
   267       val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1
   268       val (retained, dropped) = undo_list.splitAt(n max retain)
   269 
   270       retained.splitAt(retained.length - 1) match {
   271         case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate)))
   272         case _ => None
   273       }
   274     }
   275   }
   276 
   277 
   278 
   279   /** global state -- document structure, execution process, editing history **/
   280 
   281   abstract class Snapshot
   282   {
   283     val state: State
   284     val version: Version
   285     val node: Node
   286     val is_outdated: Boolean
   287     def convert(i: Text.Offset): Text.Offset
   288     def convert(range: Text.Range): Text.Range
   289     def revert(i: Text.Offset): Text.Offset
   290     def revert(range: Text.Range): Text.Range
   291     def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
   292       result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
   293     def select_markup[A](range: Text.Range, elements: Option[Set[String]],
   294       result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
   295   }
   296 
   297   type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])]  // exec state assignment
   298 
   299   object State
   300   {
   301     class Fail(state: State) extends Exception
   302 
   303     object Assignment
   304     {
   305       val init: Assignment = new Assignment()
   306     }
   307 
   308     final class Assignment private(
   309       val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
   310       val is_finished: Boolean = false)
   311     {
   312       def check_finished: Assignment = { require(is_finished); this }
   313       def unfinished: Assignment = new Assignment(command_execs, false)
   314 
   315       def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])]): Assignment =
   316       {
   317         require(!is_finished)
   318         val command_execs1 =
   319           (command_execs /: add_command_execs) {
   320             case (res, (command_id, None)) => res - command_id
   321             case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
   322           }
   323         new Assignment(command_execs1, true)
   324       }
   325     }
   326 
   327     val init: State =
   328       State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
   329   }
   330 
   331   final case class State private(
   332     val versions: Map[Version_ID, Version] = Map.empty,
   333     val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
   334     val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution
   335     val assignments: Map[Version_ID, State.Assignment] = Map.empty,
   336     val history: History = History.init)
   337   {
   338     private def fail[A]: A = throw new State.Fail(this)
   339 
   340     def define_version(version: Version, assignment: State.Assignment): State =
   341     {
   342       val id = version.id
   343       copy(versions = versions + (id -> version),
   344         assignments = assignments + (id -> assignment.unfinished))
   345     }
   346 
   347     def define_command(command: Command): State =
   348     {
   349       val id = command.id
   350       copy(commands = commands + (id -> command.empty_state))
   351     }
   352 
   353     def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
   354 
   355     def find_command(version: Version, id: ID): Option[(Node, Command)] =
   356       commands.get(id) orElse execs.get(id) match {
   357         case None => None
   358         case Some(st) =>
   359           val command = st.command
   360           val node = version.nodes(command.node_name)
   361           Some((node, command))
   362       }
   363 
   364     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
   365     def the_command_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
   366     def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
   367     def the_assignment(version: Version): State.Assignment =
   368       assignments.getOrElse(version.id, fail)
   369 
   370     def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
   371       execs.get(id) match {
   372         case Some(st) =>
   373           val new_st = st + message
   374           (new_st, copy(execs = execs + (id -> new_st)))
   375         case None =>
   376           commands.get(id) match {
   377             case Some(st) =>
   378               val new_st = st + message
   379               (new_st, copy(commands = commands + (id -> new_st)))
   380             case None => fail
   381           }
   382       }
   383 
   384     def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) =
   385     {
   386       val version = the_version(id)
   387 
   388       val (changed_commands, new_execs) =
   389         ((Nil: List[Command], execs) /: command_execs) {
   390           case ((commands1, execs1), (cmd_id, exec)) =>
   391             val st = the_command_state(cmd_id)
   392             val commands2 = st.command :: commands1
   393             val execs2 =
   394               exec match {
   395                 case None => execs1
   396                 case Some(exec_id) => execs1 + (exec_id -> st)
   397               }
   398             (commands2, execs2)
   399         }
   400       val new_assignment = the_assignment(version).assign(command_execs)
   401       val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
   402 
   403       (changed_commands, new_state)
   404     }
   405 
   406     def is_assigned(version: Version): Boolean =
   407       assignments.get(version.id) match {
   408         case Some(assgn) => assgn.is_finished
   409         case None => false
   410       }
   411 
   412     def is_stable(change: Change): Boolean =
   413       change.is_finished && is_assigned(change.version.get_finished)
   414 
   415     def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
   416     def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
   417     def tip_stable: Boolean = is_stable(history.tip)
   418     def tip_version: Version = history.tip.version.get_finished
   419 
   420     def continue_history(
   421         previous: Future[Version],
   422         edits: List[Edit_Text],
   423         version: Future[Version]): (Change, State) =
   424     {
   425       val change = Change.make(previous, edits, version)
   426       (change, copy(history = history + change))
   427     }
   428 
   429     def prune_history(retain: Int = 0): (List[Version], State) =
   430     {
   431       history.prune(is_stable, retain) match {
   432         case Some((dropped, history1)) =>
   433           val dropped_versions = dropped.map(change => change.version.get_finished)
   434           val state1 = copy(history = history1)
   435           (dropped_versions, state1)
   436         case None => fail
   437       }
   438     }
   439 
   440     def removed_versions(removed: List[Version_ID]): State =
   441     {
   442       val versions1 = versions -- removed
   443       val assignments1 = assignments -- removed
   444       var commands1 = Map.empty[Command_ID, Command.State]
   445       var execs1 = Map.empty[Exec_ID, Command.State]
   446       for {
   447         (version_id, version) <- versions1.iterator
   448         command_execs = assignments1(version_id).command_execs
   449         (_, node) <- version.nodes.entries
   450         command <- node.commands.iterator
   451       } {
   452         val id = command.id
   453         if (!commands1.isDefinedAt(id) && commands.isDefinedAt(id))
   454           commands1 += (id -> commands(id))
   455         if (command_execs.isDefinedAt(id)) {
   456           val exec_id = command_execs(id)
   457           if (!execs1.isDefinedAt(exec_id) && execs.isDefinedAt(exec_id))
   458             execs1 += (exec_id -> execs(exec_id))
   459         }
   460       }
   461       copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
   462     }
   463 
   464     def command_state(version: Version, command: Command): Command.State =
   465     {
   466       require(is_assigned(version))
   467       try {
   468         the_exec(the_assignment(version).check_finished.command_execs
   469           .getOrElse(command.id, fail))
   470       }
   471       catch {
   472         case _: State.Fail =>
   473           try { the_command_state(command.id) }
   474           catch { case _: State.Fail => command.empty_state }
   475       }
   476     }
   477 
   478 
   479     // persistent user-view
   480     def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
   481     {
   482       val stable = recent_stable
   483       val latest = history.tip
   484 
   485       // FIXME proper treatment of removed nodes
   486       val edits =
   487         (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
   488             (for ((a, Node.Edits(es)) <- change.edits if a == name) yield es).flatten ::: edits)
   489       lazy val reverse_edits = edits.reverse
   490 
   491       new Snapshot
   492       {
   493         val state = State.this
   494         val version = stable.version.get_finished
   495         val node = version.nodes(name)
   496         val is_outdated = !(pending_edits.isEmpty && latest == stable)
   497 
   498         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
   499         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   500         def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
   501         def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
   502 
   503         def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
   504           result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
   505         {
   506           val former_range = revert(range)
   507           for {
   508             (command, command_start) <- node.command_range(former_range).toStream
   509             Text.Info(r0, a) <- state.command_state(version, command).markup.
   510               cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
   511                 {
   512                   case (a, Text.Info(r0, b))
   513                   if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
   514                     result((a, Text.Info(convert(r0 + command_start), b)))
   515                 })
   516           } yield Text.Info(convert(r0 + command_start), a)
   517         }
   518 
   519         def select_markup[A](range: Text.Range, elements: Option[Set[String]],
   520           result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
   521         {
   522           val result1 =
   523             new PartialFunction[(Option[A], Text.Markup), Option[A]] {
   524               def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
   525               def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
   526             }
   527           for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
   528             yield Text.Info(r, x)
   529         }
   530       }
   531     }
   532   }
   533 }
   534