X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fsyntax_extensions%2Fpa_unicode_macro.ml;h=d81ec21310b24edda459b1d7d47447783010219f;hb=9e7df95a820cb91d075f1a20d703175da874596c;hp=dda7d4cabc852161144df5a893c1dfc253985d0e;hpb=58955ec841575330f0b429033264f9ec7df319f9;p=helm.git

diff --git a/helm/software/components/syntax_extensions/pa_unicode_macro.ml b/helm/software/components/syntax_extensions/pa_unicode_macro.ml
index dda7d4cab..d81ec2131 100644
--- a/helm/software/components/syntax_extensions/pa_unicode_macro.ml
+++ b/helm/software/components/syntax_extensions/pa_unicode_macro.ml
@@ -28,12 +28,7 @@
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s)
 
-let loc =
-  let dummy_pos =
-    { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
-      Lexing.pos_cnum = -1 }
-  in
-  (dummy_pos, dummy_pos)
+let loc = Stdpp.make_loc (-1, -1)
 
 let expand_unicode_macro macro =
   debug_print (lazy (Printf.sprintf "Expanding macro '%s' ..." macro));
@@ -56,9 +51,8 @@ EXTEND
            String.sub q (pos + 1) (String.length q - pos - 1))
         in
         debug_print (lazy (Printf.sprintf "QUOTATION = %s; ARG = %s" quotation arg));
-        if quotation = "unicode" then
-          let text = TXtok (loc, x, expand_unicode_macro arg) in
-          {used = []; text = text; styp = STlid (loc, "string")}
+        if quotation = "unicode" then 
+          AStok (loc, x, Some (ATexpr (loc, expand_unicode_macro arg)))
         else
           assert false
       ]