# HG changeset patch # User huffman # Date 1313158392 25200 # Node ID 9c120cde98f9e0bb23037593b9b4fa4b7988d3db # Parent e81d676d598ec7247107a101a9ad0bca2b4e829a# Parent a21d3e1e64fd0d6ee0af77da921a329da0527de1 merged diff -r e81d676d598e -r 9c120cde98f9 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Aug 11 14:24:05 2011 -0700 +++ b/src/Pure/PIDE/document.ML Fri Aug 12 07:13:12 2011 -0700 @@ -15,15 +15,17 @@ val new_id: unit -> id val parse_id: string -> id val print_id: id -> string - type edit = string * ((command_id option * command_id option) list) option - type header = string * (string * string list * string list) + datatype node_edit = + Remove | + Edits of (command_id option * command_id option) list | + Update_Header of (string * string list * string list) Exn.result + type edit = string * node_edit type state val init_state: state val get_theory: state -> version_id -> Position.T -> string -> theory val cancel_execution: state -> unit -> unit val define_command: command_id -> string -> state -> state - val edit: version_id -> version_id -> edit list -> header list -> - state -> (command_id * exec_id) list * state + val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state val execute: version_id -> state -> state val state: unit -> state val change_state: (state -> state) -> unit @@ -75,12 +77,12 @@ (* node edits and associated executions *) -type edit = - string * - (*NONE: remove node, SOME: insert/remove commands*) - ((command_id option * command_id option) list) option; +datatype node_edit = + Remove | + Edits of (command_id option * command_id option) list | + Update_Header of (string * string list * string list) Exn.result; -type header = string * (string * string list * string list); +type edit = string * node_edit; fun the_entry (Node {entries, ...}) id = (case Entries.lookup entries id of @@ -108,12 +110,15 @@ fun get_node version name = Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node; -fun edit_nodes (name, SOME edits) (Version nodes) = - Version (nodes +fun edit_nodes (name, node_edit) (Version nodes) = + Version + (case node_edit of + Remove => perhaps (try (Graph.del_node name)) nodes + | Edits edits => + nodes |> Graph.default_node (name, empty_node) - |> Graph.map_node name (edit_node edits)) - | edit_nodes (name, NONE) (Version nodes) = - Version (perhaps (try (Graph.del_node name)) nodes); + |> Graph.map_node name (edit_node edits) + | Update_Header _ => nodes); (* FIXME *) fun put_node name node (Version nodes) = Version (nodes @@ -313,10 +318,8 @@ in -fun edit (old_id: version_id) (new_id: version_id) edits headers state = +fun edit (old_id: version_id) (new_id: version_id) edits state = let - (* FIXME apply headers *) - val old_version = the_version state old_id; val _ = Time.now (); (* FIXME odd workaround *) val new_version = fold edit_nodes edits old_version; diff -r e81d676d598e -r 9c120cde98f9 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 11 14:24:05 2011 -0700 +++ b/src/Pure/PIDE/document.scala Fri Aug 12 07:13:12 2011 -0700 @@ -31,16 +31,26 @@ /* named nodes -- development graph */ - type Edit[A] = - (String, // node name - Option[List[A]]) // None: remove node, Some: edit content - + type Edit[A] = (String, Node.Edit[A]) type Edit_Text = Edit[Text.Edit] type Edit_Command = Edit[(Option[Command], Option[Command])] type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])] object Node { + sealed abstract class Edit[A] + { + def map[B](f: A => B): Edit[B] = + this match { + case Remove() => Remove() + case Edits(es) => Edits(es.map(f)) + case Update_Header(header: Header) => Update_Header(header) + } + } + case class Remove[A]() extends Edit[A] + case class Edits[A](edits: List[A]) extends Edit[A] + case class Update_Header[A](header: Header) extends Edit[A] + sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header]) val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header"))) @@ -290,10 +300,10 @@ val stable = found_stable.get val latest = history.undo_list.head - // FIXME proper treatment of deleted nodes + // FIXME proper treatment of removed nodes val edits = (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) => - (for ((a, Some(eds)) <- change.edits if a == name) yield eds).flatten ::: edits) + (for ((a, Node.Edits(es)) <- change.edits if a == name) yield es).flatten ::: edits) lazy val reverse_edits = edits.reverse new Snapshot diff -r e81d676d598e -r 9c120cde98f9 src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Thu Aug 11 14:24:05 2011 -0700 +++ b/src/Pure/PIDE/isar_document.ML Fri Aug 12 07:13:12 2011 -0700 @@ -13,19 +13,24 @@ val _ = Isabelle_Process.add_command "Isar_Document.edit_version" - (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state => + (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => let val old_id = Document.parse_id old_id_string; val new_id = Document.parse_id new_id_string; - val edits = YXML.parse_body edits_yxml |> - let open XML.Decode - in list (pair string (option (list (pair (option int) (option int))))) end; - val headers = YXML.parse_body headers_yxml |> - let open XML.Decode - in list (pair string (triple string (list string) (list string))) end; + val edits = + YXML.parse_body edits_yxml |> + let open XML.Decode in + list (pair string + (variant + [fn ([], []) => Document.Remove, + fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), + fn ([], a) => + Document.Update_Header (Exn.Res (triple string (list string) (list string) a)), + fn ([a], []) => Document.Update_Header (Exn.Exn (ERROR a))])) + end; val await_cancellation = Document.cancel_execution state; - val (updates, state') = Document.edit old_id new_id edits headers state; + val (updates, state') = Document.edit old_id new_id edits state; val _ = await_cancellation (); val _ = Output.status (Markup.markup (Markup.assign new_id) diff -r e81d676d598e -r 9c120cde98f9 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Thu Aug 11 14:24:05 2011 -0700 +++ b/src/Pure/PIDE/isar_document.scala Fri Aug 12 07:13:12 2011 -0700 @@ -140,19 +140,23 @@ /* document versions */ def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, - edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)]) + edits: List[Document.Edit_Command_ID]) { - val arg1 = + val edits_yxml = { import XML.Encode._ - list(pair(string, option(list(pair(option(long), option(long))))))(edits) } + def encode: T[List[Document.Edit_Command_ID]] = + list(pair(string, + variant(List( + { case Document.Node.Remove() => (Nil, Nil) }, + { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) }, + { case Document.Node.Update_Header( + Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) => + (Nil, triple(string, list(string), list(string))(a, b, c)) }, + { case Document.Node.Update_Header( + Document.Node.Header(_, Exn.Exn(ERROR(a)))) => (List(a), Nil) })))) + YXML.string_of_body(encode(edits)) } - val arg2 = - { import XML.Encode._ - list(pair(string, Thy_Header.xml_encode))(headers) } - - input("Isar_Document.edit_version", - Document.ID(old_id), Document.ID(new_id), - YXML.string_of_body(arg1), YXML.string_of_body(arg2)) + input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml) } diff -r e81d676d598e -r 9c120cde98f9 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Aug 11 14:24:05 2011 -0700 +++ b/src/Pure/System/session.scala Fri Aug 12 07:13:12 2011 -0700 @@ -168,7 +168,6 @@ private case class Change_Node( name: String, doc_edits: List[Document.Edit_Command], - header_edits: List[(String, Thy_Header.Header)], previous: Document.Version, version: Document.Version) @@ -181,23 +180,21 @@ /* incoming edits */ def handle_edits(name: String, - header: Document.Node.Header, edits: List[Option[List[Text.Edit]]]) + header: Document.Node.Header, edits: List[Document.Node.Edit[Text.Edit]]) //{{{ { val syntax = current_syntax() val previous = global_state().history.tip.version - val doc_edits = edits.map(edit => (name, edit)) - val result = Future.fork { - Thy_Syntax.text_edits(syntax, previous.join, doc_edits, List((name, header))) - } + val doc_edits = + (name, Document.Node.Update_Header[Text.Edit](header)) :: edits.map(edit => (name, edit)) + val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) } val change = - global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._3))) + global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2))) result.map { - case (doc_edits, header_edits, _) => + case (doc_edits, _) => assignments.await { global_state().is_assigned(previous.get_finished) } - this_actor ! - Change_Node(name, doc_edits, header_edits, previous.join, change.version.join) + this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join) } } //}}} @@ -212,11 +209,10 @@ val version = change.version val name = change.name val doc_edits = change.doc_edits - val header_edits = change.header_edits var former_assignment = global_state().the_assignment(previous).get_finished for { - (name, Some(cmd_edits)) <- doc_edits + (name, Document.Node.Edits(cmd_edits)) <- doc_edits // FIXME proper coverage!? (prev, None) <- cmd_edits removed <- previous.nodes(name).commands.get_after(prev) } former_assignment -= removed @@ -231,14 +227,12 @@ } val id_edits = doc_edits map { - case (name, edits) => - val ids = - edits.map(_.map { case (c1, c2) => (c1.map(id_command), c2.map(id_command)) }) - (name, ids) + case (name, edit) => + (name, edit.map({ case (c1, c2) => (c1.map(id_command), c2.map(id_command)) })) } global_state.change(_.define_version(version, former_assignment)) - prover.get.edit_version(previous.id, version.id, id_edits, header_edits) + prover.get.edit_version(previous.id, version.id, id_edits) } //}}} @@ -331,11 +325,12 @@ case Init_Node(name, header, text) if prover.isDefined => // FIXME compare with existing node - handle_edits(name, header, List(None, Some(List(Text.Edit.insert(0, text))))) + handle_edits(name, header, + List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text))))) reply(()) case Edit_Node(name, header, text_edits) if prover.isDefined => - handle_edits(name, header, List(Some(text_edits))) + handle_edits(name, header, List(Document.Node.Edits(text_edits))) reply(()) case change: Change_Node if prover.isDefined => diff -r e81d676d598e -r 9c120cde98f9 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Thu Aug 11 14:24:05 2011 -0700 +++ b/src/Pure/Thy/thy_header.scala Fri Aug 12 07:13:12 2011 -0700 @@ -31,13 +31,6 @@ Header(f(name), imports.map(f), uses.map(f)) } - val xml_encode: XML.Encode.T[Header] = - { - case Header(name, imports, uses) => - import XML.Encode._ - triple(string, list(string), list(string))(name, imports, uses) - } - /* file name */ diff -r e81d676d598e -r 9c120cde98f9 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu Aug 11 14:24:05 2011 -0700 +++ b/src/Pure/Thy/thy_syntax.scala Fri Aug 12 07:13:12 2011 -0700 @@ -102,9 +102,8 @@ def text_edits( syntax: Outer_Syntax, previous: Document.Version, - edits: List[Document.Edit_Text], - headers: List[(String, Document.Node.Header)]) - : (List[Document.Edit_Command], List[(String, Thy_Header.Header)], Document.Version) = + edits: List[Document.Edit_Text]) + : (List[Document.Edit_Command], Document.Version) = { /* phase 1: edit individual command source */ @@ -173,33 +172,18 @@ } - /* node header */ - - def node_header(name: String, node: Document.Node) - : (List[(String, Thy_Header.Header)], Document.Node.Header) = - (node.header.thy_header, headers.find(p => p._1 == name).map(_._2)) match { - case (Exn.Res(thy_header0), Some(header @ Document.Node.Header(_, Exn.Res(thy_header)))) - if thy_header0 != thy_header => - (List((name, thy_header)), header) - case (Exn.Exn(_), Some(header @ Document.Node.Header(_, Exn.Res(thy_header)))) => - (List((name, thy_header)), header) - case _ => (Nil, node.header) - } - - /* resulting document edits */ { val doc_edits = new mutable.ListBuffer[Document.Edit_Command] - val header_edits = new mutable.ListBuffer[(String, Thy_Header.Header)] var nodes = previous.nodes edits foreach { - case (name, None) => - doc_edits += (name -> None) + case (name, Document.Node.Remove()) => + doc_edits += (name -> Document.Node.Remove()) nodes -= name - case (name, Some(text_edits)) => + case (name, Document.Node.Edits(text_edits)) => val node = nodes(name) val commands0 = node.commands val commands1 = edit_text(text_edits, commands0) @@ -212,14 +196,20 @@ removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) - doc_edits += (name -> Some(cmd_edits)) + doc_edits += (name -> Document.Node.Edits(cmd_edits)) + nodes += (name -> node.copy(commands = commands2)) - val (new_headers, new_header) = node_header(name, node) - header_edits ++= new_headers - - nodes += (name -> Document.Node(new_header, node.blobs, commands2)) + case (name, Document.Node.Update_Header(header)) => + val node = nodes(name) + val update_header = + (node.header.thy_header, header) match { + case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) + if thy_header0 != thy_header => true + case (Exn.Exn(_), Document.Node.Header(_, Exn.Res(thy_header))) => true + } + if (update_header) doc_edits += (name -> Document.Node.Update_Header(header)) } - (doc_edits.toList, header_edits.toList, Document.Version(Document.new_id(), nodes)) + (doc_edits.toList, Document.Version(Document.new_id(), nodes)) } } }