From: Claudio Sacerdoti Coen Date: Thu, 30 Nov 2000 17:17:32 +0000 (+0000) Subject: Upgraded to mml-widget version 0.2.1 X-Git-Tag: nogzip~126 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=458ba0f68b06b74a3d947c6496dc23a509715a89;p=helm.git Upgraded to mml-widget version 0.2.1 --- diff --git a/helm/interface/Makefile b/helm/interface/Makefile index c3aa28f87..d2fddf453 100644 --- a/helm/interface/Makefile +++ b/helm/interface/Makefile @@ -1,6 +1,6 @@ LABLGTK_DIR = /usr/lib/ocaml/lablgtk LABLGTK_MATHVIEW_DIR = /usr/lib/ocaml/lablgtk/mathview -MINIDOM_DIR = /usr/lib/ocaml/lablgtk/mathview/minidom +MINIDOM_DIR = /usr/lib/ocaml/minidom PXP_DIR = /usr/lib/ocaml/site-lib/pxp NETSTRING_DIR = /usr/lib/ocaml/site-lib/netstring OCAMLC = ocamlc -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview @@ -106,8 +106,9 @@ depend: mmlinterface: $(MMLINTERFACEOBJS) $(OCAMLC) -custom -o mmlinterface str.cma unix.cma $(PXPLIBS) dbm.cma \ lablgtk.cma gtkInit.cmo \ - $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cma \ $(MINIDOM_DIR)/minidom.cmo \ + $(MINIDOM_DIR)/ominidom.cmo \ + $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cma \ $(MMLINTERFACEOBJS) \ -cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \ -rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \ @@ -119,8 +120,9 @@ mmlinterface: $(MMLINTERFACEOBJS) mmlinterface.opt: $(MMLINTERFACEOPTOBJS) $(OCAMLOPT) -o mmlinterface.opt str.cmxa $(PXPLIBSOPT) unix.cmxa \ dbm.cmxa lablgtk.cmxa gtkInit.cmx \ - $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cmxa \ $(MINIDOM_DIR)/minidom.cmx \ + $(MINIDOM_DIR)/ominidom.cmx \ + $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cmxa \ $(MMLINTERFACEOPTOBJS) \ -cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \ -rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \ diff --git a/helm/interface/cadet b/helm/interface/cadet index 7df42fecd..c9762da76 100755 --- a/helm/interface/cadet +++ b/helm/interface/cadet @@ -6,10 +6,10 @@ export LD_LIBRARY_PATH=/usr/local/lib:$LD_LIBRARY_PATH # WARNING!!! No "//" in the middle of the path, nor a "/" at the end!!!! #V6.2 -export HELM_CONFIGURATION_PREFIX=~/HELM/installation +#export HELM_CONFIGURATION_PREFIX=~/HELM/installation #V7 -#export HELM_CONFIGURATION_PREFIX=/home/cadet/sacerdot +export HELM_CONFIGURATION_PREFIX=/home/cadet/sacerdot export T1LIB_CONFIG=./t1.config diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 496e35e55..a164883a5 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -28,10 +28,6 @@ type item = let uritree = ref [] let theoryuritree = ref [] -(* Brutti, per via del widget che non e' imperativo *) -let loaded_uri = ref "";; -let theory_loaded_uri = ref "";; - let get_name = function Dir (name,_) -> name @@ -146,16 +142,14 @@ let theory_update_output rendering_window uri = rendering_window#label#set_text (UriManager.string_of_uri uri) ; ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ; let mmlfile = XsltProcessor.process uri true "theory" in - theory_loaded_uri := mmlfile ; - !(rendering_window#output)#load mmlfile + rendering_window#output#load mmlfile ;; let update_output rendering_window uri = rendering_window#label#set_text (UriManager.string_of_uri uri) ; ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ; let mmlfile = XsltProcessor.process uri true "cic" in - loaded_uri := mmlfile ; - !(rendering_window#output)#load mmlfile + rendering_window#output#load mmlfile ;; let theory_next rendering_window () = @@ -211,38 +205,31 @@ let prev rendering_window () = ;; (* called when an hyperlink is clicked *) -let jump rendering_window node = - let module M = Minidom in - let s = - match M.node_get_attribute node (M.mDOMString_of_string "href") with - None -> assert false - | Some s -> M.string_of_mDOMString s - in - let uri = UriManager.uri_of_string s in - rendering_window#show () ; - rendering_window#prevb#misc#set_sensitive true ; - rendering_window#nextb#misc#set_sensitive false ; - visited_uris := uri::!visited_uris ; - to_visit_uris := [] ; - annotated_obj := None ; - update_output rendering_window uri -;; - -let choose_selection rendering_window node = - let module M = Minidom in +let jump rendering_window (node : Ominidom.o_mDOMNode) = + let module O = Ominidom in + let s = (node#get_attribute (O.o_mDOMString_of_string "href"))#get_string in + let uri = UriManager.uri_of_string s in + rendering_window#show () ; + rendering_window#prevb#misc#set_sensitive true ; + rendering_window#nextb#misc#set_sensitive false ; + visited_uris := uri::!visited_uris ; + to_visit_uris := [] ; + annotated_obj := None ; + update_output rendering_window uri +;; + +let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) = + let module O = Ominidom in let rec aux node = - match M.node_get_attribute node (M.mDOMString_of_string "xref") with - None -> - let parent = - match M.node_get_parent node with - None -> assert false - | Some parent -> parent - in - aux parent - | Some s -> !(rendering_window#output)#set_selection (Some node) + try + let _ = node#get_attribute (O.o_mDOMString_of_string "xref") in + rendering_window#output#set_selection node + with + O.Minidom_exception _ -> + aux (node#get_parent) in match node with - None -> !(rendering_window#output)#set_selection None + None -> rendering_window#output#reset_selection | Some node -> aux node ;; @@ -339,41 +326,41 @@ let check rendering_window () = ;; let annotateb_pressed rendering_window annotation_window () = - let module M = Minidom in - match !(rendering_window#output)#get_selection with - None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" - | Some node -> - let xpath = - match M.node_get_attribute node (M.mDOMString_of_string "xref") with - None -> assert false - | Some xpath -> M.string_of_mDOMString xpath - in - try - let annobj = get_annotated_obj () + let module O = Ominidom in + try + let node = rendering_window#output#get_selection in + let xpath = + (node#get_attribute (O.o_mDOMString_of_string "xref"))#get_string + in + try + let annobj = get_annotated_obj () + (* next "cast" can't got rid of, but I don't know why *) + and annotation = (annotation_window#annotation : GEdit.text) in + ann := CicXPath.get_annotation annobj xpath ; + CicAnnotationHinter.create_hints annotation_window annobj xpath ; + annotation#delete_text 0 annotation#length ; + begin + match !(!ann) with + None -> + annotation#misc#set_sensitive false ; + annotation_window#radio_none#set_active true ; + radio_some_status := false + | Some ann' -> + annotation#insert ann' ; + annotation#misc#set_sensitive true ; + annotation_window#radio_some#set_active true ; + radio_some_status := true + end ; + GMain.Grab.add (annotation_window#window_to_annotate#coerce) ; + annotation_window#show () ; + with + e -> (* next "cast" can't got rid of, but I don't know why *) - and annotation = (annotation_window#annotation : GEdit.text) in - ann := CicXPath.get_annotation annobj xpath ; - CicAnnotationHinter.create_hints annotation_window annobj xpath ; - annotation#delete_text 0 annotation#length ; - begin - match !(!ann) with - None -> - annotation#misc#set_sensitive false ; - annotation_window#radio_none#set_active true ; - radio_some_status := false - | Some ann' -> - annotation#insert ann' ; - annotation#misc#set_sensitive true ; - annotation_window#radio_some#set_active true ; - radio_some_status := true - end ; - GMain.Grab.add (annotation_window#window_to_annotate#coerce) ; - annotation_window#show () ; - with - e -> - (* next "cast" can't got rid of, but I don't know why *) - let errors = (rendering_window#errors : GEdit.text) in - errors#insert ("\n" ^ Printexc.to_string e ^ "\n") + let errors = (rendering_window#errors : GEdit.text) in + errors#insert ("\n" ^ Printexc.to_string e ^ "\n") + with + O.Minidom_exception _ -> + (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" ;; (* called when the annotation is confirmed *) @@ -425,61 +412,51 @@ let mktree selection_changed rendering_window = (* Stuff for the widget settings *) let export_to_postscript output () = - !output#export_to_postscript "output.ps" ; + output#export_to_postscript ~width:595 ~height:822 ~x_margin:72 + ~y_margin:72 ~disable_colors:false "output.ps" ; ;; let activate_t1 output button_set_anti_aliasing button_set_kerning - button_export_to_postscript sw button_t1 jump_callback - selection_changed_callback last_uri () + button_export_to_postscript button_t1 () = let is_set = button_t1#active in - sw#remove !output#coerce ; - let font_size = !output#get_font_size in - let log_verbosity = !output#get_log_verbosity in - let anti_aliasing = button_set_anti_aliasing#active in - let kerning = button_set_kerning#active in - output := - (GMathView.math_view ~packing:sw#add ~width:400 ~height:380 - ~use_t1_lib:is_set ()) ; - !output#set_font_size font_size ; - !output#set_log_verbosity log_verbosity ; - if is_set then - begin - button_set_anti_aliasing#misc#set_sensitive true ; - button_set_kerning#misc#set_sensitive true ; - button_export_to_postscript#misc#set_sensitive true ; - !output#set_anti_aliasing anti_aliasing ; - !output#set_kerning kerning ; - end - else - begin - button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; - button_export_to_postscript#misc#set_sensitive false ; - end ; - !output#load !last_uri ; - ignore(!output#connect#jump jump_callback) ; - ignore(!output#connect#selection_changed selection_changed_callback) ; + output#set_font_manager_type + (if is_set then + GtkMathView.MathView.FontManagerT1 + else + GtkMathView.MathView.FontManagerGtk) ; + if is_set then + begin + button_set_anti_aliasing#misc#set_sensitive true ; + button_set_kerning#misc#set_sensitive true ; + button_export_to_postscript#misc#set_sensitive true ; + end + else + begin + button_set_anti_aliasing#misc#set_sensitive false ; + button_set_kerning#misc#set_sensitive false ; + button_export_to_postscript#misc#set_sensitive false ; + end ;; let set_anti_aliasing output button_set_anti_aliasing () = - !output#set_anti_aliasing button_set_anti_aliasing#active + output#set_anti_aliasing button_set_anti_aliasing#active ;; let set_kerning output button_set_kerning () = - !output#set_kerning button_set_kerning#active + output#set_kerning button_set_kerning#active ;; let changefont output font_size_spinb () = - !output#set_font_size font_size_spinb#value_as_int + output#set_font_size font_size_spinb#value_as_int ;; let set_log_verbosity output log_verbosity_spinb () = - !output#set_log_verbosity log_verbosity_spinb#value_as_int + output#set_log_verbosity log_verbosity_spinb#value_as_int ;; class settings_window output sw button_export_to_postscript jump_callback - selection_changed_callback last_uri + selection_changed_callback = let settings_window = GWindow.window ~title:"GtkMathView settings" () in let vbox = @@ -532,8 +509,7 @@ object(self) (* Signals connection *) ignore(button_t1#connect#clicked (activate_t1 output button_set_anti_aliasing button_set_kerning - button_export_to_postscript sw button_t1 jump_callback - selection_changed_callback last_uri)) ; + button_export_to_postscript button_t1)) ; ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; ignore(button_set_anti_aliasing#connect#toggled (set_anti_aliasing output button_set_anti_aliasing)); @@ -585,7 +561,7 @@ object (self) method radio_some = radio_some method radio_none = radio_none method annotation_hints = annotation_hints - method output = (output : GMathView.math_view ref) + method output = (output : GMathView.math_view) method show () = window_to_annotate#show () initializer (* signal handlers here *) @@ -606,8 +582,7 @@ object (self) visited_uris := new_current_uri::(List.tl !visited_uris) ; label#set_text (UriManager.string_of_uri new_current_uri) ; let mmlfile = parse_no_cache new_current_uri in - loaded_uri := mmlfile ; - !output#load mmlfile + output#load mmlfile )) ; ignore (abortb#connect#clicked (fun () -> @@ -633,7 +608,7 @@ class rendering_window annotation_window output (label : GMisc.label) = GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in - let _ = scrolled_window0#add !output#coerce in + let _ = scrolled_window0#add output#coerce in let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in @@ -665,7 +640,7 @@ object(self) method nextb = nextb method prevb = prevb method label = label - method output = (output : GMathView.math_view ref) + method output = (output : GMathView.math_view) method errors = errors method show () = window#show () initializer @@ -674,15 +649,15 @@ object(self) button_export_to_postscript#misc#set_sensitive false ; (* signal handlers here *) - ignore(!output#connect#jump (jump self)) ; - ignore(!output#connect#selection_changed (choose_selection self)) ; + ignore(output#connect#jump (jump self)) ; + ignore(output#connect#selection_changed (choose_selection self)) ; ignore(nextb#connect#clicked (next self)) ; ignore(prevb#connect#clicked (prev self)) ; ignore(checkb#connect#clicked (check self)) ; ignore(closeb#connect#clicked window#misc#hide) ; ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ; let settings_window = new settings_window output scrolled_window0 - button_export_to_postscript (jump self) (choose_selection self) loaded_uri in + button_export_to_postscript (jump self) (choose_selection self) in ignore(settingsb#connect#clicked settings_window#show) ; ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) @@ -701,8 +676,7 @@ class theory_rendering_window rendering_window = let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in let output = - ref (GMathView.math_view ~use_t1_lib:false ~width:400 ~height:380 - ~packing:scrolled_window0#add ()) in + GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in @@ -731,7 +705,7 @@ object(self) method nextb = nextb method prevb = prevb method label = label - method output = (output : GMathView.math_view ref) + method output = (output : GMathView.math_view) method errors = errors method show () = window#show () initializer @@ -740,14 +714,13 @@ object(self) button_export_to_postscript#misc#set_sensitive false ; (* signal handlers here *) - ignore(!output#connect#jump (jump rendering_window)) ; - ignore(!output#connect#selection_changed (choose_selection self)) ; + ignore(output#connect#jump (jump rendering_window)) ; + ignore(output#connect#selection_changed (choose_selection self)) ; ignore(nextb#connect#clicked (theory_next self)) ; ignore(prevb#connect#clicked (theory_prev self)) ; ignore(checkb#connect#clicked (theory_check self)) ; let settings_window = new settings_window output scrolled_window0 - button_export_to_postscript (jump rendering_window) (choose_selection self) - theory_loaded_uri in + button_export_to_postscript (jump rendering_window)(choose_selection self) in ignore(settingsb#connect#clicked settings_window#show) ; ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; ignore(closeb#connect#clicked window#misc#hide) ; @@ -805,8 +778,7 @@ end;; let _ = build_uri_tree () ; - let output = - ref (GMathView.math_view ~use_t1_lib:false ~width:400 ~height:380 ()) + let output = GMathView.math_view ~width:400 ~height:380 () and label = GMisc.label ~text:"???" () in let annotation_window = new annotation_window output label in let rendering_window = new rendering_window annotation_window output label in diff --git a/helm/interface/uris_of_filenames.pl b/helm/interface/uris_of_filenames.pl index d738f51b7..e06ac822a 100755 --- a/helm/interface/uris_of_filenames.pl +++ b/helm/interface/uris_of_filenames.pl @@ -4,7 +4,7 @@ while() { chomp; split / /; for (@_) { - if (/.*\.(con|var|ind)\.xml/) + if (/.*\.(con|var|ind)(\.types)?\.xml/) { s/\./cic:/; } elsif (/.*\.theory\.xml/) { s/\./theory:/; }