]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/termAcicContent.ml
- matitacLib: better handling of the callbacks for the dump operation
[helm.git] / helm / software / components / acic_content / termAcicContent.ml
index 508411d2847b1b84083141efa5bbe14aed16a8fa..c350f38c41ab03c6a735643e676d2e53809e1009 100644 (file)
@@ -442,19 +442,22 @@ let set_active_interpretations ids =
 
 exception Interpretation_not_found
 
-let lookup_interpretations symbol =
+let lookup_interpretations ?(sorted=true) symbol =
   try
-   HExtlib.list_uniq
-    (List.sort Pervasives.compare
-     (List.map
-      (fun id ->
-        let (dsc, _, args, appl_pattern) =
-          try
-            Hashtbl.find !level2_patterns32 id
-          with Not_found -> assert false 
-        in
-        dsc, args, appl_pattern)
-      !(Hashtbl.find !interpretations symbol)))
+    let raw = 
+      List.map (
+        fun id ->
+          let (dsc, _, args, appl_pattern) =
+            try
+              Hashtbl.find !level2_patterns32 id
+            with Not_found -> assert false 
+          in
+          dsc, args, appl_pattern
+      )
+      !(Hashtbl.find !interpretations symbol)
+    in
+    if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+              else raw
   with Not_found -> raise Interpretation_not_found
 
 let remove_interpretation id =