--- 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 ***
--- 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
--- 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) #>