From 15d5b7a1d16dd2f25d3f09ac3575c63e4c792818 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Dec 2002 16:02:52 +0000 Subject: [PATCH] New feature: the user can now enter the list of "must" constraints he wants. --- helm/gTopLevel/gTopLevel.ml | 72 ++++++++++++++++++++++++++++++------- 1 file changed, 59 insertions(+), 13 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 32599cd61..a3e369057 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -2376,8 +2376,9 @@ let completeSearchPattern () = ("

" ^ Printexc.to_string e ^ "

") ; ;; -let choose_must list_of_must = +let choose_must list_of_must can = let chosen = ref None in + let user_constraints = ref [] in let window = GWindow.window ~modal:true ~title:"Query refinement." ~border_width:2 () in @@ -2409,17 +2410,15 @@ let choose_must list_of_must = let label = GMisc.label ~text: (if !page = 1 then "More generic" else - if !page = last then "More precise" else " ") () - in + if !page = last then "More precise" else " ") () in + let expected_height = 25 * (List.length must + 2) 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 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"] () + GList.clist ~columns:2 ~packing:scrolled_window#add + ~titles:["URI" ; "Position"] () in ignore (List.map @@ -2433,6 +2432,48 @@ let choose_must list_of_must = ) ; clist#columns_autosize () ) list_of_must in + let _ = + let label = GMisc.label ~text:"User provided" () in + let vbox = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:"Select the constraints that must be satisfied and press OK." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length can + 2) 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:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + GList.clist ~columns:2 ~packing:scrolled_window#add + ~selection_mode:`EXTENDED + ~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:true n + ) can + ) ; + clist#columns_autosize () ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + user_constraints := (List.nth can row)::!user_constraints)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + user_constraints := + List.filter + (function uri -> uri != (List.nth can row)) !user_constraints)) ; + in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let okb = @@ -2452,7 +2493,12 @@ let choose_must list_of_must = GMain.Main.main () ; match !chosen with None -> raise NoChoice - | Some n -> List.nth list_of_must n + | Some n -> + if n = List.length list_of_must then + (* user provided constraints *) + !user_constraints + else + List.nth list_of_must n ;; let searchPattern () = @@ -2469,7 +2515,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 must = choose_must list_of_must in + let must = choose_must list_of_must can in let result = MQueryGenerator.searchPattern metasenv ey ty must can in let uris = List.map -- 2.39.2