]> matita.cs.unibo.it Git - helm.git/commitdiff
Upgraded to mml-widget version 0.2.1
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2000 17:17:32 +0000 (17:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2000 17:17:32 +0000 (17:17 +0000)
helm/interface/Makefile
helm/interface/cadet
helm/interface/mmlinterface.ml
helm/interface/uris_of_filenames.pl

index c3aa28f87aeeae9ca6ee6f155e0c063d13de66b2..d2fddf453bf4c6751910f1d402dc31f1217794a0 100644 (file)
@@ -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 \
index 7df42fecdac359a032622f1e44afa44d4b6de612..c9762da761572d8e497cdc7527d741c9352a0f7d 100755 (executable)
@@ -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
 
index 496e35e55527af64d82782983d18b8a642d0483c..a164883a5c47cde36bda6ee58e82a7ddea76629d 100755 (executable)
@@ -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
index d738f51b746e379b0c597244f17a1904e45a0ec2..e06ac822a0eb50a1a29c3802efb99752022d0954 100755 (executable)
@@ -4,7 +4,7 @@ while(<STDIN>) {
    chomp;
    split / /;
    for (@_) {
-      if (/.*\.(con|var|ind)\.xml/)
+      if (/.*\.(con|var|ind)(\.types)?\.xml/)
        { s/\./cic:/; }
       elsif (/.*\.theory\.xml/)
        { s/\./theory:/; }