# HG changeset patch # User wenzelm # Date 1313087564 -7200 # Node ID a21d3e1e64fd0d6ee0af77da921a329da0527de1 # Parent 6aa25b80e1a53743a6ff6ef1ca76ecb63fb9b977 uniform treatment of header edits as document edits; diff -r 6aa25b80e1a5 -r a21d3e1e64fd src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Aug 11 18:01:28 2011 +0200 +++ b/src/Pure/PIDE/document.ML Thu Aug 11 20:32:44 2011 +0200 @@ -15,16 +15,17 @@ val new_id: unit -> id val parse_id: string -> id val print_id: id -> string - datatype node_edit = Remove | Edits of (command_id option * command_id option) 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 header = string * (string * string list * string list) 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 @@ -76,11 +77,13 @@ (* node edits and associated executions *) -datatype node_edit = Remove | Edits of (command_id option * command_id option) 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 header = string * (string * string list * string list); - fun the_entry (Node {entries, ...}) id = (case Entries.lookup entries id of NONE => err_undef "command entry" id @@ -107,12 +110,15 @@ fun get_node version name = Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node; -fun edit_nodes (name, Remove) (Version nodes) = - Version (perhaps (try (Graph.del_node name)) nodes) - | edit_nodes (name, Edits 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)); + |> Graph.map_node name (edit_node edits) + | Update_Header _ => nodes); (* FIXME *) fun put_node name node (Version nodes) = Version (nodes @@ -312,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 6aa25b80e1a5 -r a21d3e1e64fd src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 11 18:01:28 2011 +0200 +++ b/src/Pure/PIDE/document.scala Thu Aug 11 20:32:44 2011 +0200 @@ -44,10 +44,12 @@ 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"))) diff -r 6aa25b80e1a5 -r a21d3e1e64fd src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Thu Aug 11 18:01:28 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Thu Aug 11 20:32:44 2011 +0200 @@ -13,23 +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 - (variant - [fn ([], []) => Document.Remove, - fn ([], a) => Document.Edits (list (pair (option int) (option int)) a)])) - 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 6aa25b80e1a5 -r a21d3e1e64fd src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Thu Aug 11 18:01:28 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Thu Aug 11 20:32:44 2011 +0200 @@ -140,24 +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._ 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)) })))) - encode(edits) } + { 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 6aa25b80e1a5 -r a21d3e1e64fd src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Aug 11 18:01:28 2011 +0200 +++ b/src/Pure/System/session.scala Thu Aug 11 20:32:44 2011 +0200 @@ -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) @@ -186,18 +185,16 @@ { 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,7 +209,6 @@ 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 { @@ -236,7 +232,7 @@ } 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) } //}}} diff -r 6aa25b80e1a5 -r a21d3e1e64fd src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Thu Aug 11 18:01:28 2011 +0200 +++ b/src/Pure/Thy/thy_header.scala Thu Aug 11 20:32:44 2011 +0200 @@ -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 6aa25b80e1a5 -r a21d3e1e64fd src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu Aug 11 18:01:28 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Thu Aug 11 20:32:44 2011 +0200 @@ -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,25 +172,10 @@ } - /* 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 { @@ -213,13 +197,19 @@ inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) doc_edits += (name -> Document.Node.Edits(cmd_edits)) - - val (new_headers, new_header) = node_header(name, node) - header_edits ++= new_headers + nodes += (name -> node.copy(commands = commands2)) - 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)) } } }