From: Stefano Zacchiroli Date: Mon, 12 Sep 2005 09:18:15 +0000 (+0000) Subject: Filled pre-generated notation levels with productions on dummy tokens (never generate... X-Git-Tag: V_0_1_2_1~47 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5709e4317f5c401435afe89d24bb798284c20921;p=helm.git Filled pre-generated notation levels with productions on dummy tokens (never generated by the lexer). This hack works around a bug in camlp4 which on delete_rule remove an entire precedence level if it gets empty after the delete_rule invocation. --- diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 13817e248..90324541d 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -278,15 +278,23 @@ let fold_binder binder pt_names body = let return_term loc term = Ast.AttributedTerm (`Loc loc, term) -let _ = (* create empty precedence level for "term" *) + (* create empty precedence level for "term" *) +let _ = + let dummy_action = + Gramext.action (fun _ -> + failwith "internal error, lexer generated a dummy token") + in + (* Needed since campl4 on "delete_rule" remove the precedence level if it gets + * empty after the deletion. The lexer never generate the Stoken below. *) + let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in let mk_level_list first last = let rec aux acc = function | i when i < first -> acc | i -> aux - ((Some (string_of_int i ^ "N"), Some Gramext.NonA, []) - :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, []) - :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, []) + ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod) + :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, dummy_prod) + :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, dummy_prod) :: acc) (i - 1) in