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 ()
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
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
| `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
| `Whelp (query, results) ->
set_whelp_query query;
- self#_loadList results);
+ self#_loadList (List.map (fun r -> "obj", r) results));
self#setEntry entry
end
with
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
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!! } *)
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