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 = "/public/sacerdot/currentproof";;
51 (*CSC: the getter should handle the innertypes, not the FS *)
52 let innertypesfile = "/public/sacerdot/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
685 let fourier rendering_window = call_tactic ProofEngine.fourier rendering_window;;
688 let whd_in_scratch scratch_window =
689 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
692 let reduce_in_scratch scratch_window =
693 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
696 let simpl_in_scratch scratch_window =
697 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
703 (**********************)
705 (**********************)
707 exception OpenConjecturesStillThere;;
708 exception WrongProof;;
710 let qed rendering_window () =
711 match !ProofEngine.proof with
713 | Some (uri,[],bo,ty) ->
715 CicReduction.are_convertible []
716 (CicTypeChecker.type_of_aux' [] [] bo) ty
719 (*CSC: Wrong: [] is just plainly wrong *)
720 let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
722 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
723 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
725 Cic2acic.acic_object_of_cic_object proof
728 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
730 (rendering_window#output : GMathView.math_view)#load_tree mml ;
733 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
738 | _ -> raise OpenConjecturesStillThere
742 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
744 let dtdname = "/projects/helm/V7/dtd/cic.dtd";;
746 let save rendering_window () =
747 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
748 match !ProofEngine.proof with
750 | Some (uri, metasenv, bo, ty) ->
752 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
754 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
755 Cic2acic.acic_object_of_cic_object currentproof
757 let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in
759 [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
761 ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
765 Xml.pp ~quiet:true xml' (Some prooffile) ;
766 output_html outputhtml
767 ("<h1 color=\"Green\">Current proof saved to " ^
771 (* Used to typecheck the loaded proofs *)
772 let typecheck_loaded_proof metasenv bo ty =
773 let module T = CicTypeChecker in
774 (*CSC: bisogna controllare anche il metasenv!!! *)
775 ignore (T.type_of_aux' metasenv [] ty) ;
776 ignore (T.type_of_aux' metasenv [] bo)
779 let load rendering_window () =
780 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
781 let output = (rendering_window#output : GMathView.math_view) in
782 let proofw = (rendering_window#proofw : GMathView.math_view) in
784 let uri = UriManager.uri_of_string "cic:/dummy.con" in
785 match CicParser.obj_of_xml prooffile uri with
786 Cic.CurrentProof (_,metasenv,bo,ty) ->
787 typecheck_loaded_proof metasenv bo ty ;
789 Some (uri, metasenv, bo, ty) ;
793 | (metano,_,_)::_ -> Some metano
795 refresh_proof output ;
796 refresh_sequent proofw ;
797 output_html outputhtml
798 ("<h1 color=\"Green\">Current proof loaded from " ^
802 RefreshSequentException e ->
803 output_html outputhtml
804 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
805 "sequent: " ^ Printexc.to_string e ^ "</h1>")
806 | RefreshProofException e ->
807 output_html outputhtml
808 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
809 "proof: " ^ Printexc.to_string e ^ "</h1>")
811 output_html outputhtml
812 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
815 let proveit rendering_window () =
816 let module L = LogicalOperations in
817 let module G = Gdome in
818 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
819 match rendering_window#output#get_selection with
822 ((node : Gdome.element)#getAttributeNS
824 ((element : G.element)#getAttributeNS
827 ~localName:(G.domString "xref"))#to_string
829 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
833 match !current_cic_infos with
834 Some (ids_to_terms, ids_to_father_ids, _, _) ->
836 L.to_sequent id ids_to_terms ids_to_father_ids ;
837 refresh_proof rendering_window#output ;
838 refresh_sequent rendering_window#proofw
839 | None -> assert false (* "ERROR: No current term!!!" *)
841 RefreshSequentException e ->
842 output_html outputhtml
843 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
844 "sequent: " ^ Printexc.to_string e ^ "</h1>")
845 | RefreshProofException e ->
846 output_html outputhtml
847 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
848 "proof: " ^ Printexc.to_string e ^ "</h1>")
850 output_html outputhtml
851 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
853 | None -> assert false (* "ERROR: No selection!!!" *)
856 let focus rendering_window () =
857 let module L = LogicalOperations in
858 let module G = Gdome in
859 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
860 match rendering_window#output#get_selection with
863 ((node : Gdome.element)#getAttributeNS
865 ((element : G.element)#getAttributeNS
868 ~localName:(G.domString "xref"))#to_string
870 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
874 match !current_cic_infos with
875 Some (ids_to_terms, ids_to_father_ids, _, _) ->
877 L.focus id ids_to_terms ids_to_father_ids ;
878 refresh_sequent rendering_window#proofw
879 | None -> assert false (* "ERROR: No current term!!!" *)
881 RefreshSequentException e ->
882 output_html outputhtml
883 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
884 "sequent: " ^ Printexc.to_string e ^ "</h1>")
885 | RefreshProofException e ->
886 output_html outputhtml
887 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
888 "proof: " ^ Printexc.to_string e ^ "</h1>")
890 output_html outputhtml
891 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
893 | None -> assert false (* "ERROR: No selection!!!" *)
896 exception NoPrevGoal;;
897 exception NoNextGoal;;
899 let prevgoal metasenv metano =
903 | [(m,_,_)] -> raise NoPrevGoal
904 | (n,_,_)::(m,_,_)::_ when m=metano -> n
910 let nextgoal metasenv metano =
914 | [(m,_,_)] when m = metano -> raise NoNextGoal
915 | (m,_,_)::(n,_,_)::_ when m=metano -> n
921 let prev_or_next_goal select_goal rendering_window () =
922 let module L = LogicalOperations in
923 let module G = Gdome in
924 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
926 match !ProofEngine.proof with
928 | Some (_,metasenv,_,_) -> metasenv
931 match !ProofEngine.goal with
936 ProofEngine.goal := Some (select_goal metasenv metano) ;
937 refresh_sequent rendering_window#proofw
939 RefreshSequentException e ->
940 output_html outputhtml
941 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
942 "sequent: " ^ Printexc.to_string e ^ "</h1>")
944 output_html outputhtml
945 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
948 exception NotADefinition;;
950 let open_ rendering_window () =
951 let inputt = (rendering_window#inputt : GEdit.text) in
952 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
953 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
954 let output = (rendering_window#output : GMathView.math_view) in
955 let proofw = (rendering_window#proofw : GMathView.math_view) in
956 let inputlen = inputt#length in
957 let input = inputt#get_chars 0 inputlen ^ "\n" in
959 let uri = UriManager.uri_of_string ("cic:" ^ input) in
960 CicTypeChecker.typecheck uri ;
962 match CicEnvironment.get_cooked_obj uri 0 with
963 Cic.Definition (_,bo,ty,_) -> [],bo,ty
964 | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
967 | Cic.InductiveDefinition _ -> raise NotADefinition
970 Some (uri, metasenv, bo, ty) ;
971 ProofEngine.goal := None ;
972 refresh_sequent proofw ;
973 refresh_proof output ;
974 inputt#delete_text 0 inputlen ;
975 ignore(oldinputt#insert_text input oldinputt#length)
977 RefreshSequentException e ->
978 output_html outputhtml
979 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
980 "sequent: " ^ Printexc.to_string e ^ "</h1>")
981 | RefreshProofException e ->
982 output_html outputhtml
983 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
984 "proof: " ^ Printexc.to_string e ^ "</h1>")
986 output_html outputhtml
987 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
990 let state rendering_window () =
991 let inputt = (rendering_window#inputt : GEdit.text) in
992 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
993 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
994 let output = (rendering_window#output : GMathView.math_view) in
995 let proofw = (rendering_window#proofw : GMathView.math_view) in
996 let inputlen = inputt#length in
997 let input = inputt#get_chars 0 inputlen ^ "\n" in
998 (* Do something interesting *)
999 let lexbuf = Lexing.from_string input in
1002 (* Execute the actions *)
1003 match CicTextualParser.main CicTextualLexer.token lexbuf with
1006 let _ = CicTypeChecker.type_of_aux' [] [] expr in
1007 ProofEngine.proof :=
1008 Some (UriManager.uri_of_string "cic:/dummy.con",
1009 [1,[],expr], Cic.Meta (1,[]), expr) ;
1010 ProofEngine.goal := Some 1 ;
1011 refresh_sequent proofw ;
1012 refresh_proof output ;
1015 CicTextualParser0.Eof ->
1016 inputt#delete_text 0 inputlen ;
1017 ignore(oldinputt#insert_text input oldinputt#length)
1018 | RefreshSequentException e ->
1019 output_html outputhtml
1020 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1021 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1022 | RefreshProofException e ->
1023 output_html outputhtml
1024 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1025 "proof: " ^ Printexc.to_string e ^ "</h1>")
1027 output_html outputhtml
1028 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1031 let check rendering_window scratch_window () =
1032 let inputt = (rendering_window#inputt : GEdit.text) in
1033 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1034 let output = (rendering_window#output : GMathView.math_view) in
1035 let proofw = (rendering_window#proofw : GMathView.math_view) in
1036 let inputlen = inputt#length in
1037 let input = inputt#get_chars 0 inputlen ^ "\n" in
1039 match !ProofEngine.proof with
1040 None -> UriManager.uri_of_string "cic:/dummy.con", []
1041 | Some (curi,metasenv,_,_) -> curi,metasenv
1043 let context,names_context =
1045 match !ProofEngine.goal with
1048 let (_,canonical_context,_) =
1049 List.find (function (m,_,_) -> m=metano) metasenv
1056 Some (n,_) -> Some n
1060 (* Do something interesting *)
1061 let lexbuf = Lexing.from_string input in
1064 (* Execute the actions *)
1066 CicTextualParserContext.main curi names_context metasenv
1067 CicTextualLexer.token lexbuf
1070 | Some (metasenv',expr) ->
1072 let ty = CicTypeChecker.type_of_aux' metasenv' context expr in
1073 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1074 scratch_window#show () ;
1075 scratch_window#mmlwidget#load_tree ~dom:mml
1078 print_endline ("? " ^ CicPp.ppterm expr) ;
1082 CicTextualParser0.Eof -> ()
1084 output_html outputhtml
1085 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1088 let locate rendering_window () =
1089 let inputt = (rendering_window#inputt : GEdit.text) in
1090 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1091 let inputlen = inputt#length in
1092 let input = inputt#get_chars 0 inputlen in
1093 output_html outputhtml (
1095 match Str.split (Str.regexp "[ \t]+") input with
1098 inputt#delete_text 0 inputlen;
1099 MQueryGenerator.locate_html head
1101 e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
1105 let backward rendering_window () =
1106 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1107 let inputt = (rendering_window#inputt : GEdit.text) in
1108 let inputlen = inputt#length in
1109 let input = inputt#get_chars 0 inputlen in
1110 let level = int_of_string input in
1112 match !ProofEngine.proof with
1113 None -> assert false
1114 | Some (_,metasenv,_,_) -> metasenv
1117 match !ProofEngine.goal with
1121 List.find (function (m,_,_) -> m=metano) metasenv
1123 MQueryGenerator.backward metasenv ey ty level
1125 output_html outputhtml result
1128 let choose_selection
1129 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1131 let module G = Gdome in
1132 let rec aux element =
1133 if element#hasAttributeNS
1134 ~namespaceURI:helmns
1135 ~localName:(G.domString "xref")
1137 mmlwidget#set_selection (Some element)
1139 match element#get_parentNode with
1140 None -> assert false
1141 (*CSC: OCAML DIVERGES!
1142 | Some p -> aux (new G.element_of_node p)
1144 | Some p -> aux (new Gdome.element_of_node p)
1148 | None -> mmlwidget#set_selection None
1151 (* STUFF TO BUILD THE GTK INTERFACE *)
1153 (* Stuff for the widget settings *)
1155 let export_to_postscript (output : GMathView.math_view) () =
1156 output#export_to_postscript ~filename:"output.ps" ();
1159 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1160 button_set_kerning button_set_transparency button_export_to_postscript
1163 let is_set = button_t1#active in
1164 output#set_font_manager_type
1165 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1168 button_set_anti_aliasing#misc#set_sensitive true ;
1169 button_set_kerning#misc#set_sensitive true ;
1170 button_set_transparency#misc#set_sensitive true ;
1171 button_export_to_postscript#misc#set_sensitive true ;
1175 button_set_anti_aliasing#misc#set_sensitive false ;
1176 button_set_kerning#misc#set_sensitive false ;
1177 button_set_transparency#misc#set_sensitive false ;
1178 button_export_to_postscript#misc#set_sensitive false ;
1182 let set_anti_aliasing output button_set_anti_aliasing () =
1183 output#set_anti_aliasing button_set_anti_aliasing#active
1186 let set_kerning output button_set_kerning () =
1187 output#set_kerning button_set_kerning#active
1190 let set_transparency output button_set_transparency () =
1191 output#set_transparency button_set_transparency#active
1194 let changefont output font_size_spinb () =
1195 output#set_font_size font_size_spinb#value_as_int
1198 let set_log_verbosity output log_verbosity_spinb () =
1199 output#set_log_verbosity log_verbosity_spinb#value_as_int
1202 class settings_window (output : GMathView.math_view) sw
1203 button_export_to_postscript selection_changed_callback
1205 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1207 GPack.vbox ~packing:settings_window#add () in
1210 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1211 ~border_width:5 ~packing:vbox#add () in
1213 GButton.toggle_button ~label:"activate t1 fonts"
1214 ~packing:(table#attach ~left:0 ~top:0) () in
1215 let button_set_anti_aliasing =
1216 GButton.toggle_button ~label:"set_anti_aliasing"
1217 ~packing:(table#attach ~left:0 ~top:1) () in
1218 let button_set_kerning =
1219 GButton.toggle_button ~label:"set_kerning"
1220 ~packing:(table#attach ~left:1 ~top:1) () in
1221 let button_set_transparency =
1222 GButton.toggle_button ~label:"set_transparency"
1223 ~packing:(table#attach ~left:2 ~top:1) () in
1226 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1227 ~border_width:5 ~packing:vbox#add () in
1228 let font_size_label =
1229 GMisc.label ~text:"font size:"
1230 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1231 let font_size_spinb =
1233 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1236 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1237 let log_verbosity_label =
1238 GMisc.label ~text:"log verbosity:"
1239 ~packing:(table#attach ~left:0 ~top:1) () in
1240 let log_verbosity_spinb =
1242 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1245 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1247 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1249 GButton.button ~label:"Close"
1250 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1252 method show = settings_window#show
1254 button_set_anti_aliasing#misc#set_sensitive false ;
1255 button_set_kerning#misc#set_sensitive false ;
1256 button_set_transparency#misc#set_sensitive false ;
1257 (* Signals connection *)
1258 ignore(button_t1#connect#clicked
1259 (activate_t1 output button_set_anti_aliasing button_set_kerning
1260 button_set_transparency button_export_to_postscript button_t1)) ;
1261 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1262 ignore(button_set_anti_aliasing#connect#toggled
1263 (set_anti_aliasing output button_set_anti_aliasing));
1264 ignore(button_set_kerning#connect#toggled
1265 (set_kerning output button_set_kerning)) ;
1266 ignore(button_set_transparency#connect#toggled
1267 (set_transparency output button_set_transparency)) ;
1268 ignore(log_verbosity_spinb#connect#changed
1269 (set_log_verbosity output log_verbosity_spinb)) ;
1270 ignore(closeb#connect#clicked settings_window#misc#hide)
1273 (* Scratch window *)
1275 class scratch_window outputhtml =
1277 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1279 GPack.vbox ~packing:window#add () in
1281 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1283 GButton.button ~label:"Whd"
1284 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1286 GButton.button ~label:"Reduce"
1287 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1289 GButton.button ~label:"Simpl"
1290 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1291 let scrolled_window =
1292 GBin.scrolled_window ~border_width:10
1293 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1296 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1298 method outputhtml = outputhtml
1299 method mmlwidget = mmlwidget
1300 method show () = window#misc#hide () ; window#show ()
1302 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1303 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1304 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1305 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1306 ignore(simplb#connect#clicked (simpl_in_scratch self))
1311 class rendering_window output proofw (label : GMisc.label) =
1313 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1315 GPack.hbox ~packing:window#add () in
1317 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1318 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1319 let scrolled_window0 =
1320 GBin.scrolled_window ~border_width:10
1321 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1322 let _ = scrolled_window0#add output#coerce in
1324 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1326 GButton.button ~label:"Settings"
1327 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1328 let button_export_to_postscript =
1329 GButton.button ~label:"export_to_postscript"
1330 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1332 GButton.button ~label:"Qed"
1333 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1335 GButton.button ~label:"Save"
1336 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1338 GButton.button ~label:"Load"
1339 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1341 GButton.button ~label:"Close"
1342 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1344 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1346 GButton.button ~label:"Prove It"
1347 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1349 GButton.button ~label:"Focus"
1350 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1352 GButton.button ~label:"<"
1353 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1355 GButton.button ~label:">"
1356 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1357 let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1358 ~packing:(vbox#pack ~padding:5) () in
1360 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1362 GButton.button ~label:"State"
1363 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1365 GButton.button ~label:"Open"
1366 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1368 GButton.button ~label:"Check"
1369 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1371 GButton.button ~label:"Locate"
1372 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1374 GButton.button ~label:"Backward"
1375 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1376 let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1377 ~packing:(vbox#pack ~padding:5) () in
1379 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1380 let scrolled_window1 =
1381 GBin.scrolled_window ~border_width:10
1382 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1383 let _ = scrolled_window1#add proofw#coerce in
1385 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1387 GButton.button ~label:"Exact"
1388 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1390 GButton.button ~label:"Intros"
1391 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1393 GButton.button ~label:"Apply"
1394 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1395 let elimintrossimplb =
1396 GButton.button ~label:"ElimIntrosSimpl"
1397 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1399 GButton.button ~label:"ElimType"
1400 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1402 GButton.button ~label:"Whd"
1403 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1405 GButton.button ~label:"Reduce"
1406 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1408 GButton.button ~label:"Simpl"
1409 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1411 GButton.button ~label:"Fold"
1412 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1414 GButton.button ~label:"Cut"
1415 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1417 GButton.button ~label:"Change"
1418 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1420 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1422 GButton.button ~label:"Let ... In"
1423 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1425 GButton.button ~label:"Ring"
1426 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1428 GButton.button ~label:"ClearBody"
1429 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1431 GButton.button ~label:"Clear"
1432 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1434 GButton.button ~label:"Fourier"
1435 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1438 ~source:"<html><body bgColor=\"white\"></body></html>"
1439 ~width:400 ~height: 200
1440 ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1442 let scratch_window = new scratch_window outputhtml in
1444 method outputhtml = outputhtml
1445 method oldinputt = oldinputt
1446 method inputt = inputt
1447 method output = (output : GMathView.math_view)
1448 method proofw = (proofw : GMathView.math_view)
1449 method show = window#show
1451 button_export_to_postscript#misc#set_sensitive false ;
1453 (* signal handlers here *)
1454 ignore(output#connect#selection_changed
1455 (function elem -> proofw#unload ; choose_selection output elem)) ;
1456 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1457 ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1458 let settings_window = new settings_window output scrolled_window0
1459 button_export_to_postscript (choose_selection output) in
1460 ignore(settingsb#connect#clicked settings_window#show) ;
1461 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1462 ignore(qedb#connect#clicked (qed self)) ;
1463 ignore(saveb#connect#clicked (save self)) ;
1464 ignore(loadb#connect#clicked (load self)) ;
1465 ignore(proveitb#connect#clicked (proveit self)) ;
1466 ignore(focusb#connect#clicked (focus self)) ;
1467 ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ;
1468 ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ;
1469 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1470 ignore(stateb#connect#clicked (state self)) ;
1471 ignore(openb#connect#clicked (open_ self)) ;
1472 ignore(checkb#connect#clicked (check self scratch_window)) ;
1473 ignore(locateb#connect#clicked (locate self)) ;
1474 ignore(backwardb#connect#clicked (backward self)) ;
1475 ignore(exactb#connect#clicked (exact self)) ;
1476 ignore(applyb#connect#clicked (apply self)) ;
1477 ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
1478 ignore(elimtypeb#connect#clicked (elimtype self)) ;
1479 ignore(whdb#connect#clicked (whd self)) ;
1480 ignore(reduceb#connect#clicked (reduce self)) ;
1481 ignore(simplb#connect#clicked (simpl self)) ;
1482 ignore(foldb#connect#clicked (fold self)) ;
1483 ignore(cutb#connect#clicked (cut self)) ;
1484 ignore(changeb#connect#clicked (change self)) ;
1485 ignore(letinb#connect#clicked (letin self)) ;
1486 ignore(ringb#connect#clicked (ring self)) ;
1487 ignore(clearbodyb#connect#clicked (clearbody self)) ;
1488 ignore(clearb#connect#clicked (clear self)) ;
1489 ignore(fourierb#connect#clicked (fourier self)) ;
1490 ignore(introsb#connect#clicked (intros self)) ;
1491 Logger.log_callback :=
1492 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1497 let initialize_everything () =
1498 let module U = Unix in
1499 let output = GMathView.math_view ~width:400 ~height:280 ()
1500 and proofw = GMathView.math_view ~width:400 ~height:275 ()
1501 and label = GMisc.label ~text:"gTopLevel" () in
1502 let rendering_window =
1503 new rendering_window output proofw label
1505 rendering_window#show () ;
1510 CicCooking.init () ;
1513 MQueryGenerator.init () ;
1514 CicTextualParser0.set_locate_object
1516 let MathQL.MQRefs uris = MQueryGenerator.locate id in
1521 | _ -> None (* here we must let the user choose one uri *)
1525 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
1526 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1527 Some (Cic.Const (UriManager.uri_of_string uri',0))
1530 (*CSC: the locate query now looks only for inductive type blocks ;-( *)
1531 (*CSC: when it will be correctly implemented we will have to work *)
1532 (*CSC: here on the fragment identifier *)
1535 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1536 Some (Cic.MutInd (UriManager.uri_of_string uri'',0,typeno))
1540 ignore (GtkMain.Main.init ()) ;
1541 initialize_everything () ;
1542 if !usedb then MQueryGenerator.close ();