The disambiguation now returns a list of interpretations.

[helm.git] / helm / gTopLevel / batchParser.ml

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
index 7cbc31201ab39f1a3e98c3f27e27a7c3f74401a4..515c417cb4cc1e29d996e3b9ae9b450ba96d9ebc 100644 (file)
--- a/helm/gTopLevel/batchParser.ml
+++ b/helm/gTopLevel/batchParser.ml
@@ -44,7 +44,14 @@ module DisambiguateCallbacks =
    ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
      List.filter !uri_predicate choices
 
-  let interactive_interpretation_choice _ = fail "Multiple interpretations"
+  let interactive_interpretation_choice =
+   let rec aux n =
+    function
+       [] -> []
+     | _::tl -> n::(aux (n+1) tl)
+   in
+    aux 0
+
   let input_or_locate_uri ~title = fail "Unknown identifier"
  end
 
@@ -59,12 +66,11 @@ let parse mqi_handle ?(uri_pred = constants_only) =
   let empty_context = [] in
   let empty_metasenv = [] in
   fun input ->
-    let (_, metasenv, term) =
-      Disambiguate'.disambiguate_term
-        mqi_handle empty_context empty_metasenv input empty_environment
-    in
-    (metasenv, term)
+   List.map (fun (_,metasenv,term) -> metasenv,term)
+    (Disambiguate'.disambiguate_term
+      mqi_handle empty_context empty_metasenv input empty_environment)
 
 let parse_pp mqi_handle ?uri_pred input = 
-   CicPp.ppterm (snd (parse mqi_handle ?uri_pred input))
+ List.map (fun (_,t) -> CicPp.ppterm t)
+  (parse mqi_handle ?uri_pred input)