From: Claudio Sacerdoti Coen Date: Fri, 6 Dec 2002 13:18:47 +0000 (+0000) Subject: The user interface for the completeSearchPattern query has been improved. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a772e377c1ca7c43c3e1e25eb47479fc3c5ceb9e;p=helm.git The user interface for the completeSearchPattern query has been improved. It is now "easy" to query for induction principles, for example. Much work still to do. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index afef8b4bb..890f5d75f 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1140,8 +1140,7 @@ let ("

" ^ Printexc.to_string e ^ "

") ; in let show_in_show_window_uri uri = - CicTypeChecker.typecheck uri ; - let obj = CicEnvironment.get_cooked_obj uri in + let obj = CicEnvironment.get_obj uri in show_in_show_window_obj uri obj in let show_in_show_window_callback mmlwidget (n : Gdome.element) = @@ -2375,7 +2374,7 @@ let open_ () = let show_query_results results = let window = GWindow.window - ~modal:false ~title:"Query refinement." ~border_width:2 () in + ~modal:false ~title:"Query results." ~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 @@ -2415,14 +2414,112 @@ let show_query_results results = window#show () ;; +let + refine_constraints (must_obj,must_rel,must_sort) (only_obj,only_rel,only_sort) += + let chosen = ref false in + let use_only = ref false in + let window = + GWindow.window + ~modal:true ~title:"Constraints 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: "\"Only\" constraints can be enforced or not." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let onlyb = + GButton.toggle_button ~label:"Enforce \"only\" constraints" + ~active:false ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) + () + in + ignore + (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ; + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on Rels." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* Rel constraints *) + let expected_height = 25 * (List.length must_rel + 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 scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let rel_constraints = + List.map + (function (position,depth) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:position + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match depth with + None -> position, ref None + | Some depth' -> + let mutable_ref = ref (Some depth') in + let depthb = + GButton.toggle_button ~label:(string_of_int depth') + ~active:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) + () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some depth' else None in + mutable_ref := sel_depth + )) ; + position, mutable_ref + ) must_rel 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 + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())); + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + if !chosen then + let chosen_must_rel = + List.map +(* + (function (position,ref_depth) -> position,!ref_depth) rel_constraints +*) +(function (position,ref_depth) -> prerr_endline ("### " ^ position ^ " " ^ match !ref_depth with None -> "NULL" | Some d -> string_of_int d) ; position,!ref_depth) rel_constraints + in + (must_obj,chosen_must_rel,must_sort), + (if !use_only then +(*CSC: ???????????????????????? I assume that must and only are the same... *) + only_obj,Some chosen_must_rel,only_sort + else + None,None,None + ) + else + raise NoChoice +;; + let completeSearchPattern () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in - let must,can = MQueryLevels2.get_constraints expr in - let results = MQueryGenerator.searchPattern must can in + let must,only = MQueryLevels2.get_constraints expr in + let must',only' = refine_constraints must only in + let results = MQueryGenerator.searchPattern must' only' in show_query_results results with e -> @@ -2430,7 +2527,7 @@ let completeSearchPattern () = ("

" ^ Printexc.to_string e ^ "

") ; ;; -let choose_must list_of_must can = +let choose_must list_of_must only = let chosen = ref None in let user_constraints = ref [] in let window = @@ -2496,7 +2593,7 @@ let choose_must list_of_must can = 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 expected_height = 25 * (List.length only + 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 @@ -2514,19 +2611,19 @@ let choose_must list_of_must can = [uri; if position then "MainConclusion" else "Conclusion"] in clist#set_row ~selectable:true n - ) can + ) only ) ; clist#columns_autosize () ; ignore (clist#connect#select_row (fun ~row ~column ~event -> - user_constraints := (List.nth can row)::!user_constraints)) ; + user_constraints := (List.nth only 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)) ; + (function uri -> uri != (List.nth only row)) !user_constraints)) ; in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in @@ -2568,16 +2665,22 @@ let searchPattern () = None -> () | 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 can in + let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in + let must = choose_must list_of_must only 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) + 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 rigth_only = Some (List.map torigth_restriction only) in + let result = + MQueryGenerator.searchPattern + (rigth_must,[],[]) (rigth_only,None,None) in let uris = List.map (function uri,_ ->