helm/ocaml/cic_disambiguation/pa_unicode_macro.ml

   1
   2 let debug = false
   3 let debug_print = if debug then prerr_endline else ignore
   4
   5 let loc = (0, 0)
   6
   7 let expand_unicode_macro macro =
   8   debug_print (Printf.sprintf "Expanding macro '%s' ..." macro);
   9   let expansion = Macro.expand macro in
  10   <:expr< $str:expansion$ >>
  11
  12 let _ =
  13   Quotation.add "unicode"
  14     (Quotation.ExAst (expand_unicode_macro, (fun _ -> assert false)))
  15
  16 open Pa_extend
  17
  18 EXTEND
  19   symbol: FIRST
  20     [
  21       [ x = UIDENT; q = QUOTATION ->
  22         let (quotation, arg) =
  23           let pos = String.index q ':' in
  24           (String.sub q 0 pos,
  25            String.sub q (pos + 1) (String.length q - pos - 1))
  26         in
  27         debug_print (Printf.sprintf "QUOTATION = %s; ARG = %s" quotation arg);
  28         if quotation = "unicode" then
  29           let text = TXtok (loc, x, expand_unicode_macro arg) in
  30           {used = []; text = text; styp = STlid (loc, "string")}
  31         else
  32           assert false
  33       ]
  34     ];
  35 END
  36