1 (* Copyright (C) 2000-2002, 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 let prooffile = "/home/galata/miohelm/currentproof";;
51 (*CSC: the getter should handle the innertypes, not the FS *)
52 let innertypesfile = "/home/galata/miohelm/innertypes";;
54 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
56 let htmlheader_and_content = ref htmlheader;;
58 let current_cic_infos = ref None;;
59 let current_goal_infos = ref None;;
60 let current_scratch_infos = ref None;;
62 (* COMMAND LINE OPTIONS *)
68 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
71 Arg.parse argspec ignore ""
76 let domImpl = Gdome.domImplementation ();;
80 domImpl#createDocumentFromURI
82 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
84 ~uri:("styles/" ^ name) ()
86 Gdome_xslt.processStylesheet style
89 let d_c = parseStyle "drop_coercions.xsl";;
90 let tc1 = parseStyle "objtheorycontent.xsl";;
91 let hc2 = parseStyle "content_to_html.xsl";;
92 let l = parseStyle "link.xsl";;
94 let c1 = parseStyle "rootcontent.xsl";;
95 let g = parseStyle "genmmlid.xsl";;
96 let c2 = parseStyle "annotatedpres.xsl";;
99 let getterURL = Configuration.getter_url;;
100 let processorURL = Configuration.processor_url;;
102 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
104 ["processorURL", "'" ^ processorURL ^ "'" ;
105 "getterURL", "'" ^ getterURL ^ "'" ;
106 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
107 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
108 "UNICODEvsSYMBOL", "'symbol'" ;
109 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
110 "encoding", "'iso-8859-1'" ;
111 "media-type", "'text/html'" ;
112 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
113 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
114 "naturalLanguage", "'yes'" ;
115 "annotations", "'no'" ;
116 "explodeall", "'true()'" ;
117 "topurl", "'http://phd.cs.unibo.it/helm'" ;
118 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
121 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
123 ["processorURL", "'" ^ processorURL ^ "'" ;
124 "getterURL", "'" ^ getterURL ^ "'" ;
125 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
126 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
127 "UNICODEvsSYMBOL", "'symbol'" ;
128 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
129 "encoding", "'iso-8859-1'" ;
130 "media-type", "'text/html'" ;
131 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
132 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
133 "naturalLanguage", "'no'" ;
134 "annotations", "'no'" ;
135 "explodeall", "'true()'" ;
136 "topurl", "'http://phd.cs.unibo.it/helm'" ;
137 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
140 let parse_file filename =
141 let inch = open_in filename in
142 let rec read_lines () =
144 let line = input_line inch in
152 let applyStylesheets input styles args =
153 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
157 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
159 Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
162 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
165 let input = Xml2Gdome.document_of_xml domImpl xml in
166 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
167 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
169 Xml.pp xmlinnertypes (Some innertypesfile) ;
170 let output = applyStylesheets input mml_styles mml_args in
177 exception RefreshSequentException of exn;;
178 exception RefreshProofException of exn;;
180 let refresh_proof (output : GMathView.math_view) =
182 let uri,currentproof =
183 match !ProofEngine.proof with
185 | Some (uri,metasenv,bo,ty) ->
186 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
189 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
190 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
192 Cic2acic.acic_object_of_cic_object currentproof
195 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
197 output#load_tree mml ;
199 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
202 match !ProofEngine.proof with
204 | Some (uri,metasenv,bo,ty) ->
205 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ;
206 raise (RefreshProofException e)
209 let refresh_sequent (proofw : GMathView.math_view) =
211 match !ProofEngine.goal with
212 None -> proofw#unload
215 match !ProofEngine.proof with
217 | Some (_,metasenv,_,_) -> metasenv
219 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
220 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
221 SequentPp.XmlPp.print_sequent metasenv currentsequent
224 Xml2Gdome.document_of_xml domImpl sequent_gdome
227 applyStylesheets sequent_doc sequent_styles sequent_args
229 proofw#load_tree ~dom:sequent_mml ;
230 current_goal_infos :=
231 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
235 match !ProofEngine.goal with
240 match !ProofEngine.proof with
242 | Some (_,metasenv,_,_) -> metasenv
244 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
245 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
246 raise (RefreshSequentException e)
250 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
251 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
254 let mml_of_cic_term metano term =
256 match !ProofEngine.proof with
258 | Some (_,metasenv,_,_) -> metasenv
261 match !ProofEngine.goal with
264 let (_,canonical_context,_) =
265 List.find (function (m,_,_) -> m=metano) metasenv
269 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
270 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
273 Xml2Gdome.document_of_xml domImpl sequent_gdome
276 applyStylesheets sequent_doc sequent_styles sequent_args ;
278 current_scratch_infos :=
279 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
283 let output_html outputhtml msg =
284 htmlheader_and_content := !htmlheader_and_content ^ msg ;
285 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
286 outputhtml#set_topline (-1)
289 (***********************)
291 (***********************)
293 let call_tactic tactic rendering_window () =
294 let proofw = (rendering_window#proofw : GMathView.math_view) in
295 let output = (rendering_window#output : GMathView.math_view) in
296 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
297 let savedproof = !ProofEngine.proof in
298 let savedgoal = !ProofEngine.goal in
302 refresh_sequent proofw ;
305 RefreshSequentException e ->
306 output_html outputhtml
307 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
308 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
309 ProofEngine.proof := savedproof ;
310 ProofEngine.goal := savedgoal ;
311 refresh_sequent proofw
312 | RefreshProofException e ->
313 output_html outputhtml
314 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
315 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
316 ProofEngine.proof := savedproof ;
317 ProofEngine.goal := savedgoal ;
318 refresh_sequent proofw ;
321 output_html outputhtml
322 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
323 ProofEngine.proof := savedproof ;
324 ProofEngine.goal := savedgoal ;
328 let call_tactic_with_input tactic rendering_window () =
329 let proofw = (rendering_window#proofw : GMathView.math_view) in
330 let output = (rendering_window#output : GMathView.math_view) in
331 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
332 let inputt = (rendering_window#inputt : GEdit.text) in
333 let savedproof = !ProofEngine.proof in
334 let savedgoal = !ProofEngine.goal in
335 (*CSC: Gran cut&paste da sotto... *)
336 let inputlen = inputt#length in
337 let input = inputt#get_chars 0 inputlen ^ "\n" in
338 let lexbuf = Lexing.from_string input in
340 match !ProofEngine.proof with
342 | Some (curi,_,_,_) -> curi
344 let uri,metasenv,bo,ty =
345 match !ProofEngine.proof with
347 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
354 (match !ProofEngine.goal with
357 let (_,canonical_context,_) =
358 List.find (function (m,_,_) -> m=metano) metasenv
366 CicTextualParserContext.main
367 curi context metasenv CicTextualLexer.token lexbuf
370 | Some (metasenv',expr) ->
371 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
373 refresh_sequent proofw ;
377 CicTextualParser0.Eof ->
378 inputt#delete_text 0 inputlen
379 | RefreshSequentException e ->
380 output_html outputhtml
381 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
382 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
383 ProofEngine.proof := savedproof ;
384 ProofEngine.goal := savedgoal ;
385 refresh_sequent proofw
386 | RefreshProofException e ->
387 output_html outputhtml
388 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
389 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
390 ProofEngine.proof := savedproof ;
391 ProofEngine.goal := savedgoal ;
392 refresh_sequent proofw ;
395 output_html outputhtml
396 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
397 ProofEngine.proof := savedproof ;
398 ProofEngine.goal := savedgoal ;
401 let call_tactic_with_goal_input tactic rendering_window () =
402 let module L = LogicalOperations in
403 let module G = Gdome in
404 let proofw = (rendering_window#proofw : GMathView.math_view) in
405 let output = (rendering_window#output : GMathView.math_view) in
406 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
407 let savedproof = !ProofEngine.proof in
408 let savedgoal = !ProofEngine.goal in
409 match proofw#get_selection with
412 ((node : Gdome.element)#getAttributeNS
414 ~localName:(G.domString "xref"))#to_string
416 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
420 match !current_goal_infos with
421 Some (ids_to_terms, ids_to_father_ids,_) ->
423 tactic (Hashtbl.find ids_to_terms id) ;
424 refresh_sequent rendering_window#proofw ;
425 refresh_proof rendering_window#output
426 | None -> assert false (* "ERROR: No current term!!!" *)
428 RefreshSequentException e ->
429 output_html outputhtml
430 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
431 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
432 ProofEngine.proof := savedproof ;
433 ProofEngine.goal := savedgoal ;
434 refresh_sequent proofw
435 | RefreshProofException e ->
436 output_html outputhtml
437 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
438 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
439 ProofEngine.proof := savedproof ;
440 ProofEngine.goal := savedgoal ;
441 refresh_sequent proofw ;
444 output_html outputhtml
445 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
446 ProofEngine.proof := savedproof ;
447 ProofEngine.goal := savedgoal ;
450 output_html outputhtml
451 ("<h1 color=\"red\">No term selected</h1>")
454 let call_tactic_with_input_and_goal_input tactic rendering_window () =
455 let module L = LogicalOperations in
456 let module G = Gdome in
457 let proofw = (rendering_window#proofw : GMathView.math_view) in
458 let output = (rendering_window#output : GMathView.math_view) in
459 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
460 let inputt = (rendering_window#inputt : GEdit.text) in
461 let savedproof = !ProofEngine.proof in
462 let savedgoal = !ProofEngine.goal in
463 match proofw#get_selection with
466 ((node : Gdome.element)#getAttributeNS
468 ~localName:(G.domString "xref"))#to_string
470 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
474 match !current_goal_infos with
475 Some (ids_to_terms, ids_to_father_ids,_) ->
477 (* Let's parse the input *)
478 let inputlen = inputt#length in
479 let input = inputt#get_chars 0 inputlen ^ "\n" in
480 let lexbuf = Lexing.from_string input in
482 match !ProofEngine.proof with
484 | Some (curi,_,_,_) -> curi
486 let uri,metasenv,bo,ty =
487 match !ProofEngine.proof with
489 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
496 (match !ProofEngine.goal with
499 let (_,canonical_context,_) =
500 List.find (function (m,_,_) -> m=metano) metasenv
509 CicTextualParserContext.main curi context metasenv
510 CicTextualLexer.token lexbuf
513 | Some (metasenv',expr) ->
514 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
515 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
517 refresh_sequent proofw ;
521 CicTextualParser0.Eof ->
522 inputt#delete_text 0 inputlen
524 | None -> assert false (* "ERROR: No current term!!!" *)
526 RefreshSequentException e ->
527 output_html outputhtml
528 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
529 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
530 ProofEngine.proof := savedproof ;
531 ProofEngine.goal := savedgoal ;
532 refresh_sequent proofw
533 | RefreshProofException e ->
534 output_html outputhtml
535 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
536 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
537 ProofEngine.proof := savedproof ;
538 ProofEngine.goal := savedgoal ;
539 refresh_sequent proofw ;
542 output_html outputhtml
543 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
544 ProofEngine.proof := savedproof ;
545 ProofEngine.goal := savedgoal ;
548 output_html outputhtml
549 ("<h1 color=\"red\">No term selected</h1>")
552 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
553 let module L = LogicalOperations in
554 let module G = Gdome in
555 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
556 let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
557 let savedproof = !ProofEngine.proof in
558 let savedgoal = !ProofEngine.goal in
559 match mmlwidget#get_selection with
562 ((node : Gdome.element)#getAttributeNS
564 ~localName:(G.domString "xref"))#to_string
566 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
570 match !current_scratch_infos with
571 (* term is the whole goal in the scratch_area *)
572 Some (term,ids_to_terms, ids_to_father_ids,_) ->
574 let expr = tactic term (Hashtbl.find ids_to_terms id) in
575 let mml = mml_of_cic_term 111 expr in
576 scratch_window#show () ;
577 scratch_window#mmlwidget#load_tree ~dom:mml
578 | None -> assert false (* "ERROR: No current term!!!" *)
581 output_html outputhtml
582 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
585 output_html outputhtml
586 ("<h1 color=\"red\">No term selected</h1>")
589 let call_tactic_with_hypothesis_input tactic rendering_window () =
590 let module L = LogicalOperations in
591 let module G = Gdome in
592 let proofw = (rendering_window#proofw : GMathView.math_view) in
593 let output = (rendering_window#output : GMathView.math_view) in
594 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
595 let savedproof = !ProofEngine.proof in
596 let savedgoal = !ProofEngine.goal in
597 match proofw#get_selection with
600 ((node : Gdome.element)#getAttributeNS
602 ~localName:(G.domString "xref"))#to_string
604 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
608 match !current_goal_infos with
609 Some (_,_,ids_to_hypotheses) ->
611 tactic (Hashtbl.find ids_to_hypotheses id) ;
612 refresh_sequent rendering_window#proofw ;
613 refresh_proof rendering_window#output
614 | None -> assert false (* "ERROR: No current term!!!" *)
616 RefreshSequentException e ->
617 output_html outputhtml
618 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
619 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
620 ProofEngine.proof := savedproof ;
621 ProofEngine.goal := savedgoal ;
622 refresh_sequent proofw
623 | RefreshProofException e ->
624 output_html outputhtml
625 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
626 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
627 ProofEngine.proof := savedproof ;
628 ProofEngine.goal := savedgoal ;
629 refresh_sequent proofw ;
632 output_html outputhtml
633 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
634 ProofEngine.proof := savedproof ;
635 ProofEngine.goal := savedgoal ;
638 output_html outputhtml
639 ("<h1 color=\"red\">No term selected</h1>")
643 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
644 let exact rendering_window =
645 call_tactic_with_input ProofEngine.exact rendering_window
647 let apply rendering_window =
648 call_tactic_with_input ProofEngine.apply rendering_window
650 let elimintrossimpl rendering_window =
651 call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window
653 let elimtype rendering_window =
654 call_tactic_with_input ProofEngine.elim_type rendering_window
656 let whd rendering_window =
657 call_tactic_with_goal_input ProofEngine.whd rendering_window
659 let reduce rendering_window =
660 call_tactic_with_goal_input ProofEngine.reduce rendering_window
662 let simpl rendering_window =
663 call_tactic_with_goal_input ProofEngine.simpl rendering_window
665 let fold rendering_window =
666 call_tactic_with_input ProofEngine.fold rendering_window
668 let cut rendering_window =
669 call_tactic_with_input ProofEngine.cut rendering_window
671 let change rendering_window =
672 call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
674 let letin rendering_window =
675 call_tactic_with_input ProofEngine.letin rendering_window
677 let ring rendering_window = call_tactic ProofEngine.ring rendering_window;;
678 let clearbody rendering_window =
679 call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window
681 let clear rendering_window =
682 call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
686 let whd_in_scratch scratch_window =
687 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
690 let reduce_in_scratch scratch_window =
691 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
694 let simpl_in_scratch scratch_window =
695 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
701 (**********************)
703 (**********************)
705 exception OpenConjecturesStillThere;;
706 exception WrongProof;;
708 let qed rendering_window () =
709 match !ProofEngine.proof with
711 | Some (uri,[],bo,ty) ->
713 CicReduction.are_convertible []
714 (CicTypeChecker.type_of_aux' [] [] bo) ty
717 (*CSC: Wrong: [] is just plainly wrong *)
718 let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
720 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
721 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
723 Cic2acic.acic_object_of_cic_object proof
726 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
728 (rendering_window#output : GMathView.math_view)#load_tree mml ;
731 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
736 | _ -> raise OpenConjecturesStillThere
740 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
742 let dtdname = "/projects/helm/V7/dtd/cic.dtd";;
744 let save rendering_window () =
745 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
746 match !ProofEngine.proof with
748 | Some (uri, metasenv, bo, ty) ->
750 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
752 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
753 Cic2acic.acic_object_of_cic_object currentproof
755 let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in
757 [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
759 ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
763 Xml.pp ~quiet:true xml' (Some prooffile) ;
764 output_html outputhtml
765 ("<h1 color=\"Green\">Current proof saved to " ^
769 (* Used to typecheck the loaded proofs *)
770 let typecheck_loaded_proof metasenv bo ty =
771 let module T = CicTypeChecker in
772 (*CSC: bisogna controllare anche il metasenv!!! *)
773 ignore (T.type_of_aux' metasenv [] ty) ;
774 ignore (T.type_of_aux' metasenv [] bo)
777 let load rendering_window () =
778 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
779 let output = (rendering_window#output : GMathView.math_view) in
780 let proofw = (rendering_window#proofw : GMathView.math_view) in
782 let uri = UriManager.uri_of_string "cic:/dummy.con" in
783 match CicParser.obj_of_xml prooffile uri with
784 Cic.CurrentProof (_,metasenv,bo,ty) ->
785 typecheck_loaded_proof metasenv bo ty ;
787 Some (uri, metasenv, bo, ty) ;
791 | (metano,_,_)::_ -> Some metano
793 refresh_proof output ;
794 refresh_sequent proofw ;
795 output_html outputhtml
796 ("<h1 color=\"Green\">Current proof loaded from " ^
800 RefreshSequentException e ->
801 output_html outputhtml
802 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
803 "sequent: " ^ Printexc.to_string e ^ "</h1>")
804 | RefreshProofException e ->
805 output_html outputhtml
806 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
807 "proof: " ^ Printexc.to_string e ^ "</h1>")
809 output_html outputhtml
810 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
813 let proveit rendering_window () =
814 let module L = LogicalOperations in
815 let module G = Gdome in
816 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
817 match rendering_window#output#get_selection with
820 ((node : Gdome.element)#getAttributeNS
822 ((element : G.element)#getAttributeNS
825 ~localName:(G.domString "xref"))#to_string
827 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
831 match !current_cic_infos with
832 Some (ids_to_terms, ids_to_father_ids, _, _) ->
834 L.to_sequent id ids_to_terms ids_to_father_ids ;
835 refresh_proof rendering_window#output ;
836 refresh_sequent rendering_window#proofw
837 | None -> assert false (* "ERROR: No current term!!!" *)
839 RefreshSequentException e ->
840 output_html outputhtml
841 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
842 "sequent: " ^ Printexc.to_string e ^ "</h1>")
843 | RefreshProofException e ->
844 output_html outputhtml
845 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
846 "proof: " ^ Printexc.to_string e ^ "</h1>")
848 output_html outputhtml
849 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
851 | None -> assert false (* "ERROR: No selection!!!" *)
854 let focus rendering_window () =
855 let module L = LogicalOperations in
856 let module G = Gdome in
857 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
858 match rendering_window#output#get_selection with
861 ((node : Gdome.element)#getAttributeNS
863 ((element : G.element)#getAttributeNS
866 ~localName:(G.domString "xref"))#to_string
868 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
872 match !current_cic_infos with
873 Some (ids_to_terms, ids_to_father_ids, _, _) ->
875 L.focus id ids_to_terms ids_to_father_ids ;
876 refresh_sequent rendering_window#proofw
877 | None -> assert false (* "ERROR: No current term!!!" *)
879 RefreshSequentException e ->
880 output_html outputhtml
881 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
882 "sequent: " ^ Printexc.to_string e ^ "</h1>")
883 | RefreshProofException e ->
884 output_html outputhtml
885 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
886 "proof: " ^ Printexc.to_string e ^ "</h1>")
888 output_html outputhtml
889 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
891 | None -> assert false (* "ERROR: No selection!!!" *)
894 exception NoPrevGoal;;
895 exception NoNextGoal;;
897 let prevgoal metasenv metano =
901 | [(m,_,_)] -> raise NoPrevGoal
902 | (n,_,_)::(m,_,_)::_ when m=metano -> n
908 let nextgoal metasenv metano =
912 | [(m,_,_)] when m = metano -> raise NoNextGoal
913 | (m,_,_)::(n,_,_)::_ when m=metano -> n
919 let prev_or_next_goal select_goal rendering_window () =
920 let module L = LogicalOperations in
921 let module G = Gdome in
922 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
924 match !ProofEngine.proof with
926 | Some (_,metasenv,_,_) -> metasenv
929 match !ProofEngine.goal with
934 ProofEngine.goal := Some (select_goal metasenv metano) ;
935 refresh_sequent rendering_window#proofw
937 RefreshSequentException e ->
938 output_html outputhtml
939 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
940 "sequent: " ^ Printexc.to_string e ^ "</h1>")
942 output_html outputhtml
943 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
946 exception NotADefinition;;
948 let open_ rendering_window () =
949 let inputt = (rendering_window#inputt : GEdit.text) in
950 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
951 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
952 let output = (rendering_window#output : GMathView.math_view) in
953 let proofw = (rendering_window#proofw : GMathView.math_view) in
954 let inputlen = inputt#length in
955 let input = inputt#get_chars 0 inputlen ^ "\n" in
957 let uri = UriManager.uri_of_string ("cic:" ^ input) in
958 CicTypeChecker.typecheck uri ;
960 match CicEnvironment.get_cooked_obj uri 0 with
961 Cic.Definition (_,bo,ty,_) -> [],bo,ty
962 | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
965 | Cic.InductiveDefinition _ -> raise NotADefinition
968 Some (uri, metasenv, bo, ty) ;
969 ProofEngine.goal := None ;
970 refresh_sequent proofw ;
971 refresh_proof output ;
972 inputt#delete_text 0 inputlen ;
973 ignore(oldinputt#insert_text input oldinputt#length)
975 RefreshSequentException e ->
976 output_html outputhtml
977 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
978 "sequent: " ^ Printexc.to_string e ^ "</h1>")
979 | RefreshProofException e ->
980 output_html outputhtml
981 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
982 "proof: " ^ Printexc.to_string e ^ "</h1>")
984 output_html outputhtml
985 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
988 let state rendering_window () =
989 let inputt = (rendering_window#inputt : GEdit.text) in
990 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
991 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
992 let output = (rendering_window#output : GMathView.math_view) in
993 let proofw = (rendering_window#proofw : GMathView.math_view) in
994 let inputlen = inputt#length in
995 let input = inputt#get_chars 0 inputlen ^ "\n" in
996 (* Do something interesting *)
997 let lexbuf = Lexing.from_string input in
1000 (* Execute the actions *)
1001 match CicTextualParser.main CicTextualLexer.token lexbuf with
1004 let _ = CicTypeChecker.type_of_aux' [] [] expr in
1005 ProofEngine.proof :=
1006 Some (UriManager.uri_of_string "cic:/dummy.con",
1007 [1,[],expr], Cic.Meta (1,[]), expr) ;
1008 ProofEngine.goal := Some 1 ;
1009 refresh_sequent proofw ;
1010 refresh_proof output ;
1013 CicTextualParser0.Eof ->
1014 inputt#delete_text 0 inputlen ;
1015 ignore(oldinputt#insert_text input oldinputt#length)
1016 | RefreshSequentException e ->
1017 output_html outputhtml
1018 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1019 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1020 | RefreshProofException e ->
1021 output_html outputhtml
1022 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1023 "proof: " ^ Printexc.to_string e ^ "</h1>")
1025 output_html outputhtml
1026 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1029 let check rendering_window scratch_window () =
1030 let inputt = (rendering_window#inputt : GEdit.text) in
1031 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1032 let output = (rendering_window#output : GMathView.math_view) in
1033 let proofw = (rendering_window#proofw : GMathView.math_view) in
1034 let inputlen = inputt#length in
1035 let input = inputt#get_chars 0 inputlen ^ "\n" in
1037 match !ProofEngine.proof with
1038 None -> UriManager.uri_of_string "cic:/dummy.con", []
1039 | Some (curi,metasenv,_,_) -> curi,metasenv
1041 let context,names_context =
1043 match !ProofEngine.goal with
1046 let (_,canonical_context,_) =
1047 List.find (function (m,_,_) -> m=metano) metasenv
1054 Some (n,_) -> Some n
1058 (* Do something interesting *)
1059 let lexbuf = Lexing.from_string input in
1062 (* Execute the actions *)
1064 CicTextualParserContext.main curi names_context metasenv
1065 CicTextualLexer.token lexbuf
1068 | Some (metasenv',expr) ->
1070 let ty = CicTypeChecker.type_of_aux' metasenv' context expr in
1071 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1072 scratch_window#show () ;
1073 scratch_window#mmlwidget#load_tree ~dom:mml
1076 print_endline ("? " ^ CicPp.ppterm expr) ;
1080 CicTextualParser0.Eof -> ()
1082 output_html outputhtml
1083 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1086 let locate rendering_window () =
1087 let inputt = (rendering_window#inputt : GEdit.text) in
1088 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1089 let inputlen = inputt#length in
1090 let input = inputt#get_chars 0 inputlen in
1091 output_html outputhtml (
1093 match Str.split (Str.regexp "[ \t]+") input with
1096 inputt#delete_text 0 inputlen;
1097 MQueryGenerator.locate head
1099 e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
1103 let backward rendering_window () =
1104 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1105 let inputt = (rendering_window#inputt : GEdit.text) in
1106 let inputlen = inputt#length in
1107 let input = inputt#get_chars 0 inputlen in
1108 let level = int_of_string input in
1110 match !ProofEngine.proof with
1111 None -> assert false
1112 | Some (_,metasenv,_,_) -> metasenv
1115 match !ProofEngine.goal with
1119 List.find (function (m,_,_) -> m=metano) metasenv
1121 MQueryGenerator.backward metasenv ey ty level
1123 output_html outputhtml result
1126 let choose_selection
1127 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1129 let module G = Gdome in
1130 let rec aux element =
1131 if element#hasAttributeNS
1132 ~namespaceURI:helmns
1133 ~localName:(G.domString "xref")
1135 mmlwidget#set_selection (Some element)
1137 match element#get_parentNode with
1138 None -> assert false
1139 (*CSC: OCAML DIVERGES!
1140 | Some p -> aux (new G.element_of_node p)
1142 | Some p -> aux (new Gdome.element_of_node p)
1146 | None -> mmlwidget#set_selection None
1149 (* STUFF TO BUILD THE GTK INTERFACE *)
1151 (* Stuff for the widget settings *)
1153 let export_to_postscript (output : GMathView.math_view) () =
1154 output#export_to_postscript ~filename:"output.ps" ();
1157 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1158 button_set_kerning button_set_transparency button_export_to_postscript
1161 let is_set = button_t1#active in
1162 output#set_font_manager_type
1163 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1166 button_set_anti_aliasing#misc#set_sensitive true ;
1167 button_set_kerning#misc#set_sensitive true ;
1168 button_set_transparency#misc#set_sensitive true ;
1169 button_export_to_postscript#misc#set_sensitive true ;
1173 button_set_anti_aliasing#misc#set_sensitive false ;
1174 button_set_kerning#misc#set_sensitive false ;
1175 button_set_transparency#misc#set_sensitive false ;
1176 button_export_to_postscript#misc#set_sensitive false ;
1180 let set_anti_aliasing output button_set_anti_aliasing () =
1181 output#set_anti_aliasing button_set_anti_aliasing#active
1184 let set_kerning output button_set_kerning () =
1185 output#set_kerning button_set_kerning#active
1188 let set_transparency output button_set_transparency () =
1189 output#set_transparency button_set_transparency#active
1192 let changefont output font_size_spinb () =
1193 output#set_font_size font_size_spinb#value_as_int
1196 let set_log_verbosity output log_verbosity_spinb () =
1197 output#set_log_verbosity log_verbosity_spinb#value_as_int
1200 class settings_window (output : GMathView.math_view) sw
1201 button_export_to_postscript selection_changed_callback
1203 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1205 GPack.vbox ~packing:settings_window#add () in
1208 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1209 ~border_width:5 ~packing:vbox#add () in
1211 GButton.toggle_button ~label:"activate t1 fonts"
1212 ~packing:(table#attach ~left:0 ~top:0) () in
1213 let button_set_anti_aliasing =
1214 GButton.toggle_button ~label:"set_anti_aliasing"
1215 ~packing:(table#attach ~left:0 ~top:1) () in
1216 let button_set_kerning =
1217 GButton.toggle_button ~label:"set_kerning"
1218 ~packing:(table#attach ~left:1 ~top:1) () in
1219 let button_set_transparency =
1220 GButton.toggle_button ~label:"set_transparency"
1221 ~packing:(table#attach ~left:2 ~top:1) () in
1224 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1225 ~border_width:5 ~packing:vbox#add () in
1226 let font_size_label =
1227 GMisc.label ~text:"font size:"
1228 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1229 let font_size_spinb =
1231 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1234 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1235 let log_verbosity_label =
1236 GMisc.label ~text:"log verbosity:"
1237 ~packing:(table#attach ~left:0 ~top:1) () in
1238 let log_verbosity_spinb =
1240 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1243 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1245 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1247 GButton.button ~label:"Close"
1248 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1250 method show = settings_window#show
1252 button_set_anti_aliasing#misc#set_sensitive false ;
1253 button_set_kerning#misc#set_sensitive false ;
1254 button_set_transparency#misc#set_sensitive false ;
1255 (* Signals connection *)
1256 ignore(button_t1#connect#clicked
1257 (activate_t1 output button_set_anti_aliasing button_set_kerning
1258 button_set_transparency button_export_to_postscript button_t1)) ;
1259 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1260 ignore(button_set_anti_aliasing#connect#toggled
1261 (set_anti_aliasing output button_set_anti_aliasing));
1262 ignore(button_set_kerning#connect#toggled
1263 (set_kerning output button_set_kerning)) ;
1264 ignore(button_set_transparency#connect#toggled
1265 (set_transparency output button_set_transparency)) ;
1266 ignore(log_verbosity_spinb#connect#changed
1267 (set_log_verbosity output log_verbosity_spinb)) ;
1268 ignore(closeb#connect#clicked settings_window#misc#hide)
1271 (* Scratch window *)
1273 class scratch_window outputhtml =
1275 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1277 GPack.vbox ~packing:window#add () in
1279 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1281 GButton.button ~label:"Whd"
1282 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1284 GButton.button ~label:"Reduce"
1285 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1287 GButton.button ~label:"Simpl"
1288 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1289 let scrolled_window =
1290 GBin.scrolled_window ~border_width:10
1291 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1294 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1296 method outputhtml = outputhtml
1297 method mmlwidget = mmlwidget
1298 method show () = window#misc#hide () ; window#show ()
1300 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1301 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1302 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1303 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1304 ignore(simplb#connect#clicked (simpl_in_scratch self))
1309 class rendering_window output proofw (label : GMisc.label) =
1311 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1313 GPack.hbox ~packing:window#add () in
1315 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1316 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1317 let scrolled_window0 =
1318 GBin.scrolled_window ~border_width:10
1319 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1320 let _ = scrolled_window0#add output#coerce in
1322 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1324 GButton.button ~label:"Settings"
1325 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1326 let button_export_to_postscript =
1327 GButton.button ~label:"export_to_postscript"
1328 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1330 GButton.button ~label:"Qed"
1331 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1333 GButton.button ~label:"Save"
1334 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1336 GButton.button ~label:"Load"
1337 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1339 GButton.button ~label:"Close"
1340 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1342 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1344 GButton.button ~label:"Prove It"
1345 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1347 GButton.button ~label:"Focus"
1348 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1350 GButton.button ~label:"<"
1351 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1353 GButton.button ~label:">"
1354 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1355 let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1356 ~packing:(vbox#pack ~padding:5) () in
1358 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1360 GButton.button ~label:"State"
1361 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1363 GButton.button ~label:"Open"
1364 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1366 GButton.button ~label:"Check"
1367 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1369 GButton.button ~label:"Locate"
1370 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1372 GButton.button ~label:"Backward"
1373 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1374 let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1375 ~packing:(vbox#pack ~padding:5) () in
1377 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1378 let scrolled_window1 =
1379 GBin.scrolled_window ~border_width:10
1380 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1381 let _ = scrolled_window1#add proofw#coerce in
1383 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1385 GButton.button ~label:"Exact"
1386 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1388 GButton.button ~label:"Intros"
1389 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1391 GButton.button ~label:"Apply"
1392 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1393 let elimintrossimplb =
1394 GButton.button ~label:"ElimIntrosSimpl"
1395 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1397 GButton.button ~label:"ElimType"
1398 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1400 GButton.button ~label:"Whd"
1401 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1403 GButton.button ~label:"Reduce"
1404 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1406 GButton.button ~label:"Simpl"
1407 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1409 GButton.button ~label:"Fold"
1410 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1412 GButton.button ~label:"Cut"
1413 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1415 GButton.button ~label:"Change"
1416 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1418 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1420 GButton.button ~label:"Let ... In"
1421 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1423 GButton.button ~label:"Ring"
1424 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1426 GButton.button ~label:"ClearBody"
1427 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1429 GButton.button ~label:"Clear"
1430 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1433 ~source:"<html><body bgColor=\"white\"></body></html>"
1434 ~width:400 ~height: 200
1435 ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1437 let scratch_window = new scratch_window outputhtml in
1439 method outputhtml = outputhtml
1440 method oldinputt = oldinputt
1441 method inputt = inputt
1442 method output = (output : GMathView.math_view)
1443 method proofw = (proofw : GMathView.math_view)
1444 method show = window#show
1446 button_export_to_postscript#misc#set_sensitive false ;
1448 (* signal handlers here *)
1449 ignore(output#connect#selection_changed
1450 (function elem -> proofw#unload ; choose_selection output elem)) ;
1451 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1452 ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1453 let settings_window = new settings_window output scrolled_window0
1454 button_export_to_postscript (choose_selection output) in
1455 ignore(settingsb#connect#clicked settings_window#show) ;
1456 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1457 ignore(qedb#connect#clicked (qed self)) ;
1458 ignore(saveb#connect#clicked (save self)) ;
1459 ignore(loadb#connect#clicked (load self)) ;
1460 ignore(proveitb#connect#clicked (proveit self)) ;
1461 ignore(focusb#connect#clicked (focus self)) ;
1462 ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ;
1463 ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ;
1464 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1465 ignore(stateb#connect#clicked (state self)) ;
1466 ignore(openb#connect#clicked (open_ self)) ;
1467 ignore(checkb#connect#clicked (check self scratch_window)) ;
1468 ignore(locateb#connect#clicked (locate self)) ;
1469 ignore(backwardb#connect#clicked (backward self)) ;
1470 ignore(exactb#connect#clicked (exact self)) ;
1471 ignore(applyb#connect#clicked (apply self)) ;
1472 ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
1473 ignore(elimtypeb#connect#clicked (elimtype self)) ;
1474 ignore(whdb#connect#clicked (whd self)) ;
1475 ignore(reduceb#connect#clicked (reduce self)) ;
1476 ignore(simplb#connect#clicked (simpl self)) ;
1477 ignore(foldb#connect#clicked (fold self)) ;
1478 ignore(cutb#connect#clicked (cut self)) ;
1479 ignore(changeb#connect#clicked (change self)) ;
1480 ignore(letinb#connect#clicked (letin self)) ;
1481 ignore(ringb#connect#clicked (ring self)) ;
1482 ignore(clearbodyb#connect#clicked (clearbody self)) ;
1483 ignore(clearb#connect#clicked (clear self)) ;
1484 ignore(introsb#connect#clicked (intros self)) ;
1485 Logger.log_callback :=
1486 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1491 let initialize_everything () =
1492 let module U = Unix in
1493 let output = GMathView.math_view ~width:400 ~height:280 ()
1494 and proofw = GMathView.math_view ~width:400 ~height:275 ()
1495 and label = GMisc.label ~text:"gTopLevel" () in
1496 let rendering_window =
1497 new rendering_window output proofw label
1499 rendering_window#show () ;
1504 CicCooking.init () ;
1505 if !usedb then MQueryGenerator.init () ;
1506 ignore (GtkMain.Main.init ()) ;
1507 initialize_everything () ;
1508 if !usedb then MQueryGenerator.close ();