--- /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 []
+
+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
+ 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
+ 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 s =
+ 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 changefont rendering_window () =
+ rendering_window#output#set_font_size rendering_window#spinb#value_as_int
+;;
+
+
+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 xpath = (rendering_window#output#get_selection : string option) in
+ match xpath with
+ None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
+ | Some xpath ->
+ 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
+ ) !content
+ | _ -> ()
+ in
+ aux
+;;
+
+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)
+ 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) ;
+ output#load (parse_no_cache new_current_uri)
+ )) ;
+ 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 ~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 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:(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 spinb = spinb
+ method output = (output : GMathView.math_view)
+ 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(nextb#connect#clicked (next self)) ;
+ ignore(prevb#connect#clicked (prev self)) ;
+ ignore(checkb#connect#clicked (check self)) ;
+ ignore(spinb#connect#changed (changefont self)) ;
+ ignore(closeb#connect#clicked window#misc#hide) ;
+ ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
+ 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 ~padding:5) () in
+ let scrolled_window0 =
+ GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
+ let output =
+ 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
+ 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 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:(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)
+ method errors = errors
+ method spinb = spinb
+ 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(nextb#connect#clicked (theory_next self)) ;
+ ignore(prevb#connect#clicked (theory_prev self)) ;
+ ignore(checkb#connect#clicked (theory_check self)) ;
+ ignore(spinb#connect#changed (changefont self)) ;
+ 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 = 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
+ 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