- if entry <> current_entry || entry = `About `Current_proof then begin
- (match entry with
- | `About `Current_proof -> self#home ()
- | `About `Blank -> self#blank ()
- | `About `Us -> () (* TODO implement easter egg here :-] *)
- | `Check term -> self#_loadCheck term
- | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
- | `Dir dir -> self#_loadDir dir
- | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
- | `Whelp (query, results) ->
- set_whelp_query query;
- self#_loadList results);
- self#setEntry entry
- end
- with
- | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri)
- | CicEnvironment.Object_not_found uri ->
- fail (sprintf "object not found: %s" (UriManager.string_of_uri uri))
- | Browser_failure msg -> fail msg
+ if entry <> current_entry || reloadable entry then begin
+ (match entry with
+ | `About `Current_proof -> self#home ()
+ | `About `Blank -> self#blank ()
+ | `About `Us -> () (* TODO implement easter egg here :-] *)
+ | `Check term -> self#_loadCheck term
+ | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
+ | `Dir dir -> self#_loadDir dir
+ | `Uri uri -> self#_loadUriManagerUri uri
+ | `Whelp (query, results) ->
+ set_whelp_query query;
+ self#_loadList (List.map (fun r -> "obj",
+ UriManager.string_of_uri r) results));
+ self#setEntry entry
+ end
+ with exn -> fail (MatitaExcPp.to_string exn)