src/Pure/ML/ml_antiquote.ML
changeset 56071 2ffdedb0c044
parent 56069 451d5b73f8cf
     1.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 22:41:04 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 22:44:55 2014 +0100
     1.3 @@ -52,7 +52,16 @@
     1.4  (** misc antiquotations **)
     1.5  
     1.6  val _ = Theory.setup
     1.7 - (inline (Binding.name "assert")
     1.8 + (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ())
     1.9 +    (fn src => fn () => fn ctxt =>
    1.10 +      let
    1.11 +        val (a, ctxt') = variant "position" ctxt;
    1.12 +        val (_, pos) = Args.name_of_src src;
    1.13 +        val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
    1.14 +        val body = "Isabelle." ^ a;
    1.15 +      in (K (env, body), ctxt') end) #>
    1.16 +
    1.17 +  inline (Binding.name "assert")
    1.18      (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    1.19  
    1.20    inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>