1/* Title: Pure/PIDE/document.scala 2 Author: Makarius 3 4Document as collection of named nodes, each consisting of an editable 5list of commands, associated with asynchronous execution process. 6*/ 7 8package isabelle 9 10 11import scala.collection.mutable 12 13 14object Document 15{ 16 /** document structure **/ 17 18 /* overlays -- print functions with arguments */ 19 20 object Overlays 21 { 22 val empty = new Overlays(Map.empty) 23 } 24 25 final class Overlays private(rep: Map[Node.Name, Node.Overlays]) 26 { 27 def apply(name: Node.Name): Node.Overlays = 28 rep.getOrElse(name, Node.Overlays.empty) 29 30 private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays = 31 { 32 val node_overlays = f(apply(name)) 33 new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays)) 34 } 35 36 def insert(command: Command, fn: String, args: List[String]): Overlays = 37 update(command.node_name, _.insert(command, fn, args)) 38 39 def remove(command: Command, fn: String, args: List[String]): Overlays = 40 update(command.node_name, _.remove(command, fn, args)) 41 42 override def toString: String = rep.mkString("Overlays(", ",", ")") 43 } 44 45 46 /* document blobs: auxiliary files */ 47 48 sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) 49 { 50 def unchanged: Blob = copy(changed = false) 51 } 52 53 object Blobs 54 { 55 def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs) 56 val empty: Blobs = apply(Map.empty) 57 } 58 59 final class Blobs private(blobs: Map[Node.Name, Blob]) 60 { 61 def get(name: Node.Name): Option[Blob] = blobs.get(name) 62 63 def changed(name: Node.Name): Boolean = 64 get(name) match { 65 case Some(blob) => blob.changed 66 case None => false 67 } 68 69 override def toString: String = blobs.mkString("Blobs(", ",", ")") 70 } 71 72 73 /* document nodes: theories and auxiliary files */ 74 75 type Edit[A, B] = (Node.Name, Node.Edit[A, B]) 76 type Edit_Text = Edit[Text.Edit, Text.Perspective] 77 type Edit_Command = Edit[Command.Edit, Command.Perspective] 78 79 object Node 80 { 81 /* header and name */ 82 83 sealed case class Header( 84 imports_pos: List[(Name, Position.T)] = Nil, 85 keywords: Thy_Header.Keywords = Nil, 86 abbrevs: Thy_Header.Abbrevs = Nil, 87 errors: List[String] = Nil) 88 { 89 def imports: List[Name] = imports_pos.map(_._1) 90 91 def append_errors(msgs: List[String]): Header = 92 copy(errors = errors ::: msgs) 93 94 def cat_errors(msg2: String): Header = 95 copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2))) 96 } 97 98 val no_header = Header() 99 def bad_header(msg: String): Header = Header(errors = List(msg)) 100 101 object Name 102 { 103 val empty = Name("") 104 105 object Ordering extends scala.math.Ordering[Name] 106 { 107 def compare(name1: Name, name2: Name): Int = name1.node compare name2.node 108 } 109 110 type Graph[A] = isabelle.Graph[Node.Name, A] 111 112 def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] = 113 Graph.make(entries, symmetric = true)(Ordering) 114 } 115 116 sealed case class Name(node: String, master_dir: String = "", theory: String = "") 117 { 118 override def hashCode: Int = node.hashCode 119 override def equals(that: Any): Boolean = 120 that match { 121 case other: Name => node == other.node 122 case _ => false 123 } 124 125 def path: Path = Path.explode(File.standard_path(node)) 126 def master_dir_path: Path = Path.explode(File.standard_path(master_dir)) 127 128 def is_theory: Boolean = theory.nonEmpty 129 130 def theory_base_name: String = Long_Name.base_name(theory) 131 132 override def toString: String = if (is_theory) theory else node 133 134 def map(f: String => String): Name = copy(f(node), f(master_dir), theory) 135 def map_theory(f: String => String): Name = copy(node, master_dir, f(theory)) 136 137 def json: JSON.Object.T = 138 JSON.Object("node_name" -> node, "theory_name" -> theory) 139 } 140 141 sealed case class Entry(name: Node.Name, header: Node.Header) 142 { 143 def map(f: String => String): Entry = copy(name = name.map(f)) 144 145 override def toString: String = name.toString 146 } 147 148 149 /* node overlays */ 150 151 object Overlays 152 { 153 val empty = new Overlays(Multi_Map.empty) 154 } 155 156 final class Overlays private(rep: Multi_Map[Command, (String, List[String])]) 157 { 158 def commands: Set[Command] = rep.keySet 159 def is_empty: Boolean = rep.isEmpty 160 def dest: List[(Command, (String, List[String]))] = rep.iterator.toList 161 def insert(cmd: Command, fn: String, args: List[String]): Overlays = 162 new Overlays(rep.insert(cmd, (fn, args))) 163 def remove(cmd: Command, fn: String, args: List[String]): Overlays = 164 new Overlays(rep.remove(cmd, (fn, args))) 165 166 override def toString: String = rep.mkString("Node.Overlays(", ",", ")") 167 } 168 169 170 /* edits */ 171 172 sealed abstract class Edit[A, B] 173 { 174 def foreach(f: A => Unit) 175 { 176 this match { 177 case Edits(es) => es.foreach(f) 178 case _ => 179 } 180 } 181 182 def is_void: Boolean = 183 this match { 184 case Edits(Nil) => true 185 case _ => false 186 } 187 } 188 case class Blob[A, B](blob: Document.Blob) extends Edit[A, B] 189 190 case class Edits[A, B](edits: List[A]) extends Edit[A, B] 191 case class Deps[A, B](header: Header) extends Edit[A, B] 192 case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B] 193 194 195 /* perspective */ 196 197 type Perspective_Text = Perspective[Text.Edit, Text.Perspective] 198 type Perspective_Command = Perspective[Command.Edit, Command.Perspective] 199 200 val no_perspective_text: Perspective_Text = 201 Perspective(false, Text.Perspective.empty, Overlays.empty) 202 203 val no_perspective_command: Perspective_Command = 204 Perspective(false, Command.Perspective.empty, Overlays.empty) 205 206 def is_no_perspective_text(perspective: Perspective_Text): Boolean = 207 !perspective.required && 208 perspective.visible.is_empty && 209 perspective.overlays.is_empty 210 211 def is_no_perspective_command(perspective: Perspective_Command): Boolean = 212 !perspective.required && 213 perspective.visible.is_empty && 214 perspective.overlays.is_empty 215 216 217 /* commands */ 218 219 object Commands 220 { 221 def apply(commands: Linear_Set[Command]): Commands = new Commands(commands) 222 val empty: Commands = apply(Linear_Set.empty) 223 224 def starts(commands: Iterator[Command], offset: Text.Offset = 0) 225 : Iterator[(Command, Text.Offset)] = 226 { 227 var i = offset 228 for (command <- commands) yield { 229 val start = i 230 i += command.length 231 (command, start) 232 } 233 } 234 235 def starts_pos(commands: Iterator[Command], pos: Token.Pos = Token.Pos.start) 236 : Iterator[(Command, Token.Pos)] = 237 { 238 var p = pos 239 for (command <- commands) yield { 240 val start = p 241 p = (p /: command.span.content)(_.advance(_)) 242 (command, start) 243 } 244 } 245 246 private val block_size = 256 247 } 248 249 final class Commands private(val commands: Linear_Set[Command]) 250 { 251 lazy val load_commands: List[Command] = 252 commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList 253 254 private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = 255 { 256 val blocks = new mutable.ListBuffer[(Command, Text.Offset)] 257 var next_block = 0 258 var last_stop = 0 259 for ((command, start) <- Commands.starts(commands.iterator)) { 260 last_stop = start + command.length 261 while (last_stop + 1 > next_block) { 262 blocks += (command -> start) 263 next_block += Commands.block_size 264 } 265 } 266 (blocks.toArray, Text.Range(0, last_stop)) 267 } 268 269 private def full_range: Text.Range = full_index._2 270 271 def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = 272 { 273 if (commands.nonEmpty && full_range.contains(i)) { 274 val (cmd0, start0) = full_index._1(i / Commands.block_size) 275 Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile { 276 case (cmd, start) => start + cmd.length <= i } 277 } 278 else Iterator.empty 279 } 280 } 281 282 val empty: Node = new Node() 283 } 284 285 final class Node private( 286 val get_blob: Option[Document.Blob] = None, 287 val header: Node.Header = Node.no_header, 288 val syntax: Option[Outer_Syntax] = None, 289 val text_perspective: Text.Perspective = Text.Perspective.empty, 290 val perspective: Node.Perspective_Command = Node.no_perspective_command, 291 _commands: Node.Commands = Node.Commands.empty) 292 { 293 def is_empty: Boolean = 294 get_blob.isEmpty && 295 header == Node.no_header && 296 text_perspective.is_empty && 297 Node.is_no_perspective_command(perspective) && 298 commands.isEmpty 299 300 def has_header: Boolean = header != Node.no_header 301 302 override def toString: String = 303 if (is_empty) "empty" 304 else if (get_blob.isDefined) "blob" 305 else "node" 306 307 def commands: Linear_Set[Command] = _commands.commands 308 def load_commands: List[Command] = _commands.load_commands 309 def load_commands_changed(doc_blobs: Blobs): Boolean = 310 load_commands.exists(_.blobs_changed(doc_blobs)) 311 312 def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged)) 313 314 def update_header(new_header: Node.Header): Node = 315 new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands) 316 317 def update_syntax(new_syntax: Option[Outer_Syntax]): Node = 318 new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands) 319 320 def update_perspective( 321 new_text_perspective: Text.Perspective, 322 new_perspective: Node.Perspective_Command): Node = 323 new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands) 324 325 def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] = 326 Node.Perspective(perspective.required, text_perspective, perspective.overlays) 327 328 def same_perspective( 329 other_text_perspective: Text.Perspective, 330 other_perspective: Node.Perspective_Command): Boolean = 331 text_perspective == other_text_perspective && 332 perspective.required == other_perspective.required && 333 perspective.visible.same(other_perspective.visible) && 334 perspective.overlays == other_perspective.overlays 335 336 def update_commands(new_commands: Linear_Set[Command]): Node = 337 if (new_commands eq _commands.commands) this 338 else 339 new Node(get_blob, header, syntax, text_perspective, perspective, 340 Node.Commands(new_commands)) 341 342 def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = 343 _commands.iterator(i) 344 345 def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] = 346 command_iterator(range.start) takeWhile { case (_, start) => start < range.stop } 347 348 def command_start(cmd: Command): Option[Text.Offset] = 349 Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2) 350 351 def source: String = 352 get_blob match { 353 case Some(blob) => blob.source 354 case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString 355 } 356 } 357 358 359 /* development graph */ 360 361 object Nodes 362 { 363 val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering)) 364 } 365 366 final class Nodes private(graph: Graph[Node.Name, Node]) 367 { 368 def apply(name: Node.Name): Node = 369 graph.default_node(name, Node.empty).get_node(name) 370 371 def is_suppressed(name: Node.Name): Boolean = 372 { 373 val graph1 = graph.default_node(name, Node.empty) 374 graph1.is_maximal(name) && graph1.get_node(name).is_empty 375 } 376 377 def purge_suppressed: Option[Nodes] = 378 graph.keys_iterator.filter(is_suppressed(_)).toList match { 379 case Nil => None 380 case del => Some(new Nodes((graph /: del)(_.del_node(_)))) 381 } 382 383 def + (entry: (Node.Name, Node)): Nodes = 384 { 385 val (name, node) = entry 386 val imports = node.header.imports 387 val graph1 = 388 (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty)) 389 val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name)) 390 val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name)) 391 new Nodes(graph3.map_node(name, _ => node)) 392 } 393 394 def domain: Set[Node.Name] = graph.domain 395 396 def iterator: Iterator[(Node.Name, Node)] = 397 graph.iterator.map({ case (name, (node, _)) => (name, node) }) 398 399 def theory_name(theory: String): Option[Node.Name] = 400 graph.keys_iterator.find(name => name.theory == theory) 401 402 def commands_loading(file_name: Node.Name): List[Command] = 403 (for { 404 (_, node) <- iterator 405 cmd <- node.load_commands.iterator 406 name <- cmd.blobs_names.iterator 407 if name == file_name 408 } yield cmd).toList 409 410 def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names) 411 def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds(names).reverse 412 def topological_order: List[Node.Name] = graph.topological_order 413 414 override def toString: String = topological_order.mkString("Nodes(", ",", ")") 415 } 416 417 418 419 /** versioning **/ 420 421 /* particular document versions */ 422 423 object Version 424 { 425 val init: Version = new Version() 426 def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes) 427 428 def purge_future(versions: Map[Document_ID.Version, Version], future: Future[Version]) 429 : Future[Version] = 430 { 431 if (future.is_finished) { 432 val version = future.join 433 versions.get(version.id) match { 434 case Some(version1) if !(version eq version1) => Future.value(version1) 435 case _ => future 436 } 437 } 438 else future 439 } 440 441 def purge_suppressed( 442 versions: Map[Document_ID.Version, Version]): Map[Document_ID.Version, Version] = 443 { 444 (versions /: 445 (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)))(_ + _) 446 } 447 } 448 449 final class Version private( 450 val id: Document_ID.Version = Document_ID.none, 451 val nodes: Nodes = Nodes.empty) 452 { 453 override def toString: String = "Version(" + id + ")" 454 455 def purge_suppressed: Option[Version] = 456 nodes.purge_suppressed.map(new Version(id, _)) 457 } 458 459 460 /* changes of plain text, eventually resulting in document edits */ 461 462 object Change 463 { 464 val init: Change = new Change() 465 466 def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change = 467 new Change(Some(previous), edits.reverse, version) 468 } 469 470 final class Change private( 471 val previous: Option[Future[Version]] = Some(Future.value(Version.init)), 472 val rev_edits: List[Edit_Text] = Nil, 473 val version: Future[Version] = Future.value(Version.init)) 474 { 475 def is_finished: Boolean = 476 (previous match { case None => true case Some(future) => future.is_finished }) && 477 version.is_finished 478 479 def truncate: Change = new Change(None, Nil, version) 480 481 def purge(versions: Map[Document_ID.Version, Version]): Option[Change] = 482 { 483 val previous1 = previous.map(Version.purge_future(versions, _)) 484 val version1 = Version.purge_future(versions, version) 485 if ((previous eq previous1) && (version eq version1)) None 486 else Some(new Change(previous1, rev_edits, version1)) 487 } 488 } 489 490 491 /* history navigation */ 492 493 object History 494 { 495 val init: History = new History() 496 } 497 498 final class History private( 499 val undo_list: List[Change] = List(Change.init)) // non-empty list 500 { 501 override def toString: String = "History(" + undo_list.length + ")" 502 503 def tip: Change = undo_list.head 504 def + (change: Change): History = new History(change :: undo_list) 505 506 def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] = 507 { 508 val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1 509 val (retained, dropped) = undo_list.splitAt(n max retain) 510 511 retained.splitAt(retained.length - 1) match { 512 case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate))) 513 case _ => None 514 } 515 } 516 517 def purge(versions: Map[Document_ID.Version, Version]): History = 518 { 519 val undo_list1 = undo_list.map(_.purge(versions)) 520 if (undo_list1.forall(_.isEmpty)) this 521 else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b)) 522 } 523 } 524 525 526 /* snapshot */ 527 528 object Snapshot 529 { 530 val init = State.init.snapshot() 531 } 532 533 abstract class Snapshot 534 { 535 def state: State 536 def version: Version 537 def is_outdated: Boolean 538 539 def convert(i: Text.Offset): Text.Offset 540 def revert(i: Text.Offset): Text.Offset 541 def convert(range: Text.Range): Text.Range 542 def revert(range: Text.Range): Text.Range 543 544 def node_name: Node.Name 545 def node: Node 546 def nodes: List[(Node.Name, Node)] 547 548 def commands_loading: List[Command] 549 def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] 550 def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] 551 552 def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body 553 def messages: List[(XML.Tree, Position.T)] 554 def exports: List[Export.Entry] 555 def exports_map: Map[String, Export.Entry] 556 557 def find_command(id: Document_ID.Generic): Option[(Node, Command)] 558 def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset) 559 : Option[Line.Node_Position] 560 561 def cumulate[A]( 562 range: Text.Range, 563 info: A, 564 elements: Markup.Elements, 565 result: List[Command.State] => (A, Text.Markup) => Option[A], 566 status: Boolean = false): List[Text.Info[A]] 567 568 def select[A]( 569 range: Text.Range, 570 elements: Markup.Elements, 571 result: List[Command.State] => Text.Markup => Option[A], 572 status: Boolean = false): List[Text.Info[A]] 573 574 def command_results(range: Text.Range): Command.Results 575 def command_results(command: Command): Command.Results 576 577 def command_id_map: Map[Document_ID.Generic, Command] 578 } 579 580 581 /* model */ 582 583 trait Session 584 { 585 def resources: Resources 586 } 587 588 trait Model 589 { 590 def session: Session 591 def is_stable: Boolean 592 def snapshot(): Snapshot 593 594 def node_name: Node.Name 595 def is_theory: Boolean = node_name.is_theory 596 override def toString: String = node_name.toString 597 598 def get_text(range: Text.Range): Option[String] 599 600 def node_required: Boolean 601 def get_blob: Option[Blob] 602 def bibtex_entries: List[Text.Info[String]] 603 604 def node_edits( 605 node_header: Node.Header, 606 text_edits: List[Text.Edit], 607 perspective: Node.Perspective_Text): List[Edit_Text] = 608 { 609 val edits: List[Node.Edit[Text.Edit, Text.Perspective]] = 610 get_blob match { 611 case None => 612 List( 613 Node.Deps( 614 if (session.resources.session_base.loaded_theory(node_name)) { 615 node_header.append_errors( 616 List("Cannot update finished theory " + quote(node_name.theory))) 617 } 618 else node_header), 619 Node.Edits(text_edits), perspective) 620 case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits)) 621 } 622 edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit)) 623 } 624 } 625 626 627 /** global state -- document structure, execution process, editing history **/ 628 629 type Assign_Update = 630 List[(Document_ID.Command, List[Document_ID.Exec])] // update of exec state assignment 631 632 object State 633 { 634 class Fail(state: State) extends Exception 635 636 object Assignment 637 { 638 val init: Assignment = new Assignment() 639 } 640 641 final class Assignment private( 642 val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty, 643 val is_finished: Boolean = false) 644 { 645 override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")" 646 647 def check_finished: Assignment = { require(is_finished); this } 648 def unfinished: Assignment = new Assignment(command_execs, false) 649 650 def assign(update: Assign_Update): Assignment = 651 { 652 require(!is_finished) 653 val command_execs1 = 654 (command_execs /: update) { 655 case (res, (command_id, exec_ids)) => 656 if (exec_ids.isEmpty) res - command_id 657 else res + (command_id -> exec_ids) 658 } 659 new Assignment(command_execs1, true) 660 } 661 } 662 663 val init: State = 664 State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2 665 } 666 667 final case class State private( 668 /*reachable versions*/ 669 versions: Map[Document_ID.Version, Version] = Map.empty, 670 /*inlined auxiliary files*/ 671 blobs: Set[SHA1.Digest] = Set.empty, 672 /*static markup from define_command*/ 673 commands: Map[Document_ID.Command, Command.State] = Map.empty, 674 /*dynamic markup from execution*/ 675 execs: Map[Document_ID.Exec, Command.State] = Map.empty, 676 /*command-exec assignment for each version*/ 677 assignments: Map[Document_ID.Version, State.Assignment] = Map.empty, 678 /*commands with markup produced by other commands (imm_succs)*/ 679 commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long, 680 /*explicit (linear) history*/ 681 history: History = History.init, 682 /*intermediate state between remove_versions/removed_versions*/ 683 removing_versions: Boolean = false) 684 { 685 override def toString: String = 686 "State(versions = " + versions.size + 687 ", blobs = " + blobs.size + 688 ", commands = " + commands.size + 689 ", execs = " + execs.size + 690 ", assignments = " + assignments.size + 691 ", commands_redirection = " + commands_redirection.size + 692 ", history = " + history.undo_list.size + 693 ", removing_versions = " + removing_versions + ")" 694 695 private def fail[A]: A = throw new State.Fail(this) 696 697 def define_version(version: Version, assignment: State.Assignment): State = 698 { 699 val id = version.id 700 copy(versions = versions + (id -> version), 701 assignments = assignments + (id -> assignment.unfinished)) 702 } 703 704 def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest) 705 def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest) 706 707 def define_command(command: Command): State = 708 { 709 val id = command.id 710 copy(commands = commands + (id -> command.init_state)) 711 } 712 713 def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id) 714 715 def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail) 716 def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail) 717 def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail) 718 def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) 719 720 def lookup_id(id: Document_ID.Generic): Option[Command.State] = 721 commands.get(id) orElse execs.get(id) 722 723 private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean = 724 id == st.command.id || 725 (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false }) 726 727 private def other_id(id: Document_ID.Generic) 728 : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = 729 lookup_id(id).map(st => ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk))) 730 731 private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] = 732 (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) => 733 graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) }) 734 735 def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache) 736 : (Command.State, State) = 737 { 738 execs.get(id) match { 739 case Some(st) => 740 val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache) 741 val execs1 = execs + (id -> new_st) 742 (new_st, copy(execs = execs1, commands_redirection = redirection(new_st))) 743 case None => 744 commands.get(id) match { 745 case Some(st) => 746 val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache) 747 val commands1 = commands + (id -> new_st) 748 (new_st, copy(commands = commands1, commands_redirection = redirection(new_st))) 749 case None => fail 750 } 751 } 752 } 753 754 def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) = 755 { 756 execs.get(id) match { 757 case Some(st) => 758 st.add_export(entry) match { 759 case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st))) 760 case None => fail 761 } 762 case None => 763 commands.get(id) match { 764 case Some(st) => 765 st.add_export(entry) match { 766 case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st))) 767 case None => fail 768 } 769 case None => fail 770 } 771 } 772 } 773 774 def node_exports(version: Version, node_name: Node.Name): Command.Exports = 775 Command.Exports.merge( 776 for { 777 command <- version.nodes(node_name).commands.iterator 778 st <- command_states(version, command).iterator 779 } yield st.exports) 780 781 def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) 782 : ((List[Node.Name], List[Command]), State) = 783 { 784 val version = the_version(id) 785 786 val edited_set = edited.toSet 787 val edited_nodes = 788 (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList 789 790 def upd(exec_id: Document_ID.Exec, st: Command.State) 791 : Option[(Document_ID.Exec, Command.State)] = 792 if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st) 793 794 val (changed_commands, new_execs) = 795 ((Nil: List[Command], execs) /: update) { 796 case ((commands1, execs1), (command_id, exec)) => 797 val st = the_static_state(command_id) 798 val command = st.command 799 val commands2 = command :: commands1 800 val execs2 = 801 exec match { 802 case Nil => execs1 803 case eval_id :: print_ids => 804 execs1 ++ upd(eval_id, st) ++ 805 (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up) 806 } 807 (commands2, execs2) 808 } 809 val new_assignment = the_assignment(version).assign(update) 810 val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) 811 812 ((edited_nodes, changed_commands), new_state) 813 } 814 815 def is_assigned(version: Version): Boolean = 816 assignments.get(version.id) match { 817 case Some(assgn) => assgn.is_finished 818 case None => false 819 } 820 821 def is_stable(change: Change): Boolean = 822 change.is_finished && is_assigned(change.version.get_finished) 823 824 def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail 825 def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail 826 def stable_tip_version: Option[Version] = 827 if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None 828 829 def continue_history( 830 previous: Future[Version], 831 edits: List[Edit_Text], 832 version: Future[Version]): State = 833 { 834 val change = Change.make(previous, edits, version) 835 copy(history = history + change) 836 } 837 838 def remove_versions(retain: Int = 0): (List[Version], State) = 839 { 840 history.prune(is_stable, retain) match { 841 case Some((dropped, history1)) => 842 val old_versions = dropped.map(change => change.version.get_finished) 843 val removing = old_versions.nonEmpty 844 val state1 = copy(history = history1, removing_versions = removing) 845 (old_versions, state1) 846 case None => fail 847 } 848 } 849 850 def removed_versions(removed: List[Document_ID.Version]): State = 851 { 852 val versions1 = Version.purge_suppressed(versions -- removed) 853 854 val assignments1 = assignments -- removed 855 var blobs1_names = Set.empty[Node.Name] 856 var blobs1 = Set.empty[SHA1.Digest] 857 var commands1 = Map.empty[Document_ID.Command, Command.State] 858 var execs1 = Map.empty[Document_ID.Exec, Command.State] 859 for { 860 (version_id, version) <- versions1.iterator 861 command_execs = assignments1(version_id).command_execs 862 (_, node) <- version.nodes.iterator 863 command <- node.commands.iterator 864 } { 865 for ((name, digest) <- command.blobs_defined) { 866 blobs1_names += name 867 blobs1 += digest 868 } 869 870 if (!commands1.isDefinedAt(command.id)) 871 commands.get(command.id).foreach(st => commands1 += (command.id -> st)) 872 873 for (exec_id <- command_execs.getOrElse(command.id, Nil)) { 874 if (!execs1.isDefinedAt(exec_id)) 875 execs.get(exec_id).foreach(st => execs1 += (exec_id -> st)) 876 } 877 } 878 879 copy( 880 versions = versions1, 881 blobs = blobs1, 882 commands = commands1, 883 execs = execs1, 884 commands_redirection = commands_redirection.restrict(commands1.keySet), 885 assignments = assignments1, 886 history = history.purge(versions1), 887 removing_versions = false) 888 } 889 890 def command_id_map(version: Version, commands: Iterable[Command]) 891 : Map[Document_ID.Generic, Command] = 892 { 893 require(is_assigned(version)) 894 val assignment = the_assignment(version).check_finished 895 (for { 896 command <- commands.iterator 897 id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator 898 } yield (id -> command)).toMap 899 } 900 901 def command_maybe_consolidated(version: Version, command: Command): Boolean = 902 { 903 require(is_assigned(version)) 904 try { 905 the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match { 906 case eval_id :: print_ids => 907 the_dynamic_state(eval_id).maybe_consolidated && 908 !print_ids.exists(print_id => the_dynamic_state(print_id).consolidating) 909 case Nil => false 910 } 911 } 912 catch { case _: State.Fail => false } 913 } 914 915 private def command_states_self(version: Version, command: Command) 916 : List[(Document_ID.Generic, Command.State)] = 917 { 918 require(is_assigned(version)) 919 try { 920 the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) 921 .map(id => id -> the_dynamic_state(id)) match { 922 case Nil => fail 923 case res => res 924 } 925 } 926 catch { 927 case _: State.Fail => 928 try { List(command.id -> the_static_state(command.id)) } 929 catch { case _: State.Fail => List(command.id -> command.init_state) } 930 } 931 } 932 933 def command_states(version: Version, command: Command): List[Command.State] = 934 { 935 val self = command_states_self(version, command) 936 val others = 937 if (commands_redirection.defined(command.id)) { 938 (for { 939 command_id <- commands_redirection.imm_succs(command.id).iterator 940 (id, st) <- command_states_self(version, the_static_state(command_id).command) 941 if !self.exists(_._1 == id) 942 } yield (id, st)).toMap.valuesIterator.toList 943 } 944 else Nil 945 self.map(_._2) ::: others.flatMap(_.redirect(command)) 946 } 947 948 def command_results(version: Version, command: Command): Command.Results = 949 Command.State.merge_results(command_states(version, command)) 950 951 def command_markup(version: Version, command: Command, index: Command.Markup_Index, 952 range: Text.Range, elements: Markup.Elements): Markup_Tree = 953 Command.State.merge_markup(command_states(version, command), index, range, elements) 954 955 def markup_to_XML( 956 version: Version, 957 node_name: Node.Name, 958 range: Text.Range, 959 elements: Markup.Elements): XML.Body = 960 { 961 val node = version.nodes(node_name) 962 if (node_name.is_theory) { 963 val markup_index = Command.Markup_Index.markup 964 (for { 965 command <- node.commands.iterator 966 command_range <- command.range.try_restrict(range).iterator 967 markup = command_markup(version, command, markup_index, command_range, elements) 968 tree <- markup.to_XML(command_range, command.source, elements).iterator 969 } yield tree).toList 970 } 971 else { 972 val node_source = node.source 973 Text.Range(0, node_source.length).try_restrict(range) match { 974 case None => Nil 975 case Some(node_range) => 976 val markup = 977 version.nodes.commands_loading(node_name).headOption match { 978 case None => Markup_Tree.empty 979 case Some(command) => 980 val chunk_name = Symbol.Text_Chunk.File(node_name.node) 981 val markup_index = Command.Markup_Index(false, chunk_name) 982 command_markup(version, command, markup_index, node_range, elements) 983 } 984 markup.to_XML(node_range, node_source, elements) 985 } 986 } 987 } 988 989 def node_initialized(version: Version, name: Node.Name): Boolean = 990 name.is_theory && 991 (version.nodes(name).commands.iterator.find(_.potentially_initialized) match { 992 case None => false 993 case Some(command) => command_states(version, command).headOption.exists(_.initialized) 994 }) 995 996 def node_maybe_consolidated(version: Version, name: Node.Name): Boolean = 997 name.is_theory && 998 version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _)) 999 1000 def node_consolidated(version: Version, name: Node.Name): Boolean = 1001 !name.is_theory || 1002 { 1003 val it = version.nodes(name).commands.reverse.iterator 1004 it.hasNext && command_states(version, it.next).exists(_.consolidated) 1005 } 1006 1007 // persistent user-view 1008 def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil) 1009 : Snapshot = 1010 { 1011 val stable = recent_stable 1012 val latest = history.tip 1013 1014 1015 /* pending edits and unstable changes */ 1016 1017 val rev_pending_changes = 1018 for { 1019 change <- history.undo_list.takeWhile(_ != stable) 1020 (a, edits) <- change.rev_edits 1021 if a == name 1022 } yield edits 1023 1024 val edits = 1025 (pending_edits /: rev_pending_changes)({ 1026 case (edits, Node.Edits(es)) => es ::: edits 1027 case (edits, _) => edits 1028 }) 1029 lazy val reverse_edits = edits.reverse 1030 1031 new Snapshot 1032 { 1033 /* global information */ 1034 1035 val state: State = State.this 1036 val version: Version = stable.version.get_finished 1037 val is_outdated: Boolean = pending_edits.nonEmpty || latest != stable 1038 1039 1040 /* local node content */ 1041 1042 def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) 1043 def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) 1044 1045 def convert(range: Text.Range) = range.map(convert(_)) 1046 def revert(range: Text.Range) = range.map(revert(_)) 1047 1048 val node_name: Node.Name = name 1049 val node: Node = version.nodes(name) 1050 1051 def nodes: List[(Node.Name, Node)] = 1052 (node_name :: node.load_commands.flatMap(_.blobs_names)). 1053 map(name => (name, version.nodes(name))) 1054 1055 val commands_loading: List[Command] = 1056 if (node_name.is_theory) Nil 1057 else version.nodes.commands_loading(node_name) 1058 1059 def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] = 1060 (for { 1061 cmd <- node.load_commands.iterator 1062 blob_name <- cmd.blobs_names.iterator 1063 if pred(blob_name) 1064 start <- node.command_start(cmd) 1065 } yield convert(cmd.core_range + start)).toList 1066 1067 def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] = 1068 if (other_node_name.is_theory) { 1069 val other_node = version.nodes(other_node_name) 1070 val iterator = other_node.command_iterator(revert(offset) max 0) 1071 if (iterator.hasNext) { 1072 val (command0, _) = iterator.next 1073 other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored) 1074 } 1075 else other_node.commands.reverse.iterator.find(command => !command.is_ignored) 1076 } 1077 else version.nodes.commands_loading(other_node_name).headOption 1078 1079 def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body = 1080 state.markup_to_XML(version, node_name, range, elements) 1081 1082 lazy val messages: List[(XML.Tree, Position.T)] = 1083 (for { 1084 (command, start) <- 1085 Document.Node.Commands.starts_pos( 1086 node.commands.iterator, Token.Pos.file(node_name.node)) 1087 pos = command.span.keyword_pos(start).position(command.span.name) 1088 (_, tree) <- state.command_results(version, command).iterator 1089 } yield (tree, pos)).toList 1090 1091 lazy val exports: List[Export.Entry] = 1092 state.node_exports(version, node_name).iterator.map(_._2).toList 1093 1094 lazy val exports_map: Map[String, Export.Entry] = 1095 (for (entry <- exports.iterator) yield (entry.name, entry)).toMap 1096 1097 1098 /* find command */ 1099 1100 def find_command(id: Document_ID.Generic): Option[(Node, Command)] = 1101 state.lookup_id(id) match { 1102 case None => None 1103 case Some(st) => 1104 val command = st.command 1105 val node = version.nodes(command.node_name) 1106 if (node.commands.contains(command)) Some((node, command)) else None 1107 } 1108 1109 def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset) 1110 : Option[Line.Node_Position] = 1111 for ((node, command) <- find_command(id)) 1112 yield { 1113 val name = command.node_name.node 1114 val sources_iterator = 1115 node.commands.iterator.takeWhile(_ != command).map(_.source) ++ 1116 (if (offset == 0) Iterator.empty 1117 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset))))) 1118 val pos = (Line.Position.zero /: sources_iterator)(_.advance(_)) 1119 Line.Node_Position(name, pos) 1120 } 1121 1122 1123 /* cumulate markup */ 1124 1125 def cumulate[A]( 1126 range: Text.Range, 1127 info: A, 1128 elements: Markup.Elements, 1129 result: List[Command.State] => (A, Text.Markup) => Option[A], 1130 status: Boolean = false): List[Text.Info[A]] = 1131 { 1132 val former_range = revert(range).inflate_singularity 1133 val (chunk_name, command_iterator) = 1134 commands_loading.headOption match { 1135 case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range)) 1136 case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0))) 1137 } 1138 val markup_index = Command.Markup_Index(status, chunk_name) 1139 (for { 1140 (command, command_start) <- command_iterator 1141 chunk <- command.chunks.get(chunk_name).iterator 1142 states = state.command_states(version, command) 1143 res = result(states) 1144 markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator 1145 markup = Command.State.merge_markup(states, markup_index, markup_range, elements) 1146 Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements, 1147 { 1148 case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) 1149 }).iterator 1150 r1 <- convert(r0 + command_start).try_restrict(range).iterator 1151 } yield Text.Info(r1, a)).toList 1152 } 1153 1154 def select[A]( 1155 range: Text.Range, 1156 elements: Markup.Elements, 1157 result: List[Command.State] => Text.Markup => Option[A], 1158 status: Boolean = false): List[Text.Info[A]] = 1159 { 1160 def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] = 1161 { 1162 val res = result(states) 1163 (_: Option[A], x: Text.Markup) => 1164 res(x) match { 1165 case None => None 1166 case some => Some(some) 1167 } 1168 } 1169 for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status)) 1170 yield Text.Info(r, x) 1171 } 1172 1173 1174 /* command results */ 1175 1176 def command_results(range: Text.Range): Command.Results = 1177 Command.State.merge_results( 1178 select[List[Command.State]](range, Markup.Elements.full, command_states => 1179 { case _ => Some(command_states) }).flatMap(_.info)) 1180 1181 def command_results(command: Command): Command.Results = 1182 state.command_results(version, command) 1183 1184 1185 /* command ids: static and dynamic */ 1186 1187 def command_id_map: Map[Document_ID.Generic, Command] = 1188 state.command_id_map(version, version.nodes(node_name).commands) 1189 1190 1191 /* output */ 1192 1193 override def toString: String = 1194 "Snapshot(node = " + node_name.node + ", version = " + version.id + 1195 (if (is_outdated) ", outdated" else "") + ")" 1196 } 1197 } 1198 } 1199} 1200