added support for directory browsing in cicBrowser

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index b62587e1d229a389d88c7fc64e7006e35554f3b5..4b9d9e1f60c0ac4fb2b389c8e814265658b4ff8e 100644 (file)
--- 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 e572f0982f80d7b6cb1d5d2ddf9b0697f05999d6..cde097e9af15342c5d67dc5b2023f6d6bbf3f2fd 100644 (file)
--- 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 66508b6316dad6a55891d48654ec6733e9875e0d..2c27704d2395838b684a157362238dd43ded1ab8 100644 (file)
--- 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 0bb2ea7e0ec2101e5726838d6cad4cdc12a05a76..c9d8ae4a6dbc313a2ede0b2110468afaec6c044d 100644 (file)
--- 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 a0d19b8b21f89bbfecf8d8f1d6d73f84d3fdef42..79219f174be1a770350c4654efda6cf9c4a8ab27 100644 (file)
--- 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