eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
eliminated ML interface of Isar_Document: the protocol only works with certain transaction positions, i.e. via Isar commands;
--- a/src/Pure/General/markup.ML Wed Dec 30 20:25:35 2009 +0100
+++ b/src/Pure/General/markup.ML Wed Dec 30 21:32:25 2009 +0100
@@ -105,7 +105,6 @@
val failedN: string val failed: T
val finishedN: string val finished: T
val disposedN: string val disposed: T
- val editsN: string val edits: string -> T
val editN: string val edit: string -> string -> T
val pidN: string
val sessionN: string
@@ -307,8 +306,6 @@
(* interactive documents *)
-val (editsN, edits) = markup_string "edits" idN;
-
val editN = "edit";
fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
--- a/src/Pure/General/markup.scala Wed Dec 30 20:25:35 2009 +0100
+++ b/src/Pure/General/markup.scala Wed Dec 30 21:32:25 2009 +0100
@@ -153,7 +153,6 @@
/* interactive documents */
- val EDITS = "edits"
val EDIT = "edit"
--- a/src/Pure/Isar/isar_document.ML Wed Dec 30 20:25:35 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML Wed Dec 30 21:32:25 2009 +0100
@@ -4,20 +4,7 @@
Interactive Isar documents.
*)
-signature ISAR_DOCUMENT =
-sig
- type state_id = string
- type command_id = string
- type document_id = string
- val no_id: string
- val create_id: unit -> string
- val define_command: command_id -> Toplevel.transition -> unit
- val begin_document: document_id -> Path.T -> unit
- val end_document: document_id -> unit
- val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
-end;
-
-structure Isar_Document: ISAR_DOCUMENT =
+structure Isar_Document: sig end =
struct
(* unique identifiers *)
@@ -245,11 +232,10 @@
in put_state state_id' state' end;
in (state_id', ((id, state_id'), make_state') :: updates) end;
-fun report_updates _ [] = ()
- | report_updates (document_id: document_id) updates =
- implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
- |> Markup.markup (Markup.edits document_id)
- |> Output.status;
+fun report_updates [] = ()
+ | report_updates updates =
+ Output.status
+ (implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates));
in
@@ -279,7 +265,7 @@
in (rev updates, new_document') end);
val _ = define_document new_id new_document';
- val _ = report_updates new_id (map #1 updates);
+ val _ = report_updates (map #1 updates);
val _ = List.app (fn (_, run) => run ()) updates;
in () end);
@@ -310,7 +296,9 @@
val _ =
OuterSyntax.internal_command "Isar.edit_document"
(P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
- >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => edit_document id new_id edits)));
+ >> (fn ((id, new_id), edits) =>
+ Toplevel.position (Position.id_only new_id) o
+ Toplevel.imperative (fn () => edit_document id new_id edits)));
end;