X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=7aa54f2c74ed03a3407bc4b4d18e5165f67c6da3;hb=393b5943416585d0612ec62b795ceee34adb8dd7;hp=7bf464a9d8390b8fea4783e6cd93220a1a4398af;hpb=ef9ec8cb57d15426a96fe40d056eb07804753bb9;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 7bf464a9d..7aa54f2c7 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 =
@@ -139,29 +139,30 @@ class sequent_viewer obj =
         selections
   
   method load_sequent metasenv metano =
-(*
-    let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
-        ids_to_hypotheses) =
-      Cic2acic.asequent_of_sequent metasenv conjecture
-    in
-*)
     let sequent = CicUtil.lookup_meta metano metasenv in
     let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
+(*
     debug_print "load_sequent: dumping MathML to ./prova";
     ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
+*)
     self#load_root ~root:mathml#get_documentElement
  end
 
 
 class sequents_viewer ~(notebook:GPack.notebook)
-  ~(sequent_viewer:sequent_viewer) ~set_goal ()
+  ~(sequent_viewer:sequent_viewer) ()
 =
   let tab_label metano =
     (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
   in
+  let set_goal goal =
+    let currentProof = MatitaProof.instance () in
+    assert (currentProof#onGoing ());
+    currentProof#proof#set_goal goal
+  in
   object (self)
     val mutable pages = 0
     val mutable switch_page_callback = None
@@ -169,8 +170,17 @@ class sequents_viewer ~(notebook:GPack.notebook)
     val mutable goal2page = []  (* the other way round *)
     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
     val mutable _metasenv = []
+    val mutable scrolledWin: GBin.scrolled_window option = None
+      (* scrolled window to which the sequent_viewer is currently attached *)
 
     method reset =
+      (match scrolledWin with
+      | Some w ->
+          (* removing page from the notebook will destroy all contained widget,
+          * we do not want the sequent_viewer to be destroyed as well *)
+          w#remove sequent_viewer#coerce;
+          scrolledWin <- None
+      | None -> ());
       for i = 1 to pages do notebook#remove_page 0 done;
       pages <- 0;
       page2goal <- [];
@@ -193,6 +203,7 @@ class sequents_viewer ~(notebook:GPack.notebook)
             ~shadow_type:`IN ~show:true ()
         in
         let reparent () =
+          scrolledWin <- Some w;
           match sequent_viewer#misc#parent with
           | None -> w#add sequent_viewer#coerce
           | Some _ -> sequent_viewer#misc#reparent w#coerce
@@ -232,7 +243,7 @@ class sequents_viewer ~(notebook:GPack.notebook)
         with Not_found -> assert false
       in
       notebook#goto_page page;
-      self#render_page page goal;
+      self#render_page page goal
 
   end
 
@@ -265,13 +276,9 @@ exception Browser_failure of string
 
 let cicBrowsers = ref []
 
-class cicBrowser 
-  ~(disambiguator:MatitaTypes.disambiguator)
-  ~(currentProof:MatitaTypes.currentProof)
-  ~(history:string MatitaMisc.history)
-  ()
-=
+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
@@ -286,24 +293,34 @@ class cicBrowser
     with exn ->
       fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
   in
+  let handle_error' f = fun () -> handle_error f in  (* used in callbacks *)
   object (self)
     initializer
-      ignore (win#browserUri#connect#activate (fun () ->
-        self#_loadUri win#browserUri#text));
-      ignore (win#browserHomeButton#connect#clicked (fun () ->
-        self#_loadUri current_proof_uri));
-      ignore (win#browserRefreshButton#connect#clicked self#refresh);
-      ignore (win#browserBackButton#connect#clicked self#back);
-      ignore (win#browserForwardButton#connect#clicked self#forward);
+      ignore (win#browserUri#connect#activate (handle_error' (fun () ->
+        self#_loadUri win#browserUri#text)));
+      ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
+        self#_loadUri current_proof_uri)));
+      ignore (win#browserRefreshButton#connect#clicked
+        (handle_error' self#refresh));
+      ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
+      ignore (win#browserForwardButton#connect#clicked
+        (handle_error' self#forward));
       ignore (win#toplevel#event#connect#delete (fun _ ->
         let my_id = Oo.id self in
         cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
+        if !cicBrowsers = [] &&
+          Helm_registry.get "matita.mode" = "cicbrowser"
+        then
+          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 ();
 
+    val disambiguator = MatitaDisambiguator.instance ()
+    val currentProof = MatitaProof.instance ()
+
     val mutable current_uri = ""
     val mutable current_infos = None
     val mutable current_mathml = None
@@ -328,6 +345,7 @@ class cicBrowser
           | 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
@@ -341,7 +359,8 @@ class cicBrowser
     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
@@ -356,6 +375,37 @@ class cicBrowser
       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
@@ -414,14 +464,14 @@ class cicBrowser
   end
 
 let sequents_viewer ~(notebook:GPack.notebook)
-  ~(sequent_viewer:sequent_viewer) ~set_goal ()
+  ~(sequent_viewer:sequent_viewer) ()
 =
-  new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
+  new sequents_viewer ~notebook ~sequent_viewer ()
 
-let cicBrowser ~disambiguator ~currentProof () =
+let cicBrowser () =
   let size = BuildTimeConf.browser_history_size in
   let rec aux history =
-    let browser = new cicBrowser ~disambiguator ~currentProof ~history () in
+    let browser = new cicBrowser ~history () in
     let win = browser#win in
     ignore (win#browserNewButton#connect#clicked (fun () ->
       let history =
@@ -442,13 +492,20 @@ let cicBrowser ~disambiguator ~currentProof () =
 
 let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
 
-class mathViewer ~disambiguator ~currentProof =
+class mathViewer =
   object
     method checkTerm (src:MatitaTypes.term_source) =
-      let browser = cicBrowser ~disambiguator ~currentProof () in
-      browser#loadTerm src
+      (cicBrowser ())#loadTerm src
   end
 
-let mathViewer ~disambiguator ~currentProof () =
-  new mathViewer ~disambiguator ~currentProof
+let mathViewer () = new mathViewer
+
+let default_sequent_viewer () = sequent_viewer ~show:true ()
+let sequent_viewer_instance = MatitaMisc.singleton default_sequent_viewer
+
+let default_sequents_viewer () =
+  let gui = MatitaGui.instance () in
+  let sequent_viewer = sequent_viewer_instance () in
+  sequents_viewer ~notebook:gui#main#sequentsNotebook ~sequent_viewer ()
+let sequents_viewer_instance = MatitaMisc.singleton default_sequents_viewer