From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Dec 2002 16:02:52 +0000 (+0000)
Subject: New feature: the user can now enter the list of "must" constraints he wants.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=15d5b7a1d16dd2f25d3f09ac3575c63e4c792818;p=helm.git

New feature: the user can now enter the list of "must" constraints he wants.
---

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 () =
      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
-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