added ML antiquotation @{here};
authorwenzelm
Wed Mar 12 22:44:55 2014 +0100 (2014-03-12)
changeset 560712ffdedb0c044
parent 56070 1bc0bea908c3
child 56072 31e427387ab5
added ML antiquotation @{here};
NEWS
src/Doc/IsarImplementation/Prelim.thy
src/Pure/ML/ml_antiquote.ML
     1.1 --- a/NEWS	Wed Mar 12 22:41:04 2014 +0100
     1.2 +++ b/NEWS	Wed Mar 12 22:44:55 2014 +0100
     1.3 @@ -441,6 +441,9 @@
     1.4  ML_Context.antiquotation, to make it more close to the analogous
     1.5  Thy_Output.antiquotation.  Minor INCOMPATIBILTY.
     1.6  
     1.7 +* ML antiquotation @{here} refers to its source position, which is
     1.8 +occasionally useful for experimentation and diagnostic purposes.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/Doc/IsarImplementation/Prelim.thy	Wed Mar 12 22:41:04 2014 +0100
     2.2 +++ b/src/Doc/IsarImplementation/Prelim.thy	Wed Mar 12 22:44:55 2014 +0100
     2.3 @@ -1056,6 +1056,14 @@
     2.4  text {* This illustrates a key virtue of formalized bindings as
     2.5    opposed to raw specifications of base names: the system can use this
     2.6    additional information for feedback given to the user (error
     2.7 -  messages etc.). *}
     2.8 +  messages etc.).
     2.9 +
    2.10 +  \medskip The following example refers to its source position
    2.11 +  directly, which is occasionally useful for experimentation and
    2.12 +  diagnostic purposes: *}
    2.13 +
    2.14 +ML_command {*
    2.15 +  warning ("Look here" ^ Position.here @{here})
    2.16 +*}
    2.17  
    2.18  end
     3.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 22:41:04 2014 +0100
     3.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Mar 12 22:44:55 2014 +0100
     3.3 @@ -52,7 +52,16 @@
     3.4  (** misc antiquotations **)
     3.5  
     3.6  val _ = Theory.setup
     3.7 - (inline (Binding.name "assert")
     3.8 + (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ())
     3.9 +    (fn src => fn () => fn ctxt =>
    3.10 +      let
    3.11 +        val (a, ctxt') = variant "position" ctxt;
    3.12 +        val (_, pos) = Args.name_of_src src;
    3.13 +        val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
    3.14 +        val body = "Isabelle." ^ a;
    3.15 +      in (K (env, body), ctxt') end) #>
    3.16 +
    3.17 +  inline (Binding.name "assert")
    3.18      (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    3.19  
    3.20    inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>