Interface improvement: a window is opened to show objects returned by the

completeSearchPattern query.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 4363b3beee623f7e22db32dd5658746c8b89859c..3909f06bfaf8090bf0a3d5f87a5730c33eeeb0e3 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -60,10 +60,15 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/public/natile/currentproof";;
-let prooffiletype = "/public/natile/currentprooftype";;
+let prooffile = "/public/sacerdot/currentproof";;
+let prooffiletype = "/public/sacerdot/currentprooftype";;
 
 (* SACERDOT
+let prooffile = "/public/sacerdot/currentproof";;
+let prooffiletype = "/public/sacerdot/currentprooftype";;
+*)
+
+(* NATILE
 let prooffile = "/public/natile/currentproof";;
 let prooffiletype = "/public/natile/currentprooftype";;
 *)
@@ -80,10 +85,15 @@ let prooffiletype = "/home/galata/miohelm/currentprooftype";;
 
 (*CSC: the getter should handle the innertypes, not the FS *)
 
-let innertypesfile = "/public/natile/innertypes";;
-let constanttypefile = "/public/natile/constanttype";;
+let innertypesfile = "/public/sacerdot/innertypes";;
+let constanttypefile = "/public/sacerdot/constanttype";;
 
 (* SACERDOT
+let innertypesfile = "/public/sacerdot/innertypes";;
+let constanttypefile = "/public/sacerdot/constanttype";;
+*)
+
+(* NATILE
 let innertypesfile = "/public/natile/innertypes";;
 let constanttypefile = "/public/natile/constanttype";;
 *)
@@ -2362,6 +2372,39 @@ let open_ () =
         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+let show_query_results results =
+ let window =
+  GWindow.window
+   ~modal:false ~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:"Click on a URI to show that object"
+   ~packing:hbox#add () in
+ let scrolled_window =
+  GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
+   ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
+  ignore
+   (List.map
+     (function (uri,_) ->
+       let n =
+        clist#append [uri]
+       in
+        clist#set_row ~selectable:false n
+     ) results
+   ) ;
+  clist#columns_autosize () ;
+  ignore
+   (clist#connect#select_row
+     (fun ~row ~column ~event ->
+       let (uri,_) = List.nth results row in
+        show_in_show_window_uri (UriManager.uri_of_string uri))
+   ) ;
+  window#show ()
+;;
 
 let completeSearchPattern () =
  let inputt = ((rendering_window ())#inputt : term_editor) in
@@ -2370,9 +2413,8 @@ let completeSearchPattern () =
    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 result = MQueryGenerator.searchPattern must can in 
-    output_html outputhtml
-     ("<h1 color=\"maroon\"><pre>" ^ MQueryUtil.text_of_result result "\n" ^ "</pre></h1>")
+   let results = MQueryGenerator.searchPattern must can in 
+    show_query_results results
   with
    e ->
     output_html outputhtml