* mQueryLevels interface clean-up

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index afbbc143919ccf8fd96bd68974779eae76a3802b..32599cd610163a85e38149dd11ae9aaaa3dd7151 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2376,28 +2376,89 @@ let completeSearchPattern () =
      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+let choose_must list_of_must =
+ let chosen = ref None in
+ let window =
+  GWindow.window
+   ~modal:true ~title:"Query refinement." ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let hbox =
+  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+  GMisc.label
+   ~text:
+    ("You can now specify the genericity of the query. " ^
+     "The more generic the slower.")
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox =
+  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+  GMisc.label
+   ~text:
+    "Suggestion: start with faster queries before moving to more generic ones."
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let notebook =
+  GPack.notebook ~scrollable:true
+   ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let _ =
+  let page = ref 0 in
+  let last = List.length list_of_must in
+  List.map
+   (function must ->
+     incr page ;
+     let label =
+      GMisc.label ~text:
+       (if !page = 1 then "More generic" else
+         if !page = last then "More precise" else "          ") ()
+     in
+     let clist =
+      let expected_height = 25 * (List.length must + 1) in
+       let height = if expected_height > 400 then 400 else expected_height in
+        let scrolled_window =
+         GBin.scrolled_window ~border_width:10 ~height ~width:600
+          ~packing:(notebook#append_page ~tab_label:label#coerce) ()
+        in
+         GList.clist ~columns:2 ~packing:scrolled_window#add
+          ~titles:["URI" ; "Position"] ()
+     in
+      ignore
+       (List.map
+         (function (uri,position) ->
+           let n =
+            clist#append 
+             [uri; if position then "MainConclusion" else "Conclusion"]
+           in
+            clist#set_row ~selectable:false n
+         ) must
+       ) ;
+      clist#columns_autosize ()
+   ) list_of_must in
+ let hbox =
+  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let okb =
+  GButton.button ~label:"Ok"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let cancelb =
+  GButton.button ~label:"Abort"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* actions *)
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+  (okb#connect#clicked
+    (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
+ window#set_position `CENTER ;
+ window#show () ;
+ GMain.Main.main () ;
+ match !chosen with
+    None -> raise NoChoice
+  | Some n -> List.nth list_of_must n
+;;
+
 let searchPattern () =
  let inputt = ((rendering_window ())#inputt : term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
-   let rec get_level ?(last_invalid=false) () =
-    match
-     GToolbox.input_string
-      ~title:"Insert the strictness parameter for the query:"
-      ((if last_invalid then
-         "Invalid input (must be a non-negative natural number). Insert again "
-        else
-         "Insert "
-       ) ^ "the strictness parameter for the query:")
-    with
-       None -> raise NoChoice
-     | Some n ->
-        try
-         int_of_string n
-        with
-         _ -> get_level ~last_invalid:true ()
-   in
-    let level = get_level () in
     let metasenv =
      match !ProofEngine.proof with
         None -> assert false
@@ -2408,8 +2469,7 @@ let searchPattern () =
       | Some metano ->
          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
           let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in
-         let len = List.length list_of_must in
-         let must = if level < len then List.nth list_of_must level else can in
+         let must = choose_must list_of_must in
          let result = MQueryGenerator.searchPattern metasenv ey ty must can in
           let uris =
            List.map
@@ -2418,9 +2478,6 @@ let searchPattern () =
             ) result in
           let html =
            " <h1>Backward Query: </h1>" ^
-           " <h2>Levels: </h2> " ^
-           MQueryLevels.string_of_levels
-            (MQueryLevels.levels_of_term metasenv ey ty) "<br>" ^
           " <pre>" ^ get_last_query result ^ "</pre>"
           in
            output_html outputhtml html ;