+ (* loads a uri which can be a cic uri or an about:* uri
+ * @param uri string *)
+ method private _loadUri ?(add_to_history = true) uri =
+ try
+ if current_uri <> uri || uri = current_proof_uri then begin
+ (match uri with
+ | uri when uri = blank_uri -> self#blank ()
+ | uri when uri = current_proof_uri -> self#home ()
+ | uri when Pcre.pmatch ~rex:term_RE uri ->
+ self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1))
+ | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri));
+ self#setUri uri;
+ if add_to_history then history#add uri
+ end
+ with
+ | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri)
+ | CicEnvironment.Object_not_found _ ->
+ fail (sprintf "object not found: %s" uri)
+ | Browser_failure msg -> fail msg
+
+ method loadUri uri =
+ handle_error (fun () -> self#_loadUri ~add_to_history:true uri)
+
+ method private blank () = mathView#load_root MatitaMisc.empty_mathml
+
+ method private home () =
+ if currentProof#onGoing () then
+ self#loadObj (cicCurrentProof currentProof#proof#proof)
+ else
+ raise (Browser_failure "no on going proof")
+
+ (** loads a cic uri from the environment
+ * @param uri UriManager.uri *)
+ method private loadUriManagerUri uri =
+ let uri = UriManager.strip_xpointer uri in
+ let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ self#loadObj obj
+
+ method private setUri uri =
+ win#browserUri#set_text uri;
+ current_uri <- uri
+
+ method private loadObj obj =
+ let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
+ let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+ ids_to_hypotheses,_,_))) =
+ ApplyTransformation.mml_of_cic_object obj
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids,
+ ids_to_conjectures, ids_to_hypotheses);
+ match current_mathml with
+ | Some current_mathml when use_diff ->
+ mathView#freeze;
+ XmlDiff.update_dom ~from:current_mathml mathml;
+ mathView#thaw
+ | _ ->
+ mathView#load_root ~root:mathml#get_documentElement;
+ current_mathml <- Some mathml