]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/disambiguate.ml
HBugs compile again (but it does not do anything right now: still to be
[helm.git] / helm / gTopLevel / disambiguate.ml
index ce41208dd3ba2833f68b105376f56166a6300ae0..efb1c05081d06cd16f1f748e72cfc2be8d21b7f8 100644 (file)
@@ -46,7 +46,7 @@ module type Callbacks =
 
     val output_html : string -> unit
     val interactive_user_uri_choice :
-      selection_mode:[`SINGLE | `EXTENDED] ->
+      selection_mode:[`SINGLE | `MULTIPLE] ->
       ?ok:string ->
       ?enable_button_for_non_vars:bool ->
       title:string -> msg:string -> id:string -> string list -> string list
@@ -73,9 +73,9 @@ module Make(C:Callbacks) =
         MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
       ) result in
      C.output_html "<h1>Locate Query: </h1><pre>";
-     MQueryUtil.text_of_query C.output_html query ""
+     MQueryUtil.text_of_query C.output_html "" query
      C.output_html "<h1>Result:</h1>";
-     MQueryUtil.text_of_result C.output_html result "<br>";
+     MQueryUtil.text_of_result C.output_html "<br>" result;
      let uris' =
       match uris with
          [] ->
@@ -85,7 +85,7 @@ module Make(C:Callbacks) =
        | [uri] -> [uri]
        | _ ->
          C.interactive_user_uri_choice
-          ~selection_mode:`EXTENDED
+          ~selection_mode:`MULTIPLE
           ~ok:"Try every selection."
           ~enable_button_for_non_vars:true
           ~title:"Ambiguous input."