--- 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;
--- 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
--- 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)
--- 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)
}
--- 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 =>
--- 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 */
--- 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))
}
}
}