added ligatures support

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

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 45ff3d23306e8131883eaf5a0ce13f97e55a41db..bcfd6c9f62282e15163a5e988beb3a736702d41a 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -78,7 +78,7 @@ let make_action action bindings =
     function
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
-    (* LUCA: DEFCON 4 BEGIN *)
+    (* LUCA: DEFCON 3 BEGIN *)
     | Binding (name, Env.TermType) :: tl ->
         Gramext.action
           (fun (v:Ast.term) ->
@@ -101,7 +101,7 @@ let make_action action bindings =
             aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
     | Env _ :: tl ->
         Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
-    (* LUCA: DEFCON 4 END *)
+    (* LUCA: DEFCON 3 END *)
   in
     aux [] (List.rev bindings)
 
@@ -411,7 +411,8 @@ EXTEND
   level2_meta: [
     [ magic = l2_magic -> Ast.Magic magic
     | var = l2_variable -> Ast.Variable var
-    | blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob)
+    | blob = UNPARSED_AST ->
+        !parse_level2_ast_ref (Ulexing.from_utf8_string blob)
     ]
   ];
 END
@@ -470,7 +471,7 @@ EXTEND
         List.map (fun n -> Ast.Ident (n, None)) names, Some ty
     | name = IDENT -> [Ast.Ident (name, None)], None
     | blob = UNPARSED_META ->
-        let meta = !parse_level2_meta_ref (Stream.of_string blob) in
+        let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _) -> [meta], None
         | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None
@@ -480,7 +481,7 @@ EXTEND
   single_arg: [
     [ name = IDENT -> Ast.Ident (name, None)
     | blob = UNPARSED_META ->
-        let meta = !parse_level2_meta_ref (Stream.of_string blob) in
+        let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _)
         | Ast.Variable (Ast.IdentVar _) -> meta
@@ -601,7 +602,8 @@ EXTEND
       | LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN ->
           return_term loc (Ast.Cast (p1, p2))
       | LPAREN; p = term; RPAREN -> p
-      | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
+      | blob = UNPARSED_META ->
+          !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
       ]
     ];
 END
@@ -618,12 +620,17 @@ let exc_located_wrapper f =
   | Stdpp.Exc_located (floc, exn) ->
       raise (Parse_error (floc, (Printexc.to_string exn)))
 
-let parse_level1_pattern stream =
-  exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
-let parse_level2_ast stream =
-  exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast stream)
-let parse_level2_meta stream =
-  exc_located_wrapper (fun () -> Grammar.Entry.parse level2_meta stream)
+let parse_level1_pattern lexbuf =
+  exc_located_wrapper
+    (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf))
+
+let parse_level2_ast lexbuf =
+  exc_located_wrapper
+    (fun () -> Grammar.Entry.parse level2_ast (Obj.magic lexbuf))
+
+let parse_level2_meta lexbuf =
+  exc_located_wrapper
+    (fun () -> Grammar.Entry.parse level2_meta (Obj.magic lexbuf))
 
 let _ =
   parse_level1_pattern_ref := parse_level1_pattern;