NEWS
changeset 56135 efa24d31e595
parent 56072 31e427387ab5
child 56148 d94d6a9178b5
     1.1 --- a/NEWS	Thu Mar 13 10:34:48 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 13 11:34:05 2014 +0100
     1.3 @@ -445,6 +445,12 @@
     1.4  * ML antiquotation @{here} refers to its source position, which is
     1.5  occasionally useful for experimentation and diagnostic purposes.
     1.6  
     1.7 +* ML antiquotation @{path} produces a Path.T value, similarly to
     1.8 +Path.explode, but with compile-time check against the file-system and
     1.9 +some PIDE markup.  Note that unlike theory source, ML does not have a
    1.10 +well-defined master directory, so an absolute symbolic path
    1.11 +specification is usually required, e.g. "~~/src/HOL".
    1.12 +
    1.13  
    1.14  *** System ***
    1.15