NEWS
changeset 56148 d94d6a9178b5
parent 56118 d3967fdc800a
parent 56135 efa24d31e595
child 56154 f0a927235162
     1.1 --- a/NEWS	Fri Mar 14 12:09:51 2014 +0100
     1.2 +++ b/NEWS	Fri Mar 14 17:32:11 2014 +0100
     1.3 @@ -460,6 +460,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