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