- 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 ~first_time 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 ~first_time:false parent
- | Some s ->
- if not first_time then
- !(rendering_window#output)#set_selection (Some node)
- in
- match node with
- None -> () (* No element selected *)
- | Some node -> aux ~first_time:true 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