# HG changeset patch # User wenzelm # Date 1281874732 -7200 # Node ID b8922ae21111b3f01a96ee24faa1a40609ccdb9a # Parent 56e76cd46b4f64f3b765181d5021f0e33dea4062 renamed class Document to Document.Version etc.; renamed Change.prev to Change.previous, and Change.document to Change.current; tuned; diff -r 56e76cd46b4f -r b8922ae21111 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun Aug 15 13:17:45 2010 +0200 +++ b/src/Pure/PIDE/document.scala Sun Aug 15 14:18:52 2010 +0200 @@ -78,9 +78,14 @@ } - /* initial document */ + /* document versions */ - val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty)) + object Version + { + val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty)) + } + + class Version(val id: Version_ID, val nodes: Map[String, Node]) @@ -94,8 +99,8 @@ abstract class Snapshot { - val document: Document - val node: Document.Node + val version: Version + val node: Node val is_outdated: Boolean def convert(offset: Int): Int def revert(offset: Int): Int @@ -105,16 +110,16 @@ object Change { - val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init)) + val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init)) } class Change( - val prev: Future[Document], + val previous: Future[Version], val edits: List[Node_Text_Edit], - val result: Future[(List[Edit[Command]], Document)]) + val result: Future[(List[Edit[Command]], Version)]) { - val document: Future[Document] = result.map(_._2) - def is_finished: Boolean = prev.is_finished && document.is_finished + val current: Future[Version] = result.map(_._2) + def is_finished: Boolean = previous.is_finished && current.is_finished } @@ -125,7 +130,7 @@ { class Fail(state: State) extends Exception - val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil) + val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil) class Assignment(former_assignment: Map[Command, Exec_ID]) { @@ -142,20 +147,20 @@ } case class State( - val documents: Map[Version_ID, Document] = Map(), + val versions: Map[Version_ID, Version] = Map(), val commands: Map[Command_ID, Command.State] = Map(), - val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(), - val assignments: Map[Document, State.Assignment] = Map(), + val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(), + val assignments: Map[Version, State.Assignment] = Map(), val disposed: Set[ID] = Set()) // FIXME unused!? { private def fail[A]: A = throw new State.Fail(this) - def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State = + def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State = { - val id = document.id - if (documents.isDefinedAt(id) || disposed(id)) fail - copy(documents = documents + (id -> document), - assignments = assignments + (document -> new State.Assignment(former_assignment))) + val id = version.id + if (versions.isDefinedAt(id) || disposed(id)) fail + copy(versions = versions + (id -> version), + assignments = assignments + (version -> new State.Assignment(former_assignment))) } def define_command(command: Command): State = @@ -167,16 +172,16 @@ def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command) - def the_document(id: Version_ID): Document = documents.getOrElse(id, fail) + def the_version(id: Version_ID): Version = versions.getOrElse(id, fail) def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1 - def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail) + def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail) def accumulate(id: ID, message: XML.Tree): (Command.State, State) = execs.get(id) match { - case Some((st, docs)) => + case Some((st, occs)) => val new_st = st.accumulate(message) - (new_st, copy(execs = execs + (id -> (new_st, docs)))) + (new_st, copy(execs = execs + (id -> (new_st, occs)))) case None => commands.get(id) match { case Some(st) => @@ -188,38 +193,33 @@ def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State = { - val doc = the_document(id) - val docs = Set(doc) // FIXME unused (!?) + val version = the_version(id) + val occs = Set(version) // FIXME unused (!?) var new_execs = execs val assigned_execs = for ((cmd_id, exec_id) <- edits) yield { val st = the_command(cmd_id) if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail - new_execs += (exec_id -> (st, docs)) + new_execs += (exec_id -> (st, occs)) (st.command, exec_id) } - the_assignment(doc).assign(assigned_execs) // FIXME explicit value instead of promise (!?) + the_assignment(version).assign(assigned_execs) // FIXME explicit value instead of promise (!?) copy(execs = new_execs) } - def is_assigned(document: Document): Boolean = - assignments.get(document) match { + def is_assigned(version: Version): Boolean = + assignments.get(version) match { case Some(assgn) => assgn.is_finished case None => false } - def command_state(document: Document, command: Command): Command.State = + def command_state(version: Version, command: Command): Command.State = { - val assgn = the_assignment(document) + val assgn = the_assignment(version) require(assgn.is_finished) the_exec_state(assgn.join.getOrElse(command, fail)) } } } - -class Document( - val id: Document.Version_ID, - val nodes: Map[String, Document.Node]) - diff -r 56e76cd46b4f -r b8922ae21111 src/Pure/System/isar_document.ML --- a/src/Pure/System/isar_document.ML Sun Aug 15 13:17:45 2010 +0200 +++ b/src/Pure/System/isar_document.ML Sun Aug 15 14:18:52 2010 +0200 @@ -27,11 +27,11 @@ fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id); -(** documents **) +(** document versions **) datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option}; type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*) -type document = node Graph.T; (*development graph via static imports*) +type version = node Graph.T; (*development graph via static imports*) (* command entries *) @@ -97,8 +97,8 @@ val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))]; -fun the_node (document: document) name = - Graph.get_node document name handle Graph.UNDEF _ => empty_node; +fun the_node (version: version) name = + Graph.get_node version name handle Graph.UNDEF _ => empty_node; fun edit_node (id, SOME id2) = insert_after id id2 | edit_node (id, NONE) = delete_after id; @@ -166,19 +166,19 @@ local -val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]); +val global_versions = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: version)]); in -fun define_document (id: Document.version_id) document = +fun define_version (id: Document.version_id) version = NAMED_CRITICAL "Isar" (fn () => - Unsynchronized.change global_documents (Inttab.update_new (id, document)) - handle Inttab.DUP dup => err_dup "document" dup); + Unsynchronized.change global_versions (Inttab.update_new (id, version)) + handle Inttab.DUP dup => err_dup "version" dup); -fun the_document (id: Document.version_id) = - (case Inttab.lookup (! global_documents) id of - NONE => err_undef "document" id - | SOME document => document); +fun the_version (id: Document.version_id) = + (case Inttab.lookup (! global_versions) id of + NONE => err_undef "version" id + | SOME version => version); end; @@ -197,20 +197,20 @@ in -fun execute document = +fun execute version = NAMED_CRITICAL "Isar" (fn () => let val old_execution = ! execution; val _ = List.app Future.cancel old_execution; fun await_cancellation () = uninterruptible (K Future.join_results) old_execution; (* FIXME proper node deps *) - val new_execution = Graph.keys document |> map (fn name => + val new_execution = Graph.keys version |> map (fn name => Future.fork_pri 1 (fn () => let val _ = await_cancellation (); val exec = fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec) - (the_node document name); + (the_node version name); in exec () end)); in execution := new_execution end); @@ -249,11 +249,11 @@ fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits = NAMED_CRITICAL "Isar" (fn () => let - val old_document = the_document old_id; - val new_document = fold edit_nodes edits old_document; + val old_version = the_version old_id; + val new_version = fold edit_nodes edits old_version; fun update_node name node = - (case first_entry (is_changed (the_node old_document name)) node of + (case first_entry (is_changed (the_node old_version name)) node of NONE => ([], node) | SOME (prev, id, _) => let @@ -263,13 +263,13 @@ in (rev updates, node') end); (* FIXME proper node deps *) - val (updatess, new_document') = - (Graph.keys new_document, new_document) + val (updatess, new_version') = + (Graph.keys new_version, new_version) |-> fold_map (fn name => Graph.map_node_yield name (update_node name)); - val _ = define_document new_id new_document'; + val _ = define_version new_id new_version'; val _ = updates_status new_id (flat updatess); - val _ = execute new_document'; + val _ = execute new_version'; in () end); end; @@ -283,7 +283,7 @@ (fn [id, text] => define_command (Document.parse_id id) text); val _ = - Isabelle_Process.add_command "Isar_Document.edit_document" + Isabelle_Process.add_command "Isar_Document.edit_version" (fn [old_id, new_id, edits] => edit_document (Document.parse_id old_id) (Document.parse_id new_id) (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string diff -r 56e76cd46b4f -r b8922ae21111 src/Pure/System/isar_document.scala --- a/src/Pure/System/isar_document.scala Sun Aug 15 13:17:45 2010 +0200 +++ b/src/Pure/System/isar_document.scala Sun Aug 15 14:18:52 2010 +0200 @@ -46,9 +46,9 @@ input("Isar_Document.define_command", Document.ID(id), text) - /* documents */ + /* document versions */ - def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID, + def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, edits: List[Document.Edit[Document.Command_ID]]) { def make_id1(id1: Option[Document.Command_ID]): XML.Body = @@ -60,7 +60,7 @@ XML_Data.make_option(XML_Data.make_list( XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits) - input("Isar_Document.edit_document", + input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg)) } } diff -r 56e76cd46b4f -r b8922ae21111 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sun Aug 15 13:17:45 2010 +0200 +++ b/src/Pure/System/session.scala Sun Aug 15 14:18:52 2010 +0200 @@ -81,14 +81,14 @@ { require(change.is_finished) - val old_doc = change.prev.join - val (node_edits, doc) = change.result.join + val previous = change.previous.join + val (node_edits, current) = change.result.join - var former_assignment = current_state().the_assignment(old_doc).join + var former_assignment = current_state().the_assignment(previous).join for { (name, Some(cmd_edits)) <- node_edits (prev, None) <- cmd_edits - removed <- old_doc.nodes(name).commands.get_after(prev) + removed <- previous.nodes(name).commands.get_after(prev) } former_assignment -= removed val id_edits = @@ -113,8 +113,8 @@ } (name -> Some(ids)) } - change_state(_.define_document(doc, former_assignment)) - prover.edit_document(old_doc.id, doc.id, id_edits) + change_state(_.define_version(current, former_assignment)) + prover.edit_version(previous.id, current.id, id_edits) } //}}} @@ -142,8 +142,8 @@ case None => if (result.is_status) { result.body match { - case List(Isar_Document.Assign(doc_id, edits)) => - try { change_state(_.assign(doc_id, edits)) } + case List(Isar_Document.Assign(id, edits)) => + try { change_state(_.assign(id, edits)) } catch { case _: Document.State.Fail => bad_result(result) } case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) case List(Keyword.Keyword_Decl(name)) => syntax += name @@ -286,7 +286,7 @@ /** editor history **/ - private case class Edit_Document(edits: List[Document.Node_Text_Edit]) + private case class Edit_Version(edits: List[Document.Node_Text_Edit]) private val editor_history = new Actor { @@ -298,7 +298,7 @@ val history_snapshot = history val found_stable = history_snapshot.find(change => - change.is_finished && state_snapshot.is_assigned(change.document.join)) + change.is_finished && state_snapshot.is_assigned(change.current.join)) require(found_stable.isDefined) val stable = found_stable.get val latest = history_snapshot.head @@ -309,15 +309,15 @@ lazy val reverse_edits = edits.reverse new Document.Snapshot { - val document = stable.document.join - val node = document.nodes(name) + val version = stable.current.join + val node = version.nodes(name) val is_outdated = !(pending_edits.isEmpty && latest == stable) def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) def lookup_command(id: Document.Command_ID): Option[Command] = state_snapshot.lookup_command(id) def state(command: Command): Command.State = - try { state_snapshot.command_state(document, command) } + try { state_snapshot.command_state(version, command) } catch { case _: Document.State.Fail => command.empty_state } } } @@ -326,20 +326,20 @@ { loop { react { - case Edit_Document(edits) => + case Edit_Version(edits) => val history_snapshot = history require(!history_snapshot.isEmpty) - val prev = history_snapshot.head.document - val result: isabelle.Future[(List[Document.Edit[Command]], Document)] = + val prev = history_snapshot.head.current + val result = isabelle.Future.fork { - val old_doc = prev.join - val former_assignment = current_state().the_assignment(old_doc).join // FIXME async!? - Thy_Syntax.text_edits(Session.this, old_doc, edits) + val previous = prev.join + val former_assignment = current_state().the_assignment(previous).join // FIXME async!? + Thy_Syntax.text_edits(Session.this, previous, edits) } val new_change = new Document.Change(prev, edits, result) history ::= new_change - new_change.document.map(_ => session_actor ! new_change) + new_change.current.map(_ => session_actor ! new_change) reply(()) case bad => System.err.println("editor_model: ignoring bad message " + bad) @@ -361,5 +361,5 @@ def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot = editor_history.snapshot(name, pending_edits) - def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) } + def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) } } diff -r 56e76cd46b4f -r b8922ae21111 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sun Aug 15 13:17:45 2010 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Sun Aug 15 14:18:52 2010 +0200 @@ -38,8 +38,8 @@ /** text edits **/ - def text_edits(session: Session, old_doc: Document, edits: List[Document.Node_Text_Edit]) - : (List[Document.Edit[Command]], Document) = + def text_edits(session: Session, previous: Document.Version, + edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) = { /* phase 1: edit individual command source */ @@ -110,7 +110,7 @@ { val doc_edits = new mutable.ListBuffer[Document.Edit[Command]] - var nodes = old_doc.nodes + var nodes = previous.nodes for ((name, text_edits) <- edits) { val commands0 = nodes(name).commands @@ -127,7 +127,7 @@ doc_edits += (name -> Some(cmd_edits)) nodes += (name -> new Document.Node(commands2)) } - (doc_edits.toList, new Document(session.create_id(), nodes)) + (doc_edits.toList, new Document.Version(session.create_id(), nodes)) } } } diff -r 56e76cd46b4f -r b8922ae21111 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Sun Aug 15 13:17:45 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Sun Aug 15 14:18:52 2010 +0200 @@ -203,7 +203,7 @@ def snapshot(): List[Text_Edit] = pending.toList private val delay_flush = Swing_Thread.delay_last(session.input_delay) { - if (!pending.isEmpty) session.edit_document(List((thy_name, flush()))) + if (!pending.isEmpty) session.edit_version(List((thy_name, flush()))) } def flush(): List[Text_Edit] = @@ -225,7 +225,8 @@ /* snapshot */ - def snapshot(): Document.Snapshot = { + def snapshot(): Document.Snapshot = + { Swing_Thread.require() session.snapshot(thy_name, pending_edits.snapshot()) } diff -r 56e76cd46b4f -r b8922ae21111 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Aug 15 13:17:45 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Aug 15 14:18:52 2010 +0200 @@ -95,9 +95,9 @@ import Isabelle_Sidekick.int_to_pos val root = data.root - val doc = Swing_Thread.now { model.snapshot().node } // FIXME cover all nodes (!??) + val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for { - (command, command_start) <- doc.command_range(0) + (command, command_start) <- snapshot.node.command_range(0) if command.is_command && !stopped } { @@ -113,8 +113,7 @@ override def getStart: Position = command_start override def setEnd(end: Position) = () override def getEnd: Position = command_start + command.length - override def toString = name - }) + override def toString = name}) root.add(node) } }