From: Stefano Zacchiroli Date: Mon, 7 Feb 2005 15:23:02 +0000 (+0000) Subject: added support for directory browsing in cicBrowser X-Git-Tag: V_0_1_0~5 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77784fbeb858e3cbec8a0ad7cb03f271089b09a3;p=helm.git added support for directory browsing in cicBrowser --- diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index b62587e1d..4b9d9e1f6 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -88,7 +88,7 @@ let interpreter = MatitaInterpreter.interpreter ~console:gui#console ~mathViewer () let _ = let href_callback uri = - let term = CicAst.Uri (UriManager.string_of_uri uri, None) in + let term = CicAst.Uri (uri, None) in ignore (interpreter#evalAst (TacticAst.Command (TacticAst.Check term))) in sequent_viewer#set_href_callback (Some href_callback) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index e572f0982..cde097e9a 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -50,7 +50,7 @@ class clickable_math_view obj = object (self) inherit GMathViewAux.multi_selection_math_view obj - val mutable href_callback: (UriManager.uri -> unit) option = None + val mutable href_callback: (string -> unit) option = None method set_href_callback f = href_callback <- f initializer @@ -65,7 +65,7 @@ class clickable_math_view obj = let uri = elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href in - f (UriManager.uri_of_string (uri#to_string))) + f (uri#to_string)) | Some elt -> ignore (self#action_toggle elt) | None -> ())) method private choose_selection gdome_elt = @@ -267,6 +267,7 @@ let cicBrowsers = ref [] class cicBrowser ~(history:string MatitaMisc.history) () = let term_RE = Pcre.regexp "^term:(.*)" in + let trailing_slash_RE = Pcre.regexp "/$" in let gui = MatitaGui.instance () in let win = gui#newBrowserWin () in let toplevel = win#toplevel in @@ -302,7 +303,7 @@ class cicBrowser ~(history:string MatitaMisc.history) () = GMain.quit (); false)); mathView#set_href_callback (Some (fun uri -> - handle_error (fun () -> self#_loadUri (UriManager.string_of_uri uri)))); + handle_error (fun () -> self#_loadUri uri))); self#_loadUri ~add_to_history:false blank_uri; toplevel#show (); @@ -333,6 +334,7 @@ class cicBrowser ~(history:string MatitaMisc.history) () = | 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 @@ -346,7 +348,8 @@ class cicBrowser ~(history:string MatitaMisc.history) () = method loadUri uri = handle_error (fun () -> self#_loadUri ~add_to_history:true uri) - method private blank () = mathView#load_root MatitaMisc.empty_mathml + method private blank () = + mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement method private home () = if currentProof#onGoing () then @@ -361,6 +364,37 @@ class cicBrowser ~(history:string MatitaMisc.history) () = 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 diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 66508b631..2c27704d2 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -31,7 +31,7 @@ class type clickable_math_view = inherit GMathViewAux.multi_selection_math_view (** set hyperlink callback. None disable hyperlink handling *) - method set_href_callback: (UriManager.uri -> unit) option -> unit + method set_href_callback: (string -> unit) option -> unit end class type sequent_viewer = diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 0bb2ea7e0..c9d8ae4a6 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -49,12 +49,13 @@ let strip_trailing_blanks = let rex = Pcre.regexp "\\s*$" in fun s -> Pcre.replace ~rex s -let empty_mathml = - let doc = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns) - ~qualifiedName:(Gdome.domString "math") ~doctype:None - in - doc#get_documentElement +let empty_mathml () = + Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns) + ~qualifiedName:(Gdome.domString "math") ~doctype:None + +let empty_boxml () = + Misc.domImpl#createDocument ~namespaceURI:(Some Misc.boxml_ns) + ~qualifiedName:(Gdome.domString "box") ~doctype:None exception History_failure diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index a0d19b8b2..79219f174 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -42,7 +42,8 @@ val strip_trailing_blanks: string -> string (** Gdome.element of a MathML document whose rendering should be blank. Used * by cicBrowser to render "about:blank" document *) -val empty_mathml: Gdome.element +val empty_mathml: unit -> Gdome.document +val empty_boxml: unit -> Gdome.document exception History_failure