+++ /dev/null
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 24/01/2000 *)
-(* *)
-(* This is a simple gtk interface to the Coq-like pretty printer cicPp for *)
-(* cic terms exported in xml. It uses directly the modules cicPp and *)
-(* cicCcache and indirectly all the other modules (cicParser, cicParser2, *)
-(* cicParser3, getter). *)
-(* The syntax is "gtkInterface[.opt] filename1 ... filenamen" where *)
-(* filenamei is the path-name of an xml file describing a cic term. *)
-(* The terms are loaded in cache and then pretty-printed one at a time and *)
-(* only once, when the user wants to look at it: if the user wants to look at *)
-(* a term again, then the pretty-printed term is showed again, but not *)
-(* recomputed *)
-(* *)
-(******************************************************************************)
-
-(* DEFINITION OF THE URI TREE AND USEFUL FUNCTIONS ON IT *)
-
-type item =
- Dir of string * item list ref
- | File of string * UriManager.uri
-;;
-
-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
- | File (name,_) -> name
-;;
-
-let get_uri =
- function
- Dir _ -> None
- | File (_,uri) -> Some uri
-;;
-
-(* STUFF TO BUILD THE URI TREE *)
-
-exception EmptyUri
-exception DuplicatedUri
-exception ConflictingUris
-
-let insert_in_uri_tree uri =
- let rec aux l =
- function
- [name] ->
- (try
- let _ = List.find (fun item -> name = get_name item) !l in
- raise DuplicatedUri
- with
- Not_found -> l := (File (name,uri))::!l
- )
- | name::tl ->
- (try
- match List.find (fun item -> name = get_name item) !l with
- Dir (_,children) -> aux children tl
- | File _ -> raise ConflictingUris
- with
- Not_found ->
- let children = ref [] in
- l := (Dir (name,children))::!l ;
- aux children tl
- )
- | [] -> raise EmptyUri
- in
- aux
-;;
-
-(* Imperative procedure that builds the two uri trees *)
-let build_uri_tree () =
- let dbh = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0 in
- Dbm.iter
- (fun uri _ ->
- let cicregexp = Str.regexp "cic:"
- and theoryregexp = Str.regexp "theory:" in
- if Str.string_match cicregexp uri 0 then
- let s = Str.replace_first cicregexp "" uri in
- let l = Str.split (Str.regexp "/") s in
- insert_in_uri_tree (UriManager.uri_of_string uri) uritree l
- else if Str.string_match theoryregexp uri 0 then
- let s = Str.replace_first theoryregexp "" uri in
- let l = Str.split (Str.regexp "/") s in
- insert_in_uri_tree (UriManager.uri_of_string uri) theoryuritree l
- ) dbh ;
- Dbm.close dbh
-;;
-
-(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
-
-let annotated_obj = ref None;; (* reference to a couple option where *)
- (* the first component is the current *)
- (* annotated object and the second is *)
- (* the map from ids to annotated targets *)
-let ann = ref (ref None);; (* current annotation *)
-let radio_some_status = ref false;; (* is the radio_some button selected? *)
-
-let theory_visited_uris = ref [];;
-let theory_to_visit_uris = ref [];;
-let visited_uris = ref [];;
-let to_visit_uris = ref [];;
-
-(* CALLBACKS *)
-
-exception NoCurrentUri;;
-exception NoNextOrPrevUri;;
-exception GtkInterfaceInternalError;;
-
-let theory_get_current_uri () =
- match !theory_visited_uris with
- [] -> raise NoCurrentUri
- | uri::_ -> uri
-;;
-
-let get_current_uri () =
- match !visited_uris with
- [] -> raise NoCurrentUri
- | uri::_ -> uri
-;;
-
-let get_annotated_obj () =
- match !annotated_obj with
- None ->
- let (annobj, ids_to_targets,_) =
- (CicCache.get_annobj (get_current_uri ()))
- in
- annotated_obj := Some (annobj, ids_to_targets) ;
- (annobj, ids_to_targets)
- | Some annobj -> annobj
-;;
-
-let filename_of_uri uri =
- Getter.get uri
-;;
-
-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
-;;
-
-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
-;;
-
-let theory_next rendering_window () =
- match !theory_to_visit_uris with
- [] -> raise NoNextOrPrevUri
- | uri::tl ->
- theory_to_visit_uris := tl ;
- theory_visited_uris := uri::!theory_visited_uris ;
- theory_update_output rendering_window uri ;
- rendering_window#prevb#misc#set_sensitive true ;
- if tl = [] then
- rendering_window#nextb#misc#set_sensitive false
-;;
-
-let next rendering_window () =
- match !to_visit_uris with
- [] -> raise NoNextOrPrevUri
- | uri::tl ->
- to_visit_uris := tl ;
- visited_uris := uri::!visited_uris ;
- annotated_obj := None ;
- update_output rendering_window uri ;
- rendering_window#prevb#misc#set_sensitive true ;
- if tl = [] then
- rendering_window#nextb#misc#set_sensitive false
-;;
-
-let theory_prev rendering_window () =
- match !theory_visited_uris with
- [] -> raise NoCurrentUri
- | [_] -> raise NoNextOrPrevUri
- | uri::(uri'::tl as newvu) ->
- theory_visited_uris := newvu ;
- theory_to_visit_uris := uri::!theory_to_visit_uris ;
- theory_update_output rendering_window uri' ;
- rendering_window#nextb#misc#set_sensitive true ;
- if tl = [] then
- rendering_window#prevb#misc#set_sensitive false
-;;
-
-let prev rendering_window () =
- match !visited_uris with
- [] -> raise NoCurrentUri
- | [_] -> raise NoNextOrPrevUri
- | uri::(uri'::tl as newvu) ->
- visited_uris := newvu ;
- to_visit_uris := uri::!to_visit_uris ;
- annotated_obj := None ;
- update_output rendering_window uri' ;
- rendering_window#nextb#misc#set_sensitive true ;
- if tl = [] then
- rendering_window#prevb#misc#set_sensitive false
-;;
-
-(* 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 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
-;;
-
-
-let theory_selection_changed rendering_window uri () =
- match uri with
- None -> ()
- | Some uri' ->
- if !theory_visited_uris <> [] then
- rendering_window#prevb#misc#set_sensitive true ;
- rendering_window#nextb#misc#set_sensitive false ;
- theory_visited_uris := uri'::!theory_visited_uris ;
- theory_to_visit_uris := [] ;
- rendering_window#show () ;
- theory_update_output rendering_window uri'
-;;
-
-let selection_changed rendering_window uri () =
- match uri with
- None -> ()
- | Some uri' ->
- if !visited_uris <> [] then
- 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 ;
- rendering_window#show () ;
- 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 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
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- 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))
-;;
-
-let theory_check rendering_window () =
- let output =
- try
- TheoryTypeChecker.typecheck (theory_get_current_uri ());
- "Type Checking was successful"
- with
- TheoryTypeChecker.NotWellTyped s ->
- "Type Checking was NOT successful:\n\t" ^ s
- in
- (* next "cast" can't got rid of, but I don't know why *)
- let errors = (rendering_window#errors : GEdit.text) in
- let _ = errors#delete_text 0 errors#length in
- errors#insert output
-;;
-
-let check rendering_window () =
- let output =
- try
- CicTypeChecker.typecheck (get_current_uri ());
- "Type Checking was successful"
- with
- CicTypeChecker.NotWellTyped s -> "Type Checking was NOT successful:\n\t" ^ s
- in
- (* next "cast" can't got rid of, but I don't know why *)
- let errors = (rendering_window#errors : GEdit.text) in
- let _ = errors#delete_text 0 errors#length in
- errors#insert output
-;;
-
-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 ()
- (* 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")
-;;
-
-(* called when the annotation is confirmed *)
-let save_annotation annotation =
- if !radio_some_status then
- !ann := Some (annotation#get_chars 0 annotation#length)
- else
- !ann := None ;
- match !annotated_obj with
- None -> raise GtkInterfaceInternalError
- | Some (annobj,_) ->
- let uri = get_current_uri () in
- let annxml = Annotation2Xml.pp_annotation annobj uri in
- Xml.pp annxml (Some (fst (Getter.get_ann_file_name_and_uri uri)))
-;;
-
-let parse_no_cache uri =
- let module U = UriManager in
- XsltProcessor.process uri false "cic"
-;;
-
-
-(* STUFF TO BUILD THE GTK INTERFACE *)
-
-(* Stuff to build the tree window *)
-
-(* selection_changed is actually selection_changed or theory_selection_changed*)
-let mktree selection_changed rendering_window =
- let rec aux treeitem =
- function
- 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)
- | _ -> ()
- in
- aux
-;;
-
-(* Stuff for the widget settings *)
-
-let export_to_postscript output () =
- !output#export_to_postscript "output.ps" ;
-;;
-
-let activate_t1 output sw is_set jump_callback selection_changed_callback
- last_uri ()
-=
- 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 set_anti_aliasing output is_set () =
- is_set := not !is_set ;
- !output#set_anti_aliasing !is_set
-;;
-
-let set_kerning output is_set () =
- is_set := not !is_set ;
- !output#set_kerning !is_set
-;;
-
-let changefont output font_size_spinb () =
- !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
-;;
-
-class settings_window output sw jump_callback selection_changed_callback
- last_uri
-=
- let settings_window = GWindow.window ~title:"GtkMathView settings" () in
- let table = GPack.table ~rows:5 ~columns:5 ~packing:settings_window#add () in
- let button_t1 =
- GButton.toggle_button ~label:"activate t1 fonts"
- ~packing:(table#attach ~left:0 ~top:0) () 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
- 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
-object(self)
- method show = settings_window#show
- initializer
- (* 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(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(log_verbosity_spinb#connect#changed
- (set_log_verbosity output log_verbosity_spinb))
-end;;
-
-(* Main windows *)
-
-class annotation_window output label =
- let window_to_annotate =
- GWindow.window ~title:"Annotating environment" ~border_width:2 () in
- let hbox1 =
- GPack.hbox ~packing:window_to_annotate#add () in
- let vbox1 =
- GPack.vbox ~packing:(hbox1#pack ~padding:5) () in
- let hbox2 =
- GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
- let radio_some = GButton.radio_button ~label:"Annotation below"
- ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
- let radio_none = GButton.radio_button ~label:"No annotation"
- ~group:radio_some#group
- ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5)
- ~active:true () in
- let annotation = GEdit.text ~editable:true ~width:400 ~height:180
- ~packing:(vbox1#pack ~padding:5) () in
- let table =
- GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in
- let annotation_hints =
- Array.init 9
- (function i ->
- GButton.button ~label:("Hint " ^ string_of_int i)
- ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) ()
- ) in
- let vbox2 =
- GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
- let confirmb =
- GButton.button ~label:"O.K."
- ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
- let abortb =
- GButton.button ~label:"Abort"
- ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in
-object (self)
- method window_to_annotate = window_to_annotate
- method annotation = annotation
- method radio_some = radio_some
- method radio_none = radio_none
- method annotation_hints = annotation_hints
- method output = (output : GMathView.math_view ref)
- method show () = window_to_annotate#show ()
- initializer
- (* signal handlers here *)
- ignore (window_to_annotate#event#connect#delete
- (fun _ ->
- window_to_annotate#misc#hide () ;
- GMain.Grab.remove (window_to_annotate#coerce) ;
- true
- )) ;
- ignore (confirmb#connect#clicked
- (fun () ->
- window_to_annotate#misc#hide () ;
- save_annotation annotation ;
- GMain.Grab.remove (window_to_annotate#coerce) ;
- let new_current_uri =
- (snd (Getter.get_ann_file_name_and_uri (get_current_uri ())))
- in
- 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
- )) ;
- ignore (abortb#connect#clicked
- (fun () ->
- window_to_annotate#misc#hide () ;
- GMain.Grab.remove (window_to_annotate#coerce)
- ));
- ignore (radio_some#connect#clicked
- (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
- ignore (radio_none #connect#clicked
- (fun () ->
- annotation#misc#set_sensitive false;
- radio_some_status := false)
- )
-end;;
-
-class rendering_window annotation_window output (label : GMisc.label) =
- let window =
- GWindow.window ~title:"MathML viewer" ~border_width:2 () in
- let vbox =
- GPack.vbox ~packing:window#add () in
- let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
- let paned =
- 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_window =
- GBin.scrolled_window
- ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
- let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
- let hbox =
- GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
- let prevb =
- GButton.button ~label:"Prev"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let nextb =
- GButton.button ~label:"Next"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let checkb =
- GButton.button ~label:"Check"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let annotateb =
- GButton.button ~label:"Annotate"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let settingsb =
- GButton.button ~label:"Settings"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let button_export_to_postscript =
- GButton.button ~label:"export_to_postscript"
- ~packing:(hbox#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 nextb = nextb
- method prevb = prevb
- method label = label
- method output = (output : GMathView.math_view ref)
- method errors = errors
- method show () = window#show ()
- initializer
- nextb#misc#set_sensitive false ;
- prevb#misc#set_sensitive false ;
-
- (* signal handlers here *)
- 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
- (jump self) (choose_selection self) loaded_uri 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 ))
-end;;
-
-class theory_rendering_window rendering_window =
- let window =
- GWindow.window ~title:"MathML theory viewer" ~border_width:2 () in
- let vbox =
- GPack.vbox ~packing:window#add () in
- let label =
- GMisc.label ~text:"???"
- ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
- let paned =
- 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 output =
- ref (GMathView.math_view ~use_t1_lib:false ~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
- let errors = GEdit.text ~packing:scrolled_window#add_with_viewport () in
- let hbox =
- GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
- let prevb =
- GButton.button ~label:"Prev"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let nextb =
- GButton.button ~label:"Next"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let checkb =
- GButton.button ~label:"Check"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let settingsb =
- GButton.button ~label:"Settings"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let button_export_to_postscript =
- GButton.button ~label:"export_to_postscript"
- ~packing:(hbox#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 nextb = nextb
- method prevb = prevb
- method label = label
- method output = (output : GMathView.math_view ref)
- method errors = errors
- method show () = window#show ()
- initializer
- nextb#misc#set_sensitive false ;
- prevb#misc#set_sensitive false ;
-
- (* signal handlers here *)
- 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
- 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) ;
- ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
-end;;
-
-(* CSC: fare in modo che i due alberi vengano svuotati invece che distrutti *)
-class selection_window theory_rendering_window rendering_window =
- let label = "cic:/" in
- let theorylabel = "theory:/" in
- 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 hbox =
- GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
- let updateb =
- GButton.button ~label:"Update"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let quitb =
- GButton.button ~label:"Quit"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
-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
- theory_rendering_window rendering_window (ref sw1, ref sw, hbox1) mktree))
-end;;
-
-
-(* MAIN *)
-
-let _ =
- build_uri_tree () ;
- let output =
- ref (GMathView.math_view ~use_t1_lib:false ~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
- let theory_rendering_window = new theory_rendering_window rendering_window in
- let selection_window =
- new selection_window theory_rendering_window rendering_window
- in
- selection_window#show () ;
- GMain.Main.main ()
-;;
projects / helm.git / blobdiff