(* *)
(* PROJECT HELM *)
(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* Claudio Sacerdoti Coen <natile@cs.unibo.it> *)
(* 06/01/2002 *)
(* *)
(* *)
"</html>"
;;
-let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+let prooffile = "/public/natile/currentproof";;
+let prooffiletype = "/public/natile/currentprooftype";;
(* SACERDOT
-let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+let prooffile = "/public/natile/currentproof";;
+let prooffiletype = "/public/natile/currentprooftype";;
*)
(* TASSI
(*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+let innertypesfile = "/public/natile/innertypes";;
+let constanttypefile = "/public/natile/constanttype";;
(* SACERDOT
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+let innertypesfile = "/public/natile/innertypes";;
+let constanttypefile = "/public/natile/constanttype";;
*)
(* TASSI
try
let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in
let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in
- ignore (MQueryLevels2.get_constraints expr)
+ let must,can = MQueryLevels2.get_constraints expr in
+ let result = MQueryGenerator.searchPattern must can in
+ output_html outputhtml
+ ("<h1 color=\"maroon\"><pre>" ^ MQueryUtil.text_of_result result "\n" ^ "</pre></h1>")
with
e ->
output_html outputhtml
("<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
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
) ;
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 =
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 () =
| 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 result = MQueryGenerator.searchPattern metasenv ey ty must can in
+ let must = choose_must list_of_must can in
+ let torigth_restriction (u,b) =
+ let p = if b then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
+ else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" in
+ (u,p,None)
+ in
+ let rigth_must = List.map torigth_restriction must in
+ let rigth_can = Some (List.map torigth_restriction can) in
+ let result = MQueryGenerator.searchPattern (rigth_must,[],[]) (rigth_can,None,None) in
let uris =
List.map
(function uri,_ ->
projects / helm.git / blobdiff