# HG changeset patch
# User wenzelm
# Date 1262205145 -3600
# Node ID 8c3e1f73953d7a34eb8ac0e6a6d758d00003510f
# Parent  686f828548effa55244b89448321cdda8f151151
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;

diff -r 686f828548ef -r 8c3e1f73953d src/Pure/General/markup.ML
--- 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)]);
 
diff -r 686f828548ef -r 8c3e1f73953d src/Pure/General/markup.scala
--- 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"
 
 
diff -r 686f828548ef -r 8c3e1f73953d src/Pure/Isar/isar_document.ML
--- 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;