# HG changeset patch
# User wenzelm
# Date 1394660695 -3600
# Node ID 2ffdedb0c04472beff51993fc247a45cb5a126e6
# Parent  1bc0bea908c396ca321ca3c06814194879d53437
added ML antiquotation @{here};

diff -r 1bc0bea908c3 -r 2ffdedb0c044 NEWS
--- a/NEWS	Wed Mar 12 22:41:04 2014 +0100
+++ b/NEWS	Wed Mar 12 22:44:55 2014 +0100
@@ -441,6 +441,9 @@
 ML_Context.antiquotation, to make it more close to the analogous
 Thy_Output.antiquotation.  Minor INCOMPATIBILTY.
 
+* ML antiquotation @{here} refers to its source position, which is
+occasionally useful for experimentation and diagnostic purposes.
+
 
 *** System ***
 
diff -r 1bc0bea908c3 -r 2ffdedb0c044 src/Doc/IsarImplementation/Prelim.thy
--- a/src/Doc/IsarImplementation/Prelim.thy	Wed Mar 12 22:41:04 2014 +0100
+++ b/src/Doc/IsarImplementation/Prelim.thy	Wed Mar 12 22:44:55 2014 +0100
@@ -1056,6 +1056,14 @@
 text {* This illustrates a key virtue of formalized bindings as
   opposed to raw specifications of base names: the system can use this
   additional information for feedback given to the user (error
-  messages etc.). *}
+  messages etc.).
+
+  \medskip The following example refers to its source position
+  directly, which is occasionally useful for experimentation and
+  diagnostic purposes: *}
+
+ML_command {*
+  warning ("Look here" ^ Position.here @{here})
+*}
 
 end
diff -r 1bc0bea908c3 -r 2ffdedb0c044 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 22:41:04 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 22:44:55 2014 +0100
@@ -52,7 +52,16 @@
 (** misc antiquotations **)
 
 val _ = Theory.setup
- (inline (Binding.name "assert")
+ (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ())
+    (fn src => fn () => fn ctxt =>
+      let
+        val (a, ctxt') = variant "position" ctxt;
+        val (_, pos) = Args.name_of_src src;
+        val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
+        val body = "Isabelle." ^ a;
+      in (K (env, body), ctxt') end) #>
+
+  inline (Binding.name "assert")
     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
 
   inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>