added ligatures support

[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 9f07baa4a77f62bc83394dd43425652d2289da36..5caba868b1e220b2392f337f17e56317baaa2d2f 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -373,10 +373,12 @@ EXTEND
       p2 = 
         [ blob = UNPARSED_AST ->
             add_raw_attribute ~text:(sprintf "@{%s}" blob)
-              (CicNotationParser.parse_level2_ast (Stream.of_string blob))
+              (CicNotationParser.parse_level2_ast
+                (Ulexing.from_utf8_string blob))
         | blob = UNPARSED_META ->
             add_raw_attribute ~text:(sprintf "${%s}" blob)
-              (CicNotationParser.parse_level2_meta (Stream.of_string blob))
+              (CicNotationParser.parse_level2_meta
+                (Ulexing.from_utf8_string blob))
         ] ->
           let assoc =
             match assoc with
@@ -390,7 +392,8 @@ EXTEND
           in
           let p1 =
             add_raw_attribute ~text:s
-              (CicNotationParser.parse_level1_pattern (Stream.of_string s))
+              (CicNotationParser.parse_level1_pattern
+                (Ulexing.from_utf8_string s))
           in
           (dir, p1, assoc, prec, p2)
     ]
@@ -504,11 +507,14 @@ let exc_located_wrapper f =
   | Stdpp.Exc_located (floc, exn) ->
       raise (CicNotationParser.Parse_error (floc, (Printexc.to_string exn)))
 
-let parse_statement stream =
-  exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statement lexbuf =
+  exc_located_wrapper
+    (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
 
-let parse_dependencies stream = 
-  let tok_stream,_ = CicNotationLexer.level2_ast_lexer.Token.tok_func stream in
+let parse_dependencies lexbuf = 
+  let tok_stream,_ =
+    CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf)
+  in
   let rec parse acc = 
     (parser
     | [< '("URI", u) >] ->