# HG changeset patch
# User wenzelm
# Date 1275596256 -7200
# Node ID 9763792e4ac7c503fc2332cdbb21b966f7604e15
# Parent  645f849eefa7bbb6f8ba9c741a000033b1b649d7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};

diff -r 645f849eefa7 -r 9763792e4ac7 NEWS
--- a/NEWS	Thu Jun 03 22:06:37 2010 +0200
+++ b/NEWS	Thu Jun 03 22:17:36 2010 +0200
@@ -558,6 +558,11 @@
 values similar to the ML toplevel.  The result is compiler dependent
 and may fall back on "?" in certain situations.
 
+* Diagnostic commands 'ML_val' and 'ML_command' may refer to
+antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure
+Isar.state() and Isar.goal(), which belong to the old TTY loop and do
+not work with the asynchronous Isar document model.
+
 * Sorts.certify_sort and derived "cert" operations for types and terms
 no longer minimize sorts.  Thus certification at the boundary of the
 inference kernel becomes invariant under addition of class relations,
diff -r 645f849eefa7 -r 9763792e4ac7 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Jun 03 22:06:37 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Jun 03 22:17:36 2010 +0200
@@ -42,6 +42,8 @@
   val disable_pr: Toplevel.transition -> Toplevel.transition
   val enable_pr: Toplevel.transition -> Toplevel.transition
   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
+  val diag_state: unit -> Toplevel.state
+  val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
@@ -299,9 +301,26 @@
 
 (* diagnostic ML evaluation *)
 
+structure Diag_State = Proof_Data
+(
+  type T = Toplevel.state;
+  fun init _ = Toplevel.toplevel;
+);
+
 fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
-  (ML_Context.eval_text_in
-    (Option.map Context.proof_of (try Toplevel.generic_theory_of state)) verbose pos txt));
+  let val opt_ctxt =
+    try Toplevel.generic_theory_of state
+    |> Option.map (Context.proof_of #> Diag_State.put state)
+  in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
+
+fun diag_state () = Diag_State.get (ML_Context.the_local_context ());
+
+fun diag_goal () =
+  Proof.goal (Toplevel.proof_of (diag_state ()))
+    handle Toplevel.UNDEF => error "No goal present";
+
+val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()");
+val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()");
 
 
 (* current working directory *)