urimanager removed

[helm.git] / matita / matita / matitaMathView.ml

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index 8a7b8fdcba47988dfbc090223a83422d965bce3f..f418abe6f8e658dc3b78eadc9610b9ed380a865a 100644 (file)
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -65,6 +65,7 @@ let near (x1, y1) (x2, y2) =
   let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
   (distance < 4.)
 
+(*
 let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML"
 let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
 let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
@@ -83,10 +84,12 @@ let empty_mathml = lazy (
 let empty_boxml = lazy (
   domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) 
     ~qualifiedName:(Gdome.domString "box") ~doctype:None)
+    *)
 
   (** shown for goals closed by side effects *)
 let closed_goal_mathml = lazy "chiuso per side effect..."
 
+(*
 (* ids_to_terms should not be passed here, is just for debugging *)
 let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
   assert false (* MATITA 1.0
@@ -177,6 +180,7 @@ let rec has_maction (elt :Gdome.element) =
         has_maction (new Gdome.element_of_node node)
     | _ -> false
 ;;
+*)
 
 class clickableMathView obj =
 let text_width = 80 in
@@ -189,17 +193,17 @@ object (self)
    self#misc#modify_font_by_name
      (sprintf "%s %d" BuildTimeConf.script_font !current_font_size)
   method set_href_callback = (function _ -> () : (string -> unit) option -> unit)
-  method private set_cic_info = (function _ -> () : (Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t *
+  method private set_cic_info = (function _ -> () : unit (*(Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t *
          (Cic.id, Cic.hypothesis) Hashtbl.t *
-         (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option) option -> unit)
+         (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option)*) option -> unit)
   (* dal widget di Luca *)
   method load_root ~root =
     self#buffer#delete ~start:(self#buffer#get_iter `START)
     ~stop:(self#buffer#get_iter `END);
     self#buffer#insert root
   method remove_selections = (() : unit)
-  method set_selection = (fun _ -> () : Gdome.element option -> unit)
-  method get_selections = (assert false : Gdome.element list)
+  method set_selection = (fun _ -> () : unit option -> unit)
+  method get_selections = (assert false : unit list)
   method set_font_size font_size =
    self#misc#modify_font_by_name
      (sprintf "%s %d" BuildTimeConf.script_font font_size)
@@ -991,7 +995,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   object (self)
     inherit scriptAccessor
     
-    val mutable gviz_uri = UriManager.uri_of_string "cic:/dummy.con";
+    val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec";
 
     val dep_contextual_menu = GMenu.menu ()
 
@@ -1017,20 +1021,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
       mathView#set_href_callback (Some (fun uri ->
         handle_error (fun () ->
-         let uri =
-          try
-           `Uri (UriManager.uri_of_string uri)
-          with
-           UriManager.IllFormedUri _ ->
-            `NRef (NReference.reference_of_string uri)
-         in
+         let uri = `NRef (NReference.reference_of_string uri) in
           self#load uri)));
       gviz#connect_href (fun button_ev attrs ->
         let time = GdkEvent.Button.time button_ev in
         let uri = List.assoc "href" attrs in
-        gviz_uri <- UriManager.uri_of_string uri;
+        gviz_uri <- NReference.reference_of_string uri;
         match GdkEvent.Button.button button_ev with
-        | button when button = left_button -> self#load (`Uri gviz_uri)
+        | button when button = left_button -> self#load (`NRef gviz_uri)
         | button when button = right_button ->
             dep_contextual_menu#popup ~button ~time
         | _ -> ());
@@ -1046,10 +1044,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       win#hBugsTutorsMenuItem#misc#hide ();
       connect_menu_item win#browserUrlMenuItem (fun () ->
         win#browserUri#misc#grab_focus ());
-      connect_menu_item win#univMenuItem (fun () ->
-        match self#currentCicUri with
-        | Some uri -> self#load (`Univs uri)
-        | None -> ());
 
       self#_load (`About `Blank);
       toplevel#show ()
@@ -1059,7 +1053,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       (** @return None if no object uri can be built from the current entry *)
     method private currentCicUri =
       match current_entry with
-      | `Uri uri -> Some uri
+      | `NRef uri -> Some uri
       | _ -> None
 
     val model =
@@ -1143,9 +1137,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
                self#_loadTermNCic term metasenv subst ctx
           | `Dir dir -> self#_loadDir dir
           | `HBugs `Tutors -> self#_loadHBugsTutors
-          | `Uri uri -> assert false (* MATITA 1.0 *)
-          | `NRef nref -> self#_loadNReference nref
-          | `Univs uri -> assert false (* MATITA 1.0 *));
+          | `NRef nref -> self#_loadNReference nref);
           self#setEntry entry
         end)
 
@@ -1170,7 +1162,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
        gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
        (match center_on with
        | None -> ()
-       | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
+       | Some uri -> gviz#center_on_href (NReference.string_of_reference uri));
        HExtlib.safe_remove tmpfile
       else
        MatitaGtkMisc.report_error ~title:"graphviz error"
@@ -1310,7 +1302,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         let entry =
           match txt with
           | txt when is_uri txt ->
-              `Uri (UriManager.uri_of_string ((*fix_uri*) txt))
+              `NRef (NReference.reference_of_string ((*fix_uri*) txt))
           | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
           | txt ->
              (try