+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
(******************************************************************************)
(* *)
(* PROJECT HELM *)
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
exception NoCurrentUri;;
exception NoNextOrPrevUri;;
-exception GtkInterfaceInternalError;;
let theory_get_current_uri () =
match !theory_visited_uris with
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 () =
;;
(* 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
+let jump rendering_window (node : Ominidom.o_mDOMNode) =
+ let module O = Ominidom in
+ match (node#get_attribute (O.o_mDOMString_of_string "href")) with
+ Some str ->
+ let s = str#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
+ | None -> assert false
+;;
+
+let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
+ let module O = Ominidom in
+ let rec aux node =
+ match node#get_attribute (O.o_mDOMString_of_string "xref") with
+ Some _ -> rendering_window#output#set_selection (Some node)
+ | None -> aux (node#get_parent)
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 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)
- in
- match node with
- None -> !(rendering_window#output)#set_selection None
- | Some node -> aux node
+ match node with
+ Some x -> aux x
+ | None -> rendering_window#output#set_selection None
;;
update_output rendering_window uri'
;;
-(* CSC: unificare con la creazione la prima volta *)
-let rec updateb_pressed theory_rendering_window rendering_window
- (sw1, sw ,(hbox : GPack.box)) mktree ()
-=
- Getter.update () ;
- (* let's empty the uri trees and rebuild them *)
- uritree := [] ;
- theoryuritree := [] ;
- build_uri_tree () ;
- hbox#remove !sw1#coerce ;
- hbox#remove !sw#coerce ;
-
+let create_gtk_trees (hbox : GPack.box) rendering_window theory_rendering_window mktree =
let sw3 =
GBin.scrolled_window ~width:250 ~height:600
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
let tree1 =
GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in
let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in
- sw1 := sw3 ;
- ignore(tree_item1#connect#select
- (theory_selection_changed theory_rendering_window None)) ;
- mktree theory_selection_changed theory_rendering_window tree_item1
- (Dir ("theory:/",theoryuritree)) ;
let sw2 =
GBin.scrolled_window ~width:250 ~height:600
let tree =
GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in
let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in
- sw := sw2 ;
+
ignore(tree_item#connect#select (selection_changed rendering_window None)) ;
- mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree))
+ mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) ;
+
+ ignore(tree_item1#connect#select
+ (theory_selection_changed theory_rendering_window None)) ;
+ mktree theory_selection_changed theory_rendering_window tree_item1
+ (Dir ("theory:/",theoryuritree)) ;
+ (sw3,sw2)
+;;
+
+let updateb_pressed theory_rendering_window rendering_window
+ (sw1, sw ,(hbox : GPack.box)) mktree ()
+=
+ Getter.update () ;
+ (* let's empty the uri trees and rebuild them *)
+ uritree := [] ;
+ theoryuritree := [] ;
+ build_uri_tree () ;
+ hbox#remove !sw1#coerce ;
+ hbox#remove !sw#coerce ;
+ let (sw3,sw2) =
+ create_gtk_trees hbox rendering_window theory_rendering_window mktree
+ in
+ sw1 := sw3 ;
+ sw := sw2
;;
let theory_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
+ match rendering_window#output#get_selection with
+ | Some node ->
+ begin
+ match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
+ | Some xpath ->
+ 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#get_string) ;
+ CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
+ 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 () ;
+ | None ->
(* 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 ("\nNo xref found\n")
+ end
+ | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
;;
(* called when the annotation is confirmed *)
else
!ann := None ;
match !annotated_obj with
- None -> raise GtkInterfaceInternalError
+ None -> assert false
| Some (annobj,_) ->
let uri = get_current_uri () in
let annxml = Annotation2Xml.pp_annotation annobj uri in
Dir (dirname, content) ->
let subtree = GTree.tree () in
treeitem#set_subtree subtree ;
- List.iter
- (fun ti ->
- let label = get_name ti
- and uri = get_uri ti in
- let treeitem2 = GTree.tree_item ~label:label () in
- subtree#append treeitem2 ;
- ignore(treeitem2#connect#select
- (selection_changed rendering_window uri)) ;
- aux treeitem2 ti
- ) (List.sort compare !content)
+ let expand_sons =
+ List.map
+ (fun ti ->
+ let label = get_name ti
+ and uri = get_uri ti in
+ let treeitem2 = GTree.tree_item ~label:label () in
+ subtree#append treeitem2 ;
+ ignore(treeitem2#connect#select
+ (selection_changed rendering_window uri)) ;
+ (* Almost lazy function *)
+ (fun () -> aux treeitem2 ti)
+ ) (List.sort compare !content)
+ in
+ let lazy_expand_sons = lazy (List.iter (fun f -> f ()) expand_sons) in
+ ignore(treeitem#connect#expand
+ (fun () -> Lazy.force lazy_expand_sons)) ;
| _ -> ()
in
aux
(* Stuff for the widget settings *)
-let export_to_postscript output () =
- !output#export_to_postscript "output.ps" ;
+let export_to_postscript (output : GMathView.math_view) () =
+ output#export_to_postscript ~filename:"output.ps" ();
;;
-let activate_t1 output sw is_set jump_callback selection_changed_callback
- last_uri ()
+let activate_t1 output button_set_anti_aliasing button_set_kerning
+ button_export_to_postscript button_t1 ()
=
- is_set := not !is_set ;
- sw#remove !output#coerce ;
- output :=
- (GMathView.math_view ~packing:sw#add ~width:400 ~height:380
- ~use_t1_lib:!is_set ()) ;
- !output#load !last_uri ;
- ignore(!output#connect#jump jump_callback) ;
- ignore(!output#connect#selection_changed selection_changed_callback) ;
+ let is_set = button_t1#active in
+ output#set_font_manager_type
+ (if is_set then `font_manager_t1 else `font_manager_gtk) ;
+ 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 is_set () =
- is_set := not !is_set ;
- !output#set_anti_aliasing !is_set
+let set_anti_aliasing output button_set_anti_aliasing () =
+ output#set_anti_aliasing button_set_anti_aliasing#active
;;
-let set_kerning output is_set () =
- is_set := not !is_set ;
- !output#set_kerning !is_set
+let set_kerning output button_set_kerning () =
+ 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 jump_callback selection_changed_callback
- last_uri
+class settings_window output sw button_export_to_postscript jump_callback
+ selection_changed_callback
=
let settings_window = GWindow.window ~title:"GtkMathView settings" () in
- let table = GPack.table ~rows:5 ~columns:5 ~packing:settings_window#add () in
+ let vbox =
+ GPack.vbox ~packing:settings_window#add () in
+ let table =
+ GPack.table
+ ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+ ~border_width:5 ~packing:vbox#add () in
let button_t1 =
GButton.toggle_button ~label:"activate t1 fonts"
~packing:(table#attach ~left:0 ~top:0) () in
+ let button_set_anti_aliasing =
+ GButton.toggle_button ~label:"set_anti_aliasing"
+ ~packing:(table#attach ~left:1 ~top:0) () in
+ let button_set_kerning =
+ GButton.toggle_button ~label:"set_kerning"
+ ~packing:(table#attach ~left:2 ~top:0) () in
+ let table =
+ GPack.table
+ ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+ ~border_width:5 ~packing:vbox#add () in
+ let font_size_label =
+ GMisc.label ~text:"font size:"
+ ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
let font_size_spinb =
let sadj =
GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
in
GEdit.spin_button
- ~adjustment:sadj ~packing:(table#attach ~left:4 ~top:2) () in
- let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:3) () in
- let button_set_kerning =
- GButton.toggle_button ~label:"set_kerning"
- ~packing:(table#attach ~left:3 ~top:3) () in
+ ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
+ let log_verbosity_label =
+ GMisc.label ~text:"log verbosity:"
+ ~packing:(table#attach ~left:0 ~top:1) () in
let log_verbosity_spinb =
let sadj =
GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
in
GEdit.spin_button
- ~adjustment:sadj ~packing:(table#attach ~left:2 ~top:2) () in
+ ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let closeb =
+ GButton.button ~label:"Close"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
object(self)
method show = settings_window#show
initializer
+ button_set_anti_aliasing#misc#set_sensitive false ;
+ button_set_kerning#misc#set_sensitive false ;
(* Signals connection *)
- let is_set_use_t1_lib = ref false in
- ignore(button_t1#connect#clicked
- (activate_t1 output sw is_set_use_t1_lib jump_callback
- selection_changed_callback last_uri)) ;
+ ignore(button_t1#connect#clicked
+ (activate_t1 output button_set_anti_aliasing button_set_kerning
+ button_export_to_postscript button_t1)) ;
ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
- let is_set_anti_aliasing = ref false in
- ignore(button_set_anti_aliasing#connect#toggled
- (set_anti_aliasing output is_set_anti_aliasing));
- let is_set_kerning = ref false in
- ignore(button_set_kerning#connect#toggled
- (set_kerning output is_set_kerning)) ;
+ ignore(button_set_anti_aliasing#connect#toggled
+ (set_anti_aliasing output button_set_anti_aliasing));
+ ignore(button_set_kerning#connect#toggled
+ (set_kerning output button_set_kerning)) ;
ignore(log_verbosity_spinb#connect#changed
- (set_log_verbosity output log_verbosity_spinb))
+ (set_log_verbosity output log_verbosity_spinb)) ;
+ ignore(closeb#connect#clicked settings_window#misc#hide)
end;;
(* Main windows *)
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 *)
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 () ->
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
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
nextb#misc#set_sensitive false ;
prevb#misc#set_sensitive false ;
+ 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)) ;
+ (* LUCA: check disabled while compression is not fully implemented *)
+ (* ignore(checkb#connect#clicked (check self)) ; *)
+ checkb#misc#set_sensitive false ;
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
- (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 ))
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
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
nextb#misc#set_sensitive false ;
prevb#misc#set_sensitive false ;
+ 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
- (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) ;
let win = GWindow.window ~title:"Known uris" ~border_width:2 () in
let vbox = GPack.vbox ~packing:win#add () in
let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in
- let sw1 = GBin.scrolled_window ~width:250 ~height:600
- ~packing:(hbox1#pack ~padding:5) () in
- let tree1 =
- GTree.tree ~selection_mode:`BROWSE ~packing:sw1#add_with_viewport () in
- let tree_item1 =
- GTree.tree_item ~label:theorylabel ~packing:tree1#append () in
- let sw = GBin.scrolled_window ~width:250 ~height:600
- ~packing:(hbox1#pack ~padding:5) () in
- let tree =
- GTree.tree ~selection_mode:`BROWSE ~packing:sw#add_with_viewport () in
- let tree_item =
- GTree.tree_item ~label:label ~packing:tree#append () in
+ let (sw1,sw) =
+ create_gtk_trees hbox1 rendering_window theory_rendering_window mktree
+ in
let hbox =
GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
let updateb =
object (self)
method show () = win#show ()
initializer
- mktree theory_selection_changed theory_rendering_window tree_item1
- (Dir ("theory:/",theoryuritree));
- mktree selection_changed rendering_window tree_item
- (Dir ("cic:/",uritree));
-
(* signal handlers here *)
- ignore (tree_item1#connect#select
- ~callback:(theory_selection_changed theory_rendering_window None)) ;
- ignore (tree_item#connect#select
- ~callback:(selection_changed rendering_window None)) ;
ignore (win#connect#destroy ~callback:GMain.Main.quit) ;
ignore (quitb#connect#clicked GMain.Main.quit) ;
ignore(updateb#connect#clicked (updateb_pressed
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
projects / helm.git / blobdiff