+ (* 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))
+ | uri when Pcre.pmatch ~rex:trailing_slash_RE uri -> self#loadDir uri
+ | _ -> 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 ())#get_documentElement
+
+ 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 loadDir dir =
+ let mathml = MatitaMisc.empty_boxml () in
+ let content = Http_getter.ls dir in
+ let root = mathml#get_documentElement in
+ let new_box_elt name =
+ mathml#createElementNS ~namespaceURI:(Some Misc.boxml_ns)
+ ~qualifiedName:(Gdome.domString ("b:" ^ name))
+ in
+ let new_text content = mathml#createTextNode (Gdome.domString content) in
+ let b_v = new_box_elt "v" in
+ List.iter
+ (fun item ->
+ let b_text = new_box_elt "text" in
+ let uri, elt =
+ match item with
+ | Http_getter_types.Ls_section subdir ->
+ (dir ^ subdir ^ "/"), (new_text (subdir ^ "/"))
+ | Http_getter_types.Ls_object obj ->
+ (dir ^ obj.Http_getter_types.uri),
+ (new_text obj.Http_getter_types.uri)
+ in
+ b_text#setAttributeNS ~namespaceURI:(Some Misc.xlink_ns)
+ ~qualifiedName:(Gdome.domString "xlink:href")
+ ~value:(Gdome.domString uri);
+ ignore (b_v#appendChild ~newChild:(b_text :> Gdome.node));
+ ignore (b_text#appendChild ~newChild:(elt :> Gdome.node)))
+ content;
+ ignore (root#appendChild ~newChild:(b_v :> Gdome.node));
+(* Misc.domImpl#saveDocumentToFile ~doc:mathml ~name:"pippo" (); *)
+ mathView#load_root ~root:root
+
+ 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