src/Doc/IsarImplementation/Prelim.thy
changeset 56071 2ffdedb0c044
parent 55837 154855d9a564
     1.1 --- a/src/Doc/IsarImplementation/Prelim.thy	Wed Mar 12 22:41:04 2014 +0100
     1.2 +++ b/src/Doc/IsarImplementation/Prelim.thy	Wed Mar 12 22:44:55 2014 +0100
     1.3 @@ -1056,6 +1056,14 @@
     1.4  text {* This illustrates a key virtue of formalized bindings as
     1.5    opposed to raw specifications of base names: the system can use this
     1.6    additional information for feedback given to the user (error
     1.7 -  messages etc.). *}
     1.8 +  messages etc.).
     1.9 +
    1.10 +  \medskip The following example refers to its source position
    1.11 +  directly, which is occasionally useful for experimentation and
    1.12 +  diagnostic purposes: *}
    1.13 +
    1.14 +ML_command {*
    1.15 +  warning ("Look here" ^ Position.here @{here})
    1.16 +*}
    1.17  
    1.18  end