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 (******************************************************************************)
37 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
38 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
40 let index_sharp = String.index uri '#' in
41 let index_rest = index_sharp + 10 in
42 let baseuri = String.sub uri 0 index_sharp in
43 let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
48 (* GLOBAL CONSTANTS *)
50 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
54 " <body bgColor=\"white\">"
63 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
65 let prooffile = "/public/sacerdot/currentproof";;
66 (*CSC: the getter should handle the innertypes, not the FS *)
68 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
70 let innertypesfile = "/public/sacerdot/innertypes";;
72 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
74 let htmlheader_and_content = ref htmlheader;;
76 let current_cic_infos = ref None;;
77 let current_goal_infos = ref None;;
78 let current_scratch_infos = ref None;;
80 (* COMMAND LINE OPTIONS *)
86 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
89 Arg.parse argspec ignore ""
94 let domImpl = Gdome.domImplementation ();;
98 domImpl#createDocumentFromURI
100 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
102 ~uri:("styles/" ^ name) ()
104 Gdome_xslt.processStylesheet style
107 let d_c = parseStyle "drop_coercions.xsl";;
108 let tc1 = parseStyle "objtheorycontent.xsl";;
109 let hc2 = parseStyle "content_to_html.xsl";;
110 let l = parseStyle "link.xsl";;
112 let c1 = parseStyle "rootcontent.xsl";;
113 let g = parseStyle "genmmlid.xsl";;
114 let c2 = parseStyle "annotatedpres.xsl";;
117 let getterURL = Configuration.getter_url;;
118 let processorURL = Configuration.processor_url;;
120 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
122 ["processorURL", "'" ^ processorURL ^ "'" ;
123 "getterURL", "'" ^ getterURL ^ "'" ;
124 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
125 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
126 "UNICODEvsSYMBOL", "'symbol'" ;
127 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
128 "encoding", "'iso-8859-1'" ;
129 "media-type", "'text/html'" ;
130 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
131 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
132 "naturalLanguage", "'yes'" ;
133 "annotations", "'no'" ;
134 "explodeall", "'true()'" ;
135 "topurl", "'http://phd.cs.unibo.it/helm'" ;
136 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
139 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
141 ["processorURL", "'" ^ processorURL ^ "'" ;
142 "getterURL", "'" ^ getterURL ^ "'" ;
143 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
144 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
145 "UNICODEvsSYMBOL", "'symbol'" ;
146 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
147 "encoding", "'iso-8859-1'" ;
148 "media-type", "'text/html'" ;
149 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
150 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
151 "naturalLanguage", "'no'" ;
152 "annotations", "'no'" ;
153 "explodeall", "'true()'" ;
154 "topurl", "'http://phd.cs.unibo.it/helm'" ;
155 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
158 let parse_file filename =
159 let inch = open_in filename in
160 let rec read_lines () =
162 let line = input_line inch in
170 let applyStylesheets input styles args =
171 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
175 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
177 Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
180 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
183 let input = Xml2Gdome.document_of_xml domImpl xml in
184 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
185 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
187 Xml.pp xmlinnertypes (Some innertypesfile) ;
188 let output = applyStylesheets input mml_styles mml_args in
195 exception RefreshSequentException of exn;;
196 exception RefreshProofException of exn;;
198 let refresh_proof (output : GMathView.math_view) =
200 let uri,currentproof =
201 match !ProofEngine.proof with
203 | Some (uri,metasenv,bo,ty) ->
204 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
207 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
208 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
210 Cic2acic.acic_object_of_cic_object currentproof
213 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
215 output#load_tree mml ;
217 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
220 match !ProofEngine.proof with
222 | Some (uri,metasenv,bo,ty) ->
223 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ;
224 raise (RefreshProofException e)
227 let refresh_sequent (proofw : GMathView.math_view) =
229 match !ProofEngine.goal with
230 None -> proofw#unload
233 match !ProofEngine.proof with
235 | Some (_,metasenv,_,_) -> metasenv
237 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
238 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
239 SequentPp.XmlPp.print_sequent metasenv currentsequent
242 Xml2Gdome.document_of_xml domImpl sequent_gdome
245 applyStylesheets sequent_doc sequent_styles sequent_args
247 proofw#load_tree ~dom:sequent_mml ;
248 current_goal_infos :=
249 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
253 match !ProofEngine.goal with
258 match !ProofEngine.proof with
260 | Some (_,metasenv,_,_) -> metasenv
262 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
263 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
264 raise (RefreshSequentException e)
268 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
269 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
272 let mml_of_cic_term metano term =
274 match !ProofEngine.proof with
276 | Some (_,metasenv,_,_) -> metasenv
279 match !ProofEngine.goal with
282 let (_,canonical_context,_) =
283 List.find (function (m,_,_) -> m=metano) metasenv
287 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
288 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
291 Xml2Gdome.document_of_xml domImpl sequent_gdome
294 applyStylesheets sequent_doc sequent_styles sequent_args ;
296 current_scratch_infos :=
297 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
301 let output_html outputhtml msg =
302 htmlheader_and_content := !htmlheader_and_content ^ msg ;
303 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
304 outputhtml#set_topline (-1)
307 (***********************)
309 (***********************)
311 let call_tactic tactic rendering_window () =
312 let proofw = (rendering_window#proofw : GMathView.math_view) in
313 let output = (rendering_window#output : GMathView.math_view) in
314 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
315 let savedproof = !ProofEngine.proof in
316 let savedgoal = !ProofEngine.goal in
320 refresh_sequent proofw ;
323 RefreshSequentException e ->
324 output_html outputhtml
325 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
326 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
327 ProofEngine.proof := savedproof ;
328 ProofEngine.goal := savedgoal ;
329 refresh_sequent proofw
330 | RefreshProofException e ->
331 output_html outputhtml
332 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
333 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
334 ProofEngine.proof := savedproof ;
335 ProofEngine.goal := savedgoal ;
336 refresh_sequent proofw ;
339 output_html outputhtml
340 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
341 ProofEngine.proof := savedproof ;
342 ProofEngine.goal := savedgoal ;
346 let call_tactic_with_input tactic rendering_window () =
347 let proofw = (rendering_window#proofw : GMathView.math_view) in
348 let output = (rendering_window#output : GMathView.math_view) in
349 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
350 let inputt = (rendering_window#inputt : GEdit.text) in
351 let savedproof = !ProofEngine.proof in
352 let savedgoal = !ProofEngine.goal in
353 (*CSC: Gran cut&paste da sotto... *)
354 let inputlen = inputt#length in
355 let input = inputt#get_chars 0 inputlen ^ "\n" in
356 let lexbuf = Lexing.from_string input in
358 match !ProofEngine.proof with
360 | Some (curi,_,_,_) -> curi
362 let uri,metasenv,bo,ty =
363 match !ProofEngine.proof with
365 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
372 (match !ProofEngine.goal with
375 let (_,canonical_context,_) =
376 List.find (function (m,_,_) -> m=metano) metasenv
384 CicTextualParserContext.main
385 curi context metasenv CicTextualLexer.token lexbuf
388 | Some (metasenv',expr) ->
389 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
391 refresh_sequent proofw ;
395 CicTextualParser0.Eof ->
396 inputt#delete_text 0 inputlen
397 | RefreshSequentException e ->
398 output_html outputhtml
399 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
400 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
401 ProofEngine.proof := savedproof ;
402 ProofEngine.goal := savedgoal ;
403 refresh_sequent proofw
404 | RefreshProofException e ->
405 output_html outputhtml
406 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
407 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
408 ProofEngine.proof := savedproof ;
409 ProofEngine.goal := savedgoal ;
410 refresh_sequent proofw ;
413 output_html outputhtml
414 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
415 ProofEngine.proof := savedproof ;
416 ProofEngine.goal := savedgoal ;
419 let call_tactic_with_goal_input tactic rendering_window () =
420 let module L = LogicalOperations in
421 let module G = Gdome in
422 let proofw = (rendering_window#proofw : GMathView.math_view) in
423 let output = (rendering_window#output : GMathView.math_view) in
424 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
425 let savedproof = !ProofEngine.proof in
426 let savedgoal = !ProofEngine.goal in
427 match proofw#get_selection with
430 ((node : Gdome.element)#getAttributeNS
432 ~localName:(G.domString "xref"))#to_string
434 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
438 match !current_goal_infos with
439 Some (ids_to_terms, ids_to_father_ids,_) ->
441 tactic (Hashtbl.find ids_to_terms id) ;
442 refresh_sequent rendering_window#proofw ;
443 refresh_proof rendering_window#output
444 | None -> assert false (* "ERROR: No current term!!!" *)
446 RefreshSequentException e ->
447 output_html outputhtml
448 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
449 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
450 ProofEngine.proof := savedproof ;
451 ProofEngine.goal := savedgoal ;
452 refresh_sequent proofw
453 | RefreshProofException e ->
454 output_html outputhtml
455 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
456 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
457 ProofEngine.proof := savedproof ;
458 ProofEngine.goal := savedgoal ;
459 refresh_sequent proofw ;
462 output_html outputhtml
463 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
464 ProofEngine.proof := savedproof ;
465 ProofEngine.goal := savedgoal ;
468 output_html outputhtml
469 ("<h1 color=\"red\">No term selected</h1>")
472 let call_tactic_with_input_and_goal_input tactic rendering_window () =
473 let module L = LogicalOperations in
474 let module G = Gdome in
475 let proofw = (rendering_window#proofw : GMathView.math_view) in
476 let output = (rendering_window#output : GMathView.math_view) in
477 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
478 let inputt = (rendering_window#inputt : GEdit.text) in
479 let savedproof = !ProofEngine.proof in
480 let savedgoal = !ProofEngine.goal in
481 match proofw#get_selection with
484 ((node : Gdome.element)#getAttributeNS
486 ~localName:(G.domString "xref"))#to_string
488 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
492 match !current_goal_infos with
493 Some (ids_to_terms, ids_to_father_ids,_) ->
495 (* Let's parse the input *)
496 let inputlen = inputt#length in
497 let input = inputt#get_chars 0 inputlen ^ "\n" in
498 let lexbuf = Lexing.from_string input in
500 match !ProofEngine.proof with
502 | Some (curi,_,_,_) -> curi
504 let uri,metasenv,bo,ty =
505 match !ProofEngine.proof with
507 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
514 (match !ProofEngine.goal with
517 let (_,canonical_context,_) =
518 List.find (function (m,_,_) -> m=metano) metasenv
527 CicTextualParserContext.main curi context metasenv
528 CicTextualLexer.token lexbuf
531 | Some (metasenv',expr) ->
532 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
533 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
535 refresh_sequent proofw ;
539 CicTextualParser0.Eof ->
540 inputt#delete_text 0 inputlen
542 | None -> assert false (* "ERROR: No current term!!!" *)
544 RefreshSequentException e ->
545 output_html outputhtml
546 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
547 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
548 ProofEngine.proof := savedproof ;
549 ProofEngine.goal := savedgoal ;
550 refresh_sequent proofw
551 | RefreshProofException e ->
552 output_html outputhtml
553 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
554 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
555 ProofEngine.proof := savedproof ;
556 ProofEngine.goal := savedgoal ;
557 refresh_sequent proofw ;
560 output_html outputhtml
561 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
562 ProofEngine.proof := savedproof ;
563 ProofEngine.goal := savedgoal ;
566 output_html outputhtml
567 ("<h1 color=\"red\">No term selected</h1>")
570 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
571 let module L = LogicalOperations in
572 let module G = Gdome in
573 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
574 let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
575 let savedproof = !ProofEngine.proof in
576 let savedgoal = !ProofEngine.goal in
577 match mmlwidget#get_selection with
580 ((node : Gdome.element)#getAttributeNS
582 ~localName:(G.domString "xref"))#to_string
584 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
588 match !current_scratch_infos with
589 (* term is the whole goal in the scratch_area *)
590 Some (term,ids_to_terms, ids_to_father_ids,_) ->
592 let expr = tactic term (Hashtbl.find ids_to_terms id) in
593 let mml = mml_of_cic_term 111 expr in
594 scratch_window#show () ;
595 scratch_window#mmlwidget#load_tree ~dom:mml
596 | None -> assert false (* "ERROR: No current term!!!" *)
599 output_html outputhtml
600 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
603 output_html outputhtml
604 ("<h1 color=\"red\">No term selected</h1>")
607 let call_tactic_with_hypothesis_input tactic rendering_window () =
608 let module L = LogicalOperations in
609 let module G = Gdome in
610 let proofw = (rendering_window#proofw : GMathView.math_view) in
611 let output = (rendering_window#output : GMathView.math_view) in
612 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
613 let savedproof = !ProofEngine.proof in
614 let savedgoal = !ProofEngine.goal in
615 match proofw#get_selection with
618 ((node : Gdome.element)#getAttributeNS
620 ~localName:(G.domString "xref"))#to_string
622 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
626 match !current_goal_infos with
627 Some (_,_,ids_to_hypotheses) ->
629 tactic (Hashtbl.find ids_to_hypotheses id) ;
630 refresh_sequent rendering_window#proofw ;
631 refresh_proof rendering_window#output
632 | None -> assert false (* "ERROR: No current term!!!" *)
634 RefreshSequentException e ->
635 output_html outputhtml
636 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
637 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
638 ProofEngine.proof := savedproof ;
639 ProofEngine.goal := savedgoal ;
640 refresh_sequent proofw
641 | RefreshProofException e ->
642 output_html outputhtml
643 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
644 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
645 ProofEngine.proof := savedproof ;
646 ProofEngine.goal := savedgoal ;
647 refresh_sequent proofw ;
650 output_html outputhtml
651 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
652 ProofEngine.proof := savedproof ;
653 ProofEngine.goal := savedgoal ;
656 output_html outputhtml
657 ("<h1 color=\"red\">No term selected</h1>")
661 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
662 let exact rendering_window =
663 call_tactic_with_input ProofEngine.exact rendering_window
665 let apply rendering_window =
666 call_tactic_with_input ProofEngine.apply rendering_window
668 let elimintrossimpl rendering_window =
669 call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window
671 let elimtype rendering_window =
672 call_tactic_with_input ProofEngine.elim_type rendering_window
674 let whd rendering_window =
675 call_tactic_with_goal_input ProofEngine.whd rendering_window
677 let reduce rendering_window =
678 call_tactic_with_goal_input ProofEngine.reduce rendering_window
680 let simpl rendering_window =
681 call_tactic_with_goal_input ProofEngine.simpl rendering_window
683 let fold rendering_window =
684 call_tactic_with_input ProofEngine.fold rendering_window
686 let cut rendering_window =
687 call_tactic_with_input ProofEngine.cut rendering_window
689 let change rendering_window =
690 call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
692 let letin rendering_window =
693 call_tactic_with_input ProofEngine.letin rendering_window
695 let ring rendering_window = call_tactic ProofEngine.ring rendering_window;;
696 let clearbody rendering_window =
697 call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window
699 let clear rendering_window =
700 call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
702 let fourier rendering_window =
703 call_tactic ProofEngine.fourier rendering_window
705 let rewritesimpl rendering_window =
706 call_tactic_with_input ProofEngine.rewrite_simpl rendering_window
711 let whd_in_scratch scratch_window =
712 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
715 let reduce_in_scratch scratch_window =
716 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
719 let simpl_in_scratch scratch_window =
720 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
726 (**********************)
728 (**********************)
730 exception OpenConjecturesStillThere;;
731 exception WrongProof;;
733 let qed rendering_window () =
734 match !ProofEngine.proof with
736 | Some (uri,[],bo,ty) ->
738 CicReduction.are_convertible []
739 (CicTypeChecker.type_of_aux' [] [] bo) ty
742 (*CSC: Wrong: [] is just plainly wrong *)
743 let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
745 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
746 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
748 Cic2acic.acic_object_of_cic_object proof
751 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
753 (rendering_window#output : GMathView.math_view)#load_tree mml ;
756 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
761 | _ -> raise OpenConjecturesStillThere
765 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
767 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
769 let save rendering_window () =
770 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
771 match !ProofEngine.proof with
773 | Some (uri, metasenv, bo, ty) ->
775 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
777 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
778 Cic2acic.acic_object_of_cic_object currentproof
780 let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in
782 [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
784 ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
788 Xml.pp ~quiet:true xml' (Some prooffile) ;
789 output_html outputhtml
790 ("<h1 color=\"Green\">Current proof saved to " ^
794 (* Used to typecheck the loaded proofs *)
795 let typecheck_loaded_proof metasenv bo ty =
796 let module T = CicTypeChecker in
797 (*CSC: bisogna controllare anche il metasenv!!! *)
798 ignore (T.type_of_aux' metasenv [] ty) ;
799 ignore (T.type_of_aux' metasenv [] bo)
802 let load rendering_window () =
803 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
804 let output = (rendering_window#output : GMathView.math_view) in
805 let proofw = (rendering_window#proofw : GMathView.math_view) in
807 let uri = UriManager.uri_of_string "cic:/dummy.con" in
808 match CicParser.obj_of_xml prooffile uri with
809 Cic.CurrentProof (_,metasenv,bo,ty) ->
810 typecheck_loaded_proof metasenv bo ty ;
812 Some (uri, metasenv, bo, ty) ;
816 | (metano,_,_)::_ -> Some metano
818 refresh_proof output ;
819 refresh_sequent proofw ;
820 output_html outputhtml
821 ("<h1 color=\"Green\">Current proof loaded from " ^
825 RefreshSequentException e ->
826 output_html outputhtml
827 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
828 "sequent: " ^ Printexc.to_string e ^ "</h1>")
829 | RefreshProofException e ->
830 output_html outputhtml
831 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
832 "proof: " ^ Printexc.to_string e ^ "</h1>")
834 output_html outputhtml
835 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
838 let proveit rendering_window () =
839 let module L = LogicalOperations in
840 let module G = Gdome in
841 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
842 match rendering_window#output#get_selection with
845 ((node : Gdome.element)#getAttributeNS
847 ((element : G.element)#getAttributeNS
850 ~localName:(G.domString "xref"))#to_string
852 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
856 match !current_cic_infos with
857 Some (ids_to_terms, ids_to_father_ids, _, _) ->
859 L.to_sequent id ids_to_terms ids_to_father_ids ;
860 refresh_proof rendering_window#output ;
861 refresh_sequent rendering_window#proofw
862 | None -> assert false (* "ERROR: No current term!!!" *)
864 RefreshSequentException e ->
865 output_html outputhtml
866 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
867 "sequent: " ^ Printexc.to_string e ^ "</h1>")
868 | RefreshProofException e ->
869 output_html outputhtml
870 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
871 "proof: " ^ Printexc.to_string e ^ "</h1>")
873 output_html outputhtml
874 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
876 | None -> assert false (* "ERROR: No selection!!!" *)
879 let focus rendering_window () =
880 let module L = LogicalOperations in
881 let module G = Gdome in
882 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
883 match rendering_window#output#get_selection with
886 ((node : Gdome.element)#getAttributeNS
888 ((element : G.element)#getAttributeNS
891 ~localName:(G.domString "xref"))#to_string
893 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
897 match !current_cic_infos with
898 Some (ids_to_terms, ids_to_father_ids, _, _) ->
900 L.focus id ids_to_terms ids_to_father_ids ;
901 refresh_sequent rendering_window#proofw
902 | None -> assert false (* "ERROR: No current term!!!" *)
904 RefreshSequentException e ->
905 output_html outputhtml
906 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
907 "sequent: " ^ Printexc.to_string e ^ "</h1>")
908 | RefreshProofException e ->
909 output_html outputhtml
910 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
911 "proof: " ^ Printexc.to_string e ^ "</h1>")
913 output_html outputhtml
914 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
916 | None -> assert false (* "ERROR: No selection!!!" *)
919 exception NoPrevGoal;;
920 exception NoNextGoal;;
922 let prevgoal metasenv metano =
926 | [(m,_,_)] -> raise NoPrevGoal
927 | (n,_,_)::(m,_,_)::_ when m=metano -> n
933 let nextgoal metasenv metano =
937 | [(m,_,_)] when m = metano -> raise NoNextGoal
938 | (m,_,_)::(n,_,_)::_ when m=metano -> n
944 let prev_or_next_goal select_goal rendering_window () =
945 let module L = LogicalOperations in
946 let module G = Gdome in
947 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
949 match !ProofEngine.proof with
951 | Some (_,metasenv,_,_) -> metasenv
954 match !ProofEngine.goal with
959 ProofEngine.goal := Some (select_goal metasenv metano) ;
960 refresh_sequent rendering_window#proofw
962 RefreshSequentException e ->
963 output_html outputhtml
964 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
965 "sequent: " ^ Printexc.to_string e ^ "</h1>")
967 output_html outputhtml
968 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
971 exception NotADefinition;;
973 let open_ rendering_window () =
974 let inputt = (rendering_window#inputt : GEdit.text) in
975 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
976 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
977 let output = (rendering_window#output : GMathView.math_view) in
978 let proofw = (rendering_window#proofw : GMathView.math_view) in
979 let inputlen = inputt#length in
980 let input = inputt#get_chars 0 inputlen ^ "\n" in
982 let uri = UriManager.uri_of_string ("cic:" ^ input) in
983 CicTypeChecker.typecheck uri ;
985 match CicEnvironment.get_cooked_obj uri 0 with
986 Cic.Definition (_,bo,ty,_) -> [],bo,ty
987 | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
990 | Cic.InductiveDefinition _ -> raise NotADefinition
993 Some (uri, metasenv, bo, ty) ;
994 ProofEngine.goal := None ;
995 refresh_sequent proofw ;
996 refresh_proof output ;
997 inputt#delete_text 0 inputlen ;
998 ignore(oldinputt#insert_text input oldinputt#length)
1000 RefreshSequentException e ->
1001 output_html outputhtml
1002 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1003 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1004 | RefreshProofException e ->
1005 output_html outputhtml
1006 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1007 "proof: " ^ Printexc.to_string e ^ "</h1>")
1009 output_html outputhtml
1010 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1013 let state rendering_window () =
1014 let inputt = (rendering_window#inputt : GEdit.text) in
1015 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
1016 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1017 let output = (rendering_window#output : GMathView.math_view) in
1018 let proofw = (rendering_window#proofw : GMathView.math_view) in
1019 let inputlen = inputt#length in
1020 let input = inputt#get_chars 0 inputlen ^ "\n" in
1021 (* Do something interesting *)
1022 let lexbuf = Lexing.from_string input in
1025 (* Execute the actions *)
1026 match CicTextualParser.main CicTextualLexer.token lexbuf with
1029 let _ = CicTypeChecker.type_of_aux' [] [] expr in
1030 ProofEngine.proof :=
1031 Some (UriManager.uri_of_string "cic:/dummy.con",
1032 [1,[],expr], Cic.Meta (1,[]), expr) ;
1033 ProofEngine.goal := Some 1 ;
1034 refresh_sequent proofw ;
1035 refresh_proof output ;
1038 CicTextualParser0.Eof ->
1039 inputt#delete_text 0 inputlen ;
1040 ignore(oldinputt#insert_text input oldinputt#length)
1041 | RefreshSequentException e ->
1042 output_html outputhtml
1043 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1044 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1045 | RefreshProofException e ->
1046 output_html outputhtml
1047 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1048 "proof: " ^ Printexc.to_string e ^ "</h1>")
1050 output_html outputhtml
1051 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1054 let check rendering_window scratch_window () =
1055 let inputt = (rendering_window#inputt : GEdit.text) in
1056 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1057 let output = (rendering_window#output : GMathView.math_view) in
1058 let proofw = (rendering_window#proofw : GMathView.math_view) in
1059 let inputlen = inputt#length in
1060 let input = inputt#get_chars 0 inputlen ^ "\n" in
1062 match !ProofEngine.proof with
1063 None -> UriManager.uri_of_string "cic:/dummy.con", []
1064 | Some (curi,metasenv,_,_) -> curi,metasenv
1066 let context,names_context =
1068 match !ProofEngine.goal with
1071 let (_,canonical_context,_) =
1072 List.find (function (m,_,_) -> m=metano) metasenv
1079 Some (n,_) -> Some n
1083 (* Do something interesting *)
1084 let lexbuf = Lexing.from_string input in
1087 (* Execute the actions *)
1089 CicTextualParserContext.main curi names_context metasenv
1090 CicTextualLexer.token lexbuf
1093 | Some (metasenv',expr) ->
1095 let ty = CicTypeChecker.type_of_aux' metasenv' context expr in
1096 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1097 scratch_window#show () ;
1098 scratch_window#mmlwidget#load_tree ~dom:mml
1101 print_endline ("? " ^ CicPp.ppterm expr) ;
1105 CicTextualParser0.Eof -> ()
1107 output_html outputhtml
1108 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1111 exception NoObjectsLocated;;
1113 let user_uri_choice uris =
1116 [] -> raise NoObjectsLocated
1120 GToolbox.question_box ~title:"Ambiguous result."
1121 ~buttons:uris ~default:1
1122 "Ambiguous result. Please, choose one."
1124 List.nth uris (choice-1)
1126 String.sub uri 4 (String.length uri - 4)
1129 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
1130 let get_last_query =
1131 let query = ref "" in
1132 MQueryGenerator.set_confirm_query
1133 (function q -> query := MQueryUtil.text_of_query q ; true) ;
1134 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
1137 let locate rendering_window () =
1138 let inputt = (rendering_window#inputt : GEdit.text) in
1139 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1140 let inputlen = inputt#length in
1141 let input = inputt#get_chars 0 inputlen in
1143 match Str.split (Str.regexp "[ \t]+") input with
1146 inputt#delete_text 0 inputlen ;
1147 let result = MQueryGenerator.locate head in
1150 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1152 let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1153 output_html outputhtml html ;
1154 let uri' = user_uri_choice uris in
1155 ignore ((inputt#insert_text uri') ~pos:0)
1158 output_html outputhtml
1159 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1162 let backward rendering_window () =
1163 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1164 let inputt = (rendering_window#inputt : GEdit.text) in
1165 let inputlen = inputt#length in
1166 let input = inputt#get_chars 0 inputlen in
1167 let level = int_of_string input in
1169 match !ProofEngine.proof with
1170 None -> assert false
1171 | Some (_,metasenv,_,_) -> metasenv
1174 match !ProofEngine.goal with
1177 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1178 let result = MQueryGenerator.backward metasenv ey ty level in
1181 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1184 " <h1>Backward Query: </h1>" ^
1185 " <h2>Levels: </h2> " ^
1186 MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1187 " <pre>" ^ get_last_query result ^ "</pre>" in
1188 output_html outputhtml html ;
1189 let uri' = user_uri_choice uris in
1190 inputt#delete_text 0 inputlen ;
1191 ignore ((inputt#insert_text uri') ~pos:0)
1194 output_html outputhtml
1195 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1198 let choose_selection
1199 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1201 let module G = Gdome in
1202 let rec aux element =
1203 if element#hasAttributeNS
1204 ~namespaceURI:helmns
1205 ~localName:(G.domString "xref")
1207 mmlwidget#set_selection (Some element)
1209 match element#get_parentNode with
1210 None -> assert false
1211 (*CSC: OCAML DIVERGES!
1212 | Some p -> aux (new G.element_of_node p)
1214 | Some p -> aux (new Gdome.element_of_node p)
1218 | None -> mmlwidget#set_selection None
1221 (* STUFF TO BUILD THE GTK INTERFACE *)
1223 (* Stuff for the widget settings *)
1225 let export_to_postscript (output : GMathView.math_view) () =
1226 output#export_to_postscript ~filename:"output.ps" ();
1229 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1230 button_set_kerning button_set_transparency button_export_to_postscript
1233 let is_set = button_t1#active in
1234 output#set_font_manager_type
1235 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1238 button_set_anti_aliasing#misc#set_sensitive true ;
1239 button_set_kerning#misc#set_sensitive true ;
1240 button_set_transparency#misc#set_sensitive true ;
1241 button_export_to_postscript#misc#set_sensitive true ;
1245 button_set_anti_aliasing#misc#set_sensitive false ;
1246 button_set_kerning#misc#set_sensitive false ;
1247 button_set_transparency#misc#set_sensitive false ;
1248 button_export_to_postscript#misc#set_sensitive false ;
1252 let set_anti_aliasing output button_set_anti_aliasing () =
1253 output#set_anti_aliasing button_set_anti_aliasing#active
1256 let set_kerning output button_set_kerning () =
1257 output#set_kerning button_set_kerning#active
1260 let set_transparency output button_set_transparency () =
1261 output#set_transparency button_set_transparency#active
1264 let changefont output font_size_spinb () =
1265 output#set_font_size font_size_spinb#value_as_int
1268 let set_log_verbosity output log_verbosity_spinb () =
1269 output#set_log_verbosity log_verbosity_spinb#value_as_int
1272 class settings_window (output : GMathView.math_view) sw
1273 button_export_to_postscript selection_changed_callback
1275 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1277 GPack.vbox ~packing:settings_window#add () in
1280 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1281 ~border_width:5 ~packing:vbox#add () in
1283 GButton.toggle_button ~label:"activate t1 fonts"
1284 ~packing:(table#attach ~left:0 ~top:0) () in
1285 let button_set_anti_aliasing =
1286 GButton.toggle_button ~label:"set_anti_aliasing"
1287 ~packing:(table#attach ~left:0 ~top:1) () in
1288 let button_set_kerning =
1289 GButton.toggle_button ~label:"set_kerning"
1290 ~packing:(table#attach ~left:1 ~top:1) () in
1291 let button_set_transparency =
1292 GButton.toggle_button ~label:"set_transparency"
1293 ~packing:(table#attach ~left:2 ~top:1) () in
1296 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1297 ~border_width:5 ~packing:vbox#add () in
1298 let font_size_label =
1299 GMisc.label ~text:"font size:"
1300 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1301 let font_size_spinb =
1303 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1306 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1307 let log_verbosity_label =
1308 GMisc.label ~text:"log verbosity:"
1309 ~packing:(table#attach ~left:0 ~top:1) () in
1310 let log_verbosity_spinb =
1312 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1315 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1317 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1319 GButton.button ~label:"Close"
1320 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1322 method show = settings_window#show
1324 button_set_anti_aliasing#misc#set_sensitive false ;
1325 button_set_kerning#misc#set_sensitive false ;
1326 button_set_transparency#misc#set_sensitive false ;
1327 (* Signals connection *)
1328 ignore(button_t1#connect#clicked
1329 (activate_t1 output button_set_anti_aliasing button_set_kerning
1330 button_set_transparency button_export_to_postscript button_t1)) ;
1331 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1332 ignore(button_set_anti_aliasing#connect#toggled
1333 (set_anti_aliasing output button_set_anti_aliasing));
1334 ignore(button_set_kerning#connect#toggled
1335 (set_kerning output button_set_kerning)) ;
1336 ignore(button_set_transparency#connect#toggled
1337 (set_transparency output button_set_transparency)) ;
1338 ignore(log_verbosity_spinb#connect#changed
1339 (set_log_verbosity output log_verbosity_spinb)) ;
1340 ignore(closeb#connect#clicked settings_window#misc#hide)
1343 (* Scratch window *)
1345 class scratch_window outputhtml =
1347 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1349 GPack.vbox ~packing:window#add () in
1351 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1353 GButton.button ~label:"Whd"
1354 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1356 GButton.button ~label:"Reduce"
1357 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1359 GButton.button ~label:"Simpl"
1360 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1361 let scrolled_window =
1362 GBin.scrolled_window ~border_width:10
1363 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1366 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1368 method outputhtml = outputhtml
1369 method mmlwidget = mmlwidget
1370 method show () = window#misc#hide () ; window#show ()
1372 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1373 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1374 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1375 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1376 ignore(simplb#connect#clicked (simpl_in_scratch self))
1381 class rendering_window output proofw (label : GMisc.label) =
1383 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1385 GPack.hbox ~packing:window#add () in
1387 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1388 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1389 let scrolled_window0 =
1390 GBin.scrolled_window ~border_width:10
1391 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1392 let _ = scrolled_window0#add output#coerce in
1394 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1396 GButton.button ~label:"Settings"
1397 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1398 let button_export_to_postscript =
1399 GButton.button ~label:"export_to_postscript"
1400 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1402 GButton.button ~label:"Qed"
1403 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1405 GButton.button ~label:"Save"
1406 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1408 GButton.button ~label:"Load"
1409 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1411 GButton.button ~label:"Close"
1412 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1414 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1416 GButton.button ~label:"Prove It"
1417 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1419 GButton.button ~label:"Focus"
1420 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1422 GButton.button ~label:"<"
1423 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1425 GButton.button ~label:">"
1426 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1427 let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1428 ~packing:(vbox#pack ~padding:5) () in
1430 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1432 GButton.button ~label:"State"
1433 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1435 GButton.button ~label:"Open"
1436 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1438 GButton.button ~label:"Check"
1439 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1441 GButton.button ~label:"Locate"
1442 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1444 GButton.button ~label:"Backward"
1445 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1446 let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1447 ~packing:(vbox#pack ~padding:5) () in
1449 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1450 let scrolled_window1 =
1451 GBin.scrolled_window ~border_width:10
1452 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1453 let _ = scrolled_window1#add proofw#coerce in
1455 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1457 GButton.button ~label:"Exact"
1458 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1460 GButton.button ~label:"Intros"
1461 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1463 GButton.button ~label:"Apply"
1464 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1465 let elimintrossimplb =
1466 GButton.button ~label:"ElimIntrosSimpl"
1467 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1469 GButton.button ~label:"ElimType"
1470 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1472 GButton.button ~label:"Whd"
1473 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1475 GButton.button ~label:"Reduce"
1476 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1478 GButton.button ~label:"Simpl"
1479 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1481 GButton.button ~label:"Fold"
1482 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1484 GButton.button ~label:"Cut"
1485 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1487 GButton.button ~label:"Change"
1488 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1490 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1492 GButton.button ~label:"Let ... In"
1493 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1495 GButton.button ~label:"Ring"
1496 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1498 GButton.button ~label:"ClearBody"
1499 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1501 GButton.button ~label:"Clear"
1502 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1504 GButton.button ~label:"Fourier"
1505 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1507 GButton.button ~label:"RewriteSimpl ->"
1508 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1511 ~source:"<html><body bgColor=\"white\"></body></html>"
1512 ~width:400 ~height: 200
1513 ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1515 let scratch_window = new scratch_window outputhtml in
1517 method outputhtml = outputhtml
1518 method oldinputt = oldinputt
1519 method inputt = inputt
1520 method output = (output : GMathView.math_view)
1521 method proofw = (proofw : GMathView.math_view)
1522 method show = window#show
1524 button_export_to_postscript#misc#set_sensitive false ;
1526 (* signal handlers here *)
1527 ignore(output#connect#selection_changed
1528 (function elem -> proofw#unload ; choose_selection output elem)) ;
1529 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1530 ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1531 let settings_window = new settings_window output scrolled_window0
1532 button_export_to_postscript (choose_selection output) in
1533 ignore(settingsb#connect#clicked settings_window#show) ;
1534 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1535 ignore(qedb#connect#clicked (qed self)) ;
1536 ignore(saveb#connect#clicked (save self)) ;
1537 ignore(loadb#connect#clicked (load self)) ;
1538 ignore(proveitb#connect#clicked (proveit self)) ;
1539 ignore(focusb#connect#clicked (focus self)) ;
1540 ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ;
1541 ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ;
1542 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1543 ignore(stateb#connect#clicked (state self)) ;
1544 ignore(openb#connect#clicked (open_ self)) ;
1545 ignore(checkb#connect#clicked (check self scratch_window)) ;
1546 ignore(locateb#connect#clicked (locate self)) ;
1547 ignore(backwardb#connect#clicked (backward self)) ;
1548 ignore(exactb#connect#clicked (exact self)) ;
1549 ignore(applyb#connect#clicked (apply self)) ;
1550 ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
1551 ignore(elimtypeb#connect#clicked (elimtype self)) ;
1552 ignore(whdb#connect#clicked (whd self)) ;
1553 ignore(reduceb#connect#clicked (reduce self)) ;
1554 ignore(simplb#connect#clicked (simpl self)) ;
1555 ignore(foldb#connect#clicked (fold self)) ;
1556 ignore(cutb#connect#clicked (cut self)) ;
1557 ignore(changeb#connect#clicked (change self)) ;
1558 ignore(letinb#connect#clicked (letin self)) ;
1559 ignore(ringb#connect#clicked (ring self)) ;
1560 ignore(clearbodyb#connect#clicked (clearbody self)) ;
1561 ignore(clearb#connect#clicked (clear self)) ;
1562 ignore(fourierb#connect#clicked (fourier self)) ;
1563 ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ;
1564 ignore(introsb#connect#clicked (intros self)) ;
1565 Logger.log_callback :=
1566 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1571 let rendering_window = ref None;;
1573 let initialize_everything () =
1574 let module U = Unix in
1575 let output = GMathView.math_view ~width:350 ~height:280 ()
1576 and proofw = GMathView.math_view ~width:400 ~height:275 ()
1577 and label = GMisc.label ~text:"gTopLevel" () in
1578 let rendering_window' =
1579 new rendering_window output proofw label
1581 rendering_window := Some rendering_window' ;
1582 rendering_window'#show () ;
1587 CicCooking.init () ;
1590 Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ;
1591 CicTextualParser0.set_locate_object
1593 let result = MQueryGenerator.locate id in
1596 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1598 let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1600 match !rendering_window with
1601 None -> assert false
1602 | Some rw -> output_html rw#outputhtml html ;
1608 (GToolbox.input_string ~title:"Unknown input"
1609 ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
1612 | Some uri -> Some ("cic:" ^ uri)
1617 GToolbox.question_box ~title:"Ambiguous input."
1618 ~buttons:uris ~default:1 "Ambiguous input. Please, choose one."
1621 Some (List.nth uris (choice - 1))
1623 (* No choice from the user *)
1629 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
1630 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1631 Some (Cic.Const (UriManager.uri_of_string uri',0))
1634 (* Inductive Type *)
1635 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
1636 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1637 Some (Cic.MutInd (uri'',0,typeno))
1640 (* Constructor of an Inductive Type *)
1641 let uri'',typeno,consno =
1642 CicTextualLexer.indconuri_of_uri uri'
1644 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1645 Some (Cic.MutConstruct (uri'',0,typeno,consno))
1650 ignore (GtkMain.Main.init ()) ;
1651 initialize_everything () ;
1652 if !usedb then Mqint.close ();