notation_id were compared using Pervasives.equal this was rarely triggering the

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index f58bd21b59b460295d196e3a095f626ac8298e48..5236193d054257091e2962ea626d20f90122777d 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -214,6 +214,19 @@ let extract_term_production pattern =
 
 type rule_id = Grammar.token Gramext.g_symbol list
 
+let compare_rule_id x y =
+  let rec aux = function
+    | [],[] -> 0
+    | [],_ -> ~-1
+    | _,[] -> 1
+    | s1::tl1, s2::tl2 ->
+        if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
+        else 
+          let d = List.length tl1 - List.length tl2 in
+          if d <> 0 then d else 1 (* bad and broken *)
+  in
+    aux (x,y)
+
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23