(******************************************************************************)
(*                                                                            *)
(*                               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;;

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 (node : Ominidom.o_mDOMNode) =
 let module O = Ominidom in
  match (node#get_attribute (O.o_mDOMString_of_string "href")) with
    Some str ->
     let s = str#get_string 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
  | None -> assert false
;;

let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
 let module O = Ominidom in
  let rec aux node =
   match node#get_attribute (O.o_mDOMString_of_string "xref") with
     Some _ -> rendering_window#output#set_selection (Some node)
   | None   -> aux (node#get_parent)
  in
   match node with
     Some x -> aux x
   | None   -> rendering_window#output#set_selection None
;;


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
;;

let annotateb_pressed rendering_window annotation_window () =
 let module O = Ominidom in
 match rendering_window#output#get_selection with
 | Some node ->
  begin
   match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
   | Some xpath ->
     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#get_string) ;
      CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
      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 () ;
   | None ->
       (* next "cast" can't got rid of, but I don't know why *)
       let errors = (rendering_window#errors : GEdit.text) in
        errors#insert ("\nNo xref found\n")
  end
 | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\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 -> assert false
  | 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 ;
        let expand_sons =
         List.map
          (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)) ;
               (* Almost lazy function *)
               (fun () -> aux treeitem2 ti)
          ) (List.sort compare !content)
        in
         let lazy_expand_sons = lazy (List.iter (fun f -> f ()) expand_sons) in
         ignore(treeitem#connect#expand
          (fun () -> Lazy.force lazy_expand_sons)) ;
   | _ -> ()
 in
  aux 
;;

(* Stuff for the widget settings *)

let export_to_postscript (output : GMathView.math_view) () =
 output#export_to_postscript ~filename:"output.ps" ();
;;

let activate_t1 output button_set_anti_aliasing button_set_kerning 
 button_export_to_postscript button_t1 ()
=
 let is_set = button_t1#active in
  output#set_font_manager_type
   (if is_set then `font_manager_t1 else `font_manager_gtk) ;
  if is_set then
   begin
    button_set_anti_aliasing#misc#set_sensitive true ;
    button_set_kerning#misc#set_sensitive true ;
    button_export_to_postscript#misc#set_sensitive true ;
   end
  else
   begin
    button_set_anti_aliasing#misc#set_sensitive false ;
    button_set_kerning#misc#set_sensitive false ;
    button_export_to_postscript#misc#set_sensitive false ;
   end
;;

let set_anti_aliasing output button_set_anti_aliasing () =
 output#set_anti_aliasing button_set_anti_aliasing#active
;;

let set_kerning output button_set_kerning () =
 output#set_kerning button_set_kerning#active
;;

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 button_export_to_postscript jump_callback
 selection_changed_callback
=
 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
 let vbox =
  GPack.vbox ~packing:settings_window#add () in
 let table =
  GPack.table
   ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
   ~border_width:5 ~packing:vbox#add () in
 let button_t1 =
  GButton.toggle_button ~label:"activate t1 fonts"
   ~packing:(table#attach ~left:0 ~top:0) () in
 let button_set_anti_aliasing =
  GButton.toggle_button ~label:"set_anti_aliasing"
   ~packing:(table#attach ~left:1 ~top:0) () in
 let button_set_kerning =
  GButton.toggle_button ~label:"set_kerning"
   ~packing:(table#attach ~left:2 ~top:0) () in
 let table =
  GPack.table
   ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
   ~border_width:5 ~packing:vbox#add () in
 let font_size_label =
  GMisc.label ~text:"font size:"
   ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () 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:1 ~top:0 ~fill:`NONE) () in
 let log_verbosity_label =
  GMisc.label ~text:"log verbosity:"
   ~packing:(table#attach ~left:0 ~top:1) () 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:1 ~top:1) () in
 let hbox =
  GPack.hbox ~packing:(vbox#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 show = settings_window#show
 initializer
  button_set_anti_aliasing#misc#set_sensitive false ;
  button_set_kerning#misc#set_sensitive false ;
  (* Signals connection *)
  ignore(button_t1#connect#clicked
   (activate_t1 output button_set_anti_aliasing button_set_kerning
    button_export_to_postscript button_t1)) ;
  ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
  ignore(button_set_anti_aliasing#connect#toggled
   (set_anti_aliasing output button_set_anti_aliasing));
  ignore(button_set_kerning#connect#toggled
   (set_kerning output button_set_kerning)) ;
  ignore(log_verbosity_spinb#connect#changed
   (set_log_verbosity output log_verbosity_spinb)) ;
  ignore(closeb#connect#clicked settings_window#misc#hide)
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)
 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
        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)
 method errors = errors
 method show () = window#show ()
 initializer
  nextb#misc#set_sensitive false ;
  prevb#misc#set_sensitive false ;
  button_export_to_postscript#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
   button_export_to_postscript (jump self) (choose_selection self) 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 =
  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 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)
 method errors = errors
 method show () = window#show ()
 initializer
  nextb#misc#set_sensitive false ;
  prevb#misc#set_sensitive false ;
  button_export_to_postscript#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
   button_export_to_postscript (jump rendering_window)(choose_selection self) 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,sw) =
   create_gtk_trees hbox1 rendering_window theory_rendering_window mktree
  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
    (* signal handlers here *)
    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 ()
;;