+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(* GLOBAL CONSTANTS *)
+
+let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
+
+let htmlheader =
+ "<html>" ^
+ " <body bgColor=\"white\">"
+;;
+
+let htmlfooter =
+ " </body>" ^
+ "</html>"
+;;
+
+(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
+
+let htmlheader_and_content = ref htmlheader;;
+
+let filename4uwobo = "/public/sacerdot/prova.xml";;
+
+let current_cic_infos = ref None;;
+
+
+(* MISC FUNCTIONS *)
+
+let domImpl = Gdome.domImplementation ();;
+
+let parseStyle name =
+ let style =
+ domImpl#createDocumentFromURI
+(*
+ ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
+*)
+ ~uri:("styles/" ^ name) ()
+ in
+ Gdome_xslt.processStylesheet style
+;;
+
+let d_c = parseStyle "drop_coercions.xsl";;
+let tc1 = parseStyle "objtheorycontent.xsl";;
+let hc2 = parseStyle "content_to_html.xsl";;
+let l = parseStyle "link.xsl";;
+
+let c1 = parseStyle "rootcontent.xsl";;
+let g = parseStyle "genmmlid.xsl";;
+let c2 = parseStyle "annotatedpres.xsl";;
+
+(*
+let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";;
+let getterURL = "http://phd.cs.unibo.it:8081/";;
+*)
+let processorURL = "http://localhost:8080/helm/servelt/uwobo/";;
+let getterURL = "http://localhost:8081/";;
+
+let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
+let mml_args =
+ ["processorURL", "'" ^ processorURL ^ "'" ;
+ "getterURL", "'" ^ getterURL ^ "'" ;
+ "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
+ "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
+ "UNICODEvsSYMBOL", "'symbol'" ;
+ "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
+ "encoding", "'iso-8859-1'" ;
+ "media-type", "'text/html'" ;
+ "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
+ "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
+ "naturalLanguage", "'no'" ;
+ "annotations", "'no'" ;
+ "topurl", "'http://phd.cs.unibo.it/helm'" ;
+ "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
+;;
+
+let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
+let sequent_args =
+ ["processorURL", "'" ^ processorURL ^ "'" ;
+ "getterURL", "'" ^ getterURL ^ "'" ;
+ "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
+ "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
+ "UNICODEvsSYMBOL", "'symbol'" ;
+ "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
+ "encoding", "'iso-8859-1'" ;
+ "media-type", "'text/html'" ;
+ "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
+ "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
+ "naturalLanguage", "'no'" ;
+ "annotations", "'no'" ;
+ "topurl", "'http://phd.cs.unibo.it/helm'" ;
+ "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
+;;
+
+let parse_file filename =
+ let inch = open_in filename in
+ let rec read_lines () =
+ try
+ let line = input_line inch in
+ line ^ read_lines ()
+ with
+ End_of_file -> ""
+ in
+ read_lines ()
+;;
+
+let applyStylesheets input styles args =
+ List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
+ input styles
+;;
+
+let mml_of_cic acic =
+prerr_endline "BBB CREAZIONE" ;
+ let xml =
+ Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") acic
+ in
+ Xml.pp ~quiet:true xml (Some filename4uwobo) ;
+prerr_endline "BBB PARSING" ;
+ let input = domImpl#createDocumentFromURI ~uri:filename4uwobo () in
+prerr_endline "BBB STYLESHEETS" ;
+ let output = applyStylesheets input mml_styles mml_args in
+prerr_endline "BBB RESA" ;
+ignore(domImpl#saveDocumentToFile ~doc:output ~name:"/tmp/xxxyyyzzz" ()) ;
+ output
+;;
+
+
+(* CALLBACKS *)
+
+let exact rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+(*CSC: Gran cut&paste da sotto... *)
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ let lexbuf = Lexing.from_string input in
+ try
+ while true do
+ (* Execute the actions *)
+ match CicTextualParser.main CicTextualLexer.token lexbuf with
+ None -> ()
+ | Some expr ->
+ try
+(*??? Ma servira' da qualche parte!
+ let ty = CicTypeChecker.type_of_aux' [] expr in
+*)
+ let (acic, ids_to_terms, ids_to_father_ids) =
+ Cic2acic.acic_of_cic expr
+ in
+(*CSC: chiamare la vera tattica exact qui! *)
+ ()
+ with
+ e ->
+ print_endline ("? " ^ CicPp.ppterm expr) ;
+ raise e
+ done
+ with
+ CicTextualParser0.Eof ->
+ inputt#delete_text 0 inputlen
+(*CSC: fare qualcosa di utile *)
+ | e ->
+ print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+;;
+
+let proveit rendering_window () =
+ let module G = Gdome in
+ match rendering_window#output#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ (*CSC: OCAML DIVERGE
+ ((element : G.element)#getAttributeNS
+ *)
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ match !current_cic_infos with
+ Some (ids_to_terms, ids_to_father_ids) ->
+ let id = xpath in
+ let sequent =
+ LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids
+ in
+ SequentPp.TextualPp.print_sequent sequent ;
+ let sequent_gdome = SequentPp.XmlPp.print_sequent sequent in
+ let sequent_doc =
+ Xml2Gdome.document_of_xml domImpl sequent_gdome
+ in
+ let sequent_mml =
+ applyStylesheets sequent_doc sequent_styles sequent_args
+ in
+ rendering_window#proofw#load_tree ~dom:sequent_mml ;
+ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
+ ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
+ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
+ ~name:"/public/sacerdot/guruguru2" ~indent:true ())
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ end
+ | None -> assert false (* "ERROR: No selection!!!" *)
+;;
+
+let output_html outputhtml msg =
+ htmlheader_and_content := !htmlheader_and_content ^ msg ;
+ outputhtml#source (!htmlheader_and_content ^ htmlfooter)
+;;
+
+let execute rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let oldinputt = (rendering_window#oldinputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let proofw = (rendering_window#proofw : GMathView.math_view) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ (* Do something interesting *)
+ let lexbuf = Lexing.from_string input in
+ try
+ while true do
+ (* Execute the actions *)
+ match CicTextualParser.main CicTextualLexer.token lexbuf with
+ None -> ()
+ | Some expr ->
+ try
+ let ty = CicTypeChecker.type_of_aux' [] expr in
+ let whd = CicReduction.whd expr in
+
+ let (acic, ids_to_terms, ids_to_father_ids) =
+ Cic2acic.acic_of_cic expr
+ in
+ let mml = mml_of_cic acic in
+ output#load_tree mml ;
+prerr_endline "BBB FINE RESA" ;
+ current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ;
+print_endline ("? " ^ CicPp.ppterm expr) ;
+print_endline (">> " ^ CicPp.ppterm whd) ;
+print_endline (": " ^ CicPp.ppterm ty) ;
+flush stdout ;
+ with
+ e ->
+ print_endline ("? " ^ CicPp.ppterm expr) ;
+ raise e
+ done
+ with
+ CicTextualParser0.Eof ->
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length) ;
+ | e ->
+ print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+;;
+
+let choose_selection
+ (mmlwidget : GMathView.math_view) (element : Gdome.element option)
+=
+ let module G = Gdome in
+ let rec aux element =
+ if element#hasAttributeNS
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref")
+ then
+ mmlwidget#set_selection (Some element)
+ else
+ match element#get_parentNode with
+ None -> assert false
+ (*CSC: OCAML DIVERGES!
+ | Some p -> aux (new G.element_of_node p)
+ *)
+ | Some p -> aux (new Gdome.element_of_node p)
+ in
+ match element with
+ Some x -> aux x
+ | None -> mmlwidget#set_selection None
+;;
+
+(* STUFF TO BUILD THE GTK INTERFACE *)
+
+(* Stuff for the widget settings *)
+
+let export_to_postscript (output : GMathView.math_view) () =
+ output#export_to_postscript ~filename:"output.ps" ();
+;;
+
+let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
+ button_set_kerning button_set_transparency 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_set_transparency#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_set_transparency#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 set_transparency output button_set_transparency () =
+ output#set_transparency button_set_transparency#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 : GMathView.math_view) sw
+ button_export_to_postscript 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:0 ~top:1) () in
+ let button_set_kerning =
+ GButton.toggle_button ~label:"set_kerning"
+ ~packing:(table#attach ~left:1 ~top:1) () in
+ let button_set_transparency =
+ GButton.toggle_button ~label:"set_transparency"
+ ~packing:(table#attach ~left:2 ~top:1) () 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 ;
+ button_set_transparency#misc#set_sensitive false ;
+ (* Signals connection *)
+ ignore(button_t1#connect#clicked
+ (activate_t1 output button_set_anti_aliasing button_set_kerning
+ button_set_transparency 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(button_set_transparency#connect#toggled
+ (set_transparency output button_set_transparency)) ;
+ 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 rendering_window output proofw (label : GMisc.label) =
+ let window =
+ GWindow.window ~title:"MathML viewer" ~border_width:2 () in
+ let hbox0 =
+ GPack.hbox ~packing:window#add () in
+ let vbox =
+ GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
+ let scrolled_window0 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox#pack ~expand:true ~padding:5) () in
+ let _ = scrolled_window0#add output#coerce in
+ let hbox1 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let settingsb =
+ GButton.button ~label:"Settings"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let button_export_to_postscript =
+ GButton.button ~label:"export_to_postscript"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let closeb =
+ GButton.button ~label:"Close"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox2 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let proveitb =
+ GButton.button ~label:"Prove It"
+ ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
+ let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
+ ~packing:(vbox#pack ~padding:5) () in
+ let executeb =
+ GButton.button ~label:"Execute"
+ ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
+ ~packing:(vbox#pack ~padding:5) () in
+ let vbox1 =
+ GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window1 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox1#pack ~expand:true ~padding:5) () in
+ let _ = scrolled_window1#add proofw#coerce in
+ let hbox3 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let exactb =
+ GButton.button ~label:"Exact"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let outputhtml =
+ GHtml.xmhtml
+ ~source:"<html><body bgColor=\"white\"></body></html>"
+ ~width:400 ~height: 200
+ ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
+ ~show:true () in
+object(self)
+ method outputhtml = outputhtml
+ method oldinputt = oldinputt
+ method inputt = inputt
+ method output = (output : GMathView.math_view)
+ method proofw = (proofw : GMathView.math_view)
+ method show () = window#show ()
+ initializer
+ button_export_to_postscript#misc#set_sensitive false ;
+
+ (* signal handlers here *)
+ ignore(output#connect#selection_changed
+ (function elem -> proofw#unload ; choose_selection output elem)) ;
+ ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+ ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
+ let settings_window = new settings_window output scrolled_window0
+ button_export_to_postscript (choose_selection output) in
+ ignore(settingsb#connect#clicked settings_window#show) ;
+ ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
+ ignore(proveitb#connect#clicked (proveit self)) ;
+ ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
+ ignore(executeb#connect#clicked (execute self)) ;
+ ignore(exactb#connect#clicked (exact self)) ;
+ Logger.log_callback :=
+ (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
+end;;
+
+(* MAIN *)
+
+let initialize_everything () =
+ let module U = Unix in
+ let output = GMathView.math_view ~width:400 ~height:280 ()
+ and proofw = GMathView.math_view ~width:400 ~height:275 ()
+ and label = GMisc.label ~text:"gTopLevel" () in
+ let rendering_window =
+ new rendering_window output proofw label
+ in
+ rendering_window#show () ;
+ GMain.Main.main ()
+;;
+
+let _ =
+ CicCooking.init () ;
+ initialize_everything ()
+;;