+
+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'
+;;
+
+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
+
+ 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
+
+ ignore(tree_item#connect#select (selection_changed rendering_window None)) ;
+ 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 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
+;;
+