]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationParser.expanded.ml
version 0.7.1
[helm.git] / helm / ocaml / cic_notation / cicNotationParser.expanded.ml
index fcbc081a7474d9e8b4f61bf95ff92cfc906c32cd..0adf84723ce7587f88c66f5018a3d8320e373f68 100644 (file)
@@ -54,37 +54,27 @@ ttype binding =
 llet make_action action bindings =
   let rec aux (vl : env_type) =
     function
-      [] ->
-        prerr_endline "aux: make_action";
-        Gramext.action (fun (loc : location) -> action vl loc)
-    | NoBinding :: tl ->
-        prerr_endline "aux: none"; Gramext.action (fun _ -> aux vl tl)
+      [] -> Gramext.action (fun (loc : location) -> action vl loc)
+    | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
     | Binding (name, TermType) :: tl ->
-        prerr_endline "aux: term";
         Gramext.action
           (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
     | Binding (name, StringType) :: tl ->
-        prerr_endline "aux: string";
         Gramext.action
           (fun (v : string) ->
              aux ((name, (StringType, StringValue v)) :: vl) tl)
     | Binding (name, NumType) :: tl ->
-        prerr_endline "aux: num";
         Gramext.action
           (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
     | Binding (name, OptType t) :: tl ->
-        prerr_endline "aux: opt";
         Gramext.action
           (fun (v : 'a option) ->
              aux ((name, (OptType t, OptValue v)) :: vl) tl)
     | Binding (name, ListType t) :: tl ->
-        prerr_endline "aux: list";
         Gramext.action
           (fun (v : 'a list) ->
              aux ((name, (ListType t, ListValue v)) :: vl) tl)
-    | Env _ :: tl ->
-        prerr_endline "aux: env";
-        Gramext.action (fun (v : env_type) -> aux (v @ vl) tl)
+    | Env _ :: tl -> Gramext.action (fun (v : env_type) -> aux (v @ vl) tl)
   in
   aux [] (List.rev bindings)
 llet flatten_opt =
@@ -125,7 +115,7 @@ let extract_term_production pattern =
         [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"] @
           aux p1
     | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
-    | Break -> []
+(*     | Break -> [] *)
     | Box (_, pl) -> List.flatten (List.map aux pl)
   and aux_magic magic =
     match magic with
@@ -975,8 +965,7 @@ let _ =
         [Gramext.Stoken ("NUMBER", "")],
         Gramext.action
           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
-             (prerr_endline "number"; return_term loc (Num (n, 0)) :
-              'l2_pattern));
+             (return_term loc (Num (n, 0)) : 'l2_pattern));
         [Gramext.Stoken ("URI", "")],
         Gramext.action
           (fun (u : string) (loc : Lexing.position * Lexing.position) ->