X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;fp=helm%2Finterface%2Fmmlinterface.ml;h=0000000000000000000000000000000000000000;hb=fa11ed6dc134f8ad3421c37a97271018e075bbed;hp=784c9f4b127e47a21089047296af4dc079675dfa;hpb=c03d2c1fdab8d228cb88aaba5ca0f556318bebc5;p=helm.git diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml deleted file mode 100755 index 784c9f4b1..000000000 --- a/helm/interface/mmlinterface.ml +++ /dev/null @@ -1,774 +0,0 @@ -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 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 () -;;