Query results were erroneously tagged as directories.

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index df10be56336e7b55917180c1e7ad6ae2b47f6cbd..6db20400eb9d84caabc4209671d6f8c605371484 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -307,12 +307,25 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     combo#set_active (aux 0 queries);
     win#queryInputText#set_text input
   in
+  let set_whelp_query txt =
+    let query, arg = 
+      try
+        let q = Pcre.extract ~rex:whelp_query_RE txt in
+        q.(1), q.(2)
+      with Invalid_argument _ -> failwith "Malformed Whelp query"
+    in
+    activate_combo_query arg query
+  in
   let toplevel = win#toplevel in
   let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
   let fail msg =
     ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ())
       ~title:"Cic browser" ~msg ~cancel:false ());
   in
+  let tags =
+    [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
+      "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ]
+  in
   let handle_error f =
     try
       f ()
@@ -369,8 +382,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       ignore(win#whelpResultTreeview#connect#row_activated 
         ~callback:(fun _ _ ->
           let selection = self#_getWhelpResultTreeviewSelection () in
+          let is_cic s =
+            try
+              String.sub s 0 5 = "cic:/"
+            with Invalid_argument _ -> false
+          in
           let txt = 
-            if String.sub selection 0 5 = "cic:/" then
+            if is_cic selection then
               selection
             else
               win#browserUri#text ^ selection 
@@ -385,7 +403,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     val mutable current_infos = None
     val mutable current_mathml = None
 
-    val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview
+(*     val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview *)
+    val model =
+      new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
 
     method private _getWhelpResultTreeviewSelection () =
       match model#easy_selection () with
@@ -449,7 +469,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
             | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
             | `Dir dir -> self#_loadDir dir
             | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
-            | `Whelp (query, results) -> self#_loadList results);
+            | `Whelp (query, results) -> 
+                set_whelp_query query;
+                self#_loadList (List.map (fun r -> "obj", r) results));
             self#setEntry entry
           end
       with
@@ -489,8 +511,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _loadDir dir = 
       let content = Http_getter.ls dir in
       let l = List.map (function 
-        | Http_getter_types.Ls_section sec -> sec            
-        | Http_getter_types.Ls_object obj -> obj.Http_getter_types.uri
+        | Http_getter_types.Ls_section sec -> "dir", sec
+        | Http_getter_types.Ls_object obj -> "obj", obj.Http_getter_types.uri
         ) content
       in
       self#_loadList l
@@ -529,7 +551,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private _loadList l =
       model#list_store#clear ();
-      List.iter model#easy_append l;
+      List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
       self#_showList
     
     (** { public methods, all must call _load!! } *)
@@ -547,22 +569,20 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let is_uri txt = 
         try 
           let u = UriManager.strip_xpointer (UriManager.uri_of_string txt) in
-          ignore(Http_getter.resolve' u); true
+          ignore (Http_getter.resolve' u);
+          true
         with
         | Http_getter_types.Key_not_found _ 
-        | Http_getter_types.Unresolvable_URI _ -> false
+        | Http_getter_types.Unresolvable_URI _
+        | UriManager.IllFormedUri ("cic:/" | "cic:") -> false
         | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'")
       in
       let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
       if is_whelp txt then
         begin
-          let q = Pcre.extract ~rex:whelp_query_RE txt in
-          let query, arg = 
-            try
-              q.(1), q.(2)
-            with Invalid_argument _ -> failwith "Malformed Whelp query"
-          in
-          activate_combo_query arg query;
+          set_whelp_query txt;  
+          
+            
           (MatitaScript.instance ())#advance ~statement:(txt^".") ()
         end
       else