1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
36 (* GLOBAL CONSTANTS *)
38 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
42 " <body bgColor=\"white\">"
50 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
52 let htmlheader_and_content = ref htmlheader;;
54 let filename4uwobo = "/public/sacerdot/prova.xml";;
56 let current_cic_infos = ref None;;
61 let domImpl = Gdome.domImplementation ();;
65 domImpl#createDocumentFromURI
67 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
69 ~uri:("styles/" ^ name) ()
71 Gdome_xslt.processStylesheet style
74 let d_c = parseStyle "drop_coercions.xsl";;
75 let tc1 = parseStyle "objtheorycontent.xsl";;
76 let hc2 = parseStyle "content_to_html.xsl";;
77 let l = parseStyle "link.xsl";;
79 let c1 = parseStyle "rootcontent.xsl";;
80 let g = parseStyle "genmmlid.xsl";;
81 let c2 = parseStyle "annotatedpres.xsl";;
84 let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";;
85 let getterURL = "http://phd.cs.unibo.it:8081/";;
87 let processorURL = "http://localhost:8080/helm/servelt/uwobo/";;
88 let getterURL = "http://localhost:8081/";;
90 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
92 ["processorURL", "'" ^ processorURL ^ "'" ;
93 "getterURL", "'" ^ getterURL ^ "'" ;
94 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
95 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
96 "UNICODEvsSYMBOL", "'symbol'" ;
97 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
98 "encoding", "'iso-8859-1'" ;
99 "media-type", "'text/html'" ;
100 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
101 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
102 "naturalLanguage", "'no'" ;
103 "annotations", "'no'" ;
104 "topurl", "'http://phd.cs.unibo.it/helm'" ;
105 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
108 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
110 ["processorURL", "'" ^ processorURL ^ "'" ;
111 "getterURL", "'" ^ getterURL ^ "'" ;
112 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
113 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
114 "UNICODEvsSYMBOL", "'symbol'" ;
115 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
116 "encoding", "'iso-8859-1'" ;
117 "media-type", "'text/html'" ;
118 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
119 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
120 "naturalLanguage", "'no'" ;
121 "annotations", "'no'" ;
122 "topurl", "'http://phd.cs.unibo.it/helm'" ;
123 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
126 let parse_file filename =
127 let inch = open_in filename in
128 let rec read_lines () =
130 let line = input_line inch in
138 let applyStylesheets input styles args =
139 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
143 let mml_of_cic acic =
144 prerr_endline "BBB CREAZIONE" ;
146 Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") acic
148 Xml.pp ~quiet:true xml (Some filename4uwobo) ;
149 prerr_endline "BBB PARSING" ;
150 let input = domImpl#createDocumentFromURI ~uri:filename4uwobo () in
151 prerr_endline "BBB STYLESHEETS" ;
152 let output = applyStylesheets input mml_styles mml_args in
153 prerr_endline "BBB RESA" ;
154 ignore(domImpl#saveDocumentToFile ~doc:output ~name:"/tmp/xxxyyyzzz" ()) ;
161 let exact rendering_window () =
162 let inputt = (rendering_window#inputt : GEdit.text) in
163 (*CSC: Gran cut&paste da sotto... *)
164 let inputlen = inputt#length in
165 let input = inputt#get_chars 0 inputlen ^ "\n" in
166 let lexbuf = Lexing.from_string input in
169 (* Execute the actions *)
170 match CicTextualParser.main CicTextualLexer.token lexbuf with
174 (*??? Ma servira' da qualche parte!
175 let ty = CicTypeChecker.type_of_aux' [] expr in
177 let (acic, ids_to_terms, ids_to_father_ids) =
178 Cic2acic.acic_of_cic expr
180 (*CSC: chiamare la vera tattica exact qui! *)
184 print_endline ("? " ^ CicPp.ppterm expr) ;
188 CicTextualParser0.Eof ->
189 inputt#delete_text 0 inputlen
190 (*CSC: fare qualcosa di utile *)
192 print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
195 let proveit rendering_window () =
196 let module G = Gdome in
197 match rendering_window#output#get_selection with
200 ((node : Gdome.element)#getAttributeNS
202 ((element : G.element)#getAttributeNS
205 ~localName:(G.domString "xref"))#to_string
207 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
210 match !current_cic_infos with
211 Some (ids_to_terms, ids_to_father_ids) ->
214 LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids
216 SequentPp.TextualPp.print_sequent sequent ;
217 let sequent_gdome = SequentPp.XmlPp.print_sequent sequent in
219 Xml2Gdome.document_of_xml domImpl sequent_gdome
222 applyStylesheets sequent_doc sequent_styles sequent_args
224 rendering_window#proofw#load_tree ~dom:sequent_mml ;
225 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
226 ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
227 ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
228 ~name:"/public/sacerdot/guruguru2" ~indent:true ())
229 | None -> assert false (* "ERROR: No current term!!!" *)
231 | None -> assert false (* "ERROR: No selection!!!" *)
234 let output_html outputhtml msg =
235 htmlheader_and_content := !htmlheader_and_content ^ msg ;
236 outputhtml#source (!htmlheader_and_content ^ htmlfooter)
239 let execute rendering_window () =
240 let inputt = (rendering_window#inputt : GEdit.text) in
241 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
242 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
243 let output = (rendering_window#output : GMathView.math_view) in
244 let proofw = (rendering_window#proofw : GMathView.math_view) in
245 let inputlen = inputt#length in
246 let input = inputt#get_chars 0 inputlen ^ "\n" in
247 (* Do something interesting *)
248 let lexbuf = Lexing.from_string input in
251 (* Execute the actions *)
252 match CicTextualParser.main CicTextualLexer.token lexbuf with
256 let ty = CicTypeChecker.type_of_aux' [] expr in
257 let whd = CicReduction.whd expr in
259 let (acic, ids_to_terms, ids_to_father_ids) =
260 Cic2acic.acic_of_cic expr
262 let mml = mml_of_cic acic in
263 output#load_tree mml ;
264 prerr_endline "BBB FINE RESA" ;
265 current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ;
266 print_endline ("? " ^ CicPp.ppterm expr) ;
267 print_endline (">> " ^ CicPp.ppterm whd) ;
268 print_endline (": " ^ CicPp.ppterm ty) ;
272 print_endline ("? " ^ CicPp.ppterm expr) ;
276 CicTextualParser0.Eof ->
277 inputt#delete_text 0 inputlen ;
278 ignore(oldinputt#insert_text input oldinputt#length) ;
280 print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
284 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
286 let module G = Gdome in
287 let rec aux element =
288 if element#hasAttributeNS
290 ~localName:(G.domString "xref")
292 mmlwidget#set_selection (Some element)
294 match element#get_parentNode with
296 (*CSC: OCAML DIVERGES!
297 | Some p -> aux (new G.element_of_node p)
299 | Some p -> aux (new Gdome.element_of_node p)
303 | None -> mmlwidget#set_selection None
306 (* STUFF TO BUILD THE GTK INTERFACE *)
308 (* Stuff for the widget settings *)
310 let export_to_postscript (output : GMathView.math_view) () =
311 output#export_to_postscript ~filename:"output.ps" ();
314 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
315 button_set_kerning button_set_transparency button_export_to_postscript
318 let is_set = button_t1#active in
319 output#set_font_manager_type
320 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
323 button_set_anti_aliasing#misc#set_sensitive true ;
324 button_set_kerning#misc#set_sensitive true ;
325 button_set_transparency#misc#set_sensitive true ;
326 button_export_to_postscript#misc#set_sensitive true ;
330 button_set_anti_aliasing#misc#set_sensitive false ;
331 button_set_kerning#misc#set_sensitive false ;
332 button_set_transparency#misc#set_sensitive false ;
333 button_export_to_postscript#misc#set_sensitive false ;
337 let set_anti_aliasing output button_set_anti_aliasing () =
338 output#set_anti_aliasing button_set_anti_aliasing#active
341 let set_kerning output button_set_kerning () =
342 output#set_kerning button_set_kerning#active
345 let set_transparency output button_set_transparency () =
346 output#set_transparency button_set_transparency#active
349 let changefont output font_size_spinb () =
350 output#set_font_size font_size_spinb#value_as_int
353 let set_log_verbosity output log_verbosity_spinb () =
354 output#set_log_verbosity log_verbosity_spinb#value_as_int
357 class settings_window (output : GMathView.math_view) sw
358 button_export_to_postscript selection_changed_callback
360 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
362 GPack.vbox ~packing:settings_window#add () in
365 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
366 ~border_width:5 ~packing:vbox#add () in
368 GButton.toggle_button ~label:"activate t1 fonts"
369 ~packing:(table#attach ~left:0 ~top:0) () in
370 let button_set_anti_aliasing =
371 GButton.toggle_button ~label:"set_anti_aliasing"
372 ~packing:(table#attach ~left:0 ~top:1) () in
373 let button_set_kerning =
374 GButton.toggle_button ~label:"set_kerning"
375 ~packing:(table#attach ~left:1 ~top:1) () in
376 let button_set_transparency =
377 GButton.toggle_button ~label:"set_transparency"
378 ~packing:(table#attach ~left:2 ~top:1) () in
381 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
382 ~border_width:5 ~packing:vbox#add () in
383 let font_size_label =
384 GMisc.label ~text:"font size:"
385 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
386 let font_size_spinb =
388 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
391 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
392 let log_verbosity_label =
393 GMisc.label ~text:"log verbosity:"
394 ~packing:(table#attach ~left:0 ~top:1) () in
395 let log_verbosity_spinb =
397 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
400 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
402 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
404 GButton.button ~label:"Close"
405 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
407 method show = settings_window#show
409 button_set_anti_aliasing#misc#set_sensitive false ;
410 button_set_kerning#misc#set_sensitive false ;
411 button_set_transparency#misc#set_sensitive false ;
412 (* Signals connection *)
413 ignore(button_t1#connect#clicked
414 (activate_t1 output button_set_anti_aliasing button_set_kerning
415 button_set_transparency button_export_to_postscript button_t1)) ;
416 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
417 ignore(button_set_anti_aliasing#connect#toggled
418 (set_anti_aliasing output button_set_anti_aliasing));
419 ignore(button_set_kerning#connect#toggled
420 (set_kerning output button_set_kerning)) ;
421 ignore(button_set_transparency#connect#toggled
422 (set_transparency output button_set_transparency)) ;
423 ignore(log_verbosity_spinb#connect#changed
424 (set_log_verbosity output log_verbosity_spinb)) ;
425 ignore(closeb#connect#clicked settings_window#misc#hide)
430 class rendering_window output proofw (label : GMisc.label) =
432 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
434 GPack.hbox ~packing:window#add () in
436 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
437 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
438 let scrolled_window0 =
439 GBin.scrolled_window ~border_width:10
440 ~packing:(vbox#pack ~expand:true ~padding:5) () in
441 let _ = scrolled_window0#add output#coerce in
443 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
445 GButton.button ~label:"Settings"
446 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
447 let button_export_to_postscript =
448 GButton.button ~label:"export_to_postscript"
449 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
451 GButton.button ~label:"Close"
452 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
454 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
456 GButton.button ~label:"Prove It"
457 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
458 let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
459 ~packing:(vbox#pack ~padding:5) () in
461 GButton.button ~label:"Execute"
462 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
463 let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
464 ~packing:(vbox#pack ~padding:5) () in
466 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
467 let scrolled_window1 =
468 GBin.scrolled_window ~border_width:10
469 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
470 let _ = scrolled_window1#add proofw#coerce in
472 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
474 GButton.button ~label:"Exact"
475 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
478 ~source:"<html><body bgColor=\"white\"></body></html>"
479 ~width:400 ~height: 200
480 ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
483 method outputhtml = outputhtml
484 method oldinputt = oldinputt
485 method inputt = inputt
486 method output = (output : GMathView.math_view)
487 method proofw = (proofw : GMathView.math_view)
488 method show () = window#show ()
490 button_export_to_postscript#misc#set_sensitive false ;
492 (* signal handlers here *)
493 ignore(output#connect#selection_changed
494 (function elem -> proofw#unload ; choose_selection output elem)) ;
495 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
496 ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
497 let settings_window = new settings_window output scrolled_window0
498 button_export_to_postscript (choose_selection output) in
499 ignore(settingsb#connect#clicked settings_window#show) ;
500 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
501 ignore(proveitb#connect#clicked (proveit self)) ;
502 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
503 ignore(executeb#connect#clicked (execute self)) ;
504 ignore(exactb#connect#clicked (exact self)) ;
505 Logger.log_callback :=
506 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
511 let initialize_everything () =
512 let module U = Unix in
513 let output = GMathView.math_view ~width:400 ~height:280 ()
514 and proofw = GMathView.math_view ~width:400 ~height:275 ()
515 and label = GMisc.label ~text:"gTopLevel" () in
516 let rendering_window =
517 new rendering_window output proofw label
519 rendering_window#show () ;
525 initialize_everything ()