1 (* Copyright (C) 2000-2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
36 (* GLOBAL CONSTANTS *)
38 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
42 " <body bgColor=\"white\">"
50 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
51 (*CSC: the getter should handle the innertypes, not the FS *)
52 let innertypesfile = "/home/tassi/miohelm/tmp/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
684 let fourier rendering_window =
685 call_tactic ProofEngine.fourier rendering_window
687 let rewritesimpl rendering_window =
688 call_tactic_with_input ProofEngine.rewrite_simpl rendering_window
693 let whd_in_scratch scratch_window =
694 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
697 let reduce_in_scratch scratch_window =
698 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
701 let simpl_in_scratch scratch_window =
702 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
708 (**********************)
710 (**********************)
712 exception OpenConjecturesStillThere;;
713 exception WrongProof;;
715 let qed rendering_window () =
716 match !ProofEngine.proof with
718 | Some (uri,[],bo,ty) ->
720 CicReduction.are_convertible []
721 (CicTypeChecker.type_of_aux' [] [] bo) ty
724 (*CSC: Wrong: [] is just plainly wrong *)
725 let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
727 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
728 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
730 Cic2acic.acic_object_of_cic_object proof
733 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
735 (rendering_window#output : GMathView.math_view)#load_tree mml ;
738 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
743 | _ -> raise OpenConjecturesStillThere
747 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
749 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
751 let save rendering_window () =
752 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
753 match !ProofEngine.proof with
755 | Some (uri, metasenv, bo, ty) ->
757 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
759 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
760 Cic2acic.acic_object_of_cic_object currentproof
762 let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in
764 [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
766 ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
770 Xml.pp ~quiet:true xml' (Some prooffile) ;
771 output_html outputhtml
772 ("<h1 color=\"Green\">Current proof saved to " ^
776 (* Used to typecheck the loaded proofs *)
777 let typecheck_loaded_proof metasenv bo ty =
778 let module T = CicTypeChecker in
779 (*CSC: bisogna controllare anche il metasenv!!! *)
780 ignore (T.type_of_aux' metasenv [] ty) ;
781 ignore (T.type_of_aux' metasenv [] bo)
784 let load rendering_window () =
785 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
786 let output = (rendering_window#output : GMathView.math_view) in
787 let proofw = (rendering_window#proofw : GMathView.math_view) in
789 let uri = UriManager.uri_of_string "cic:/dummy.con" in
790 match CicParser.obj_of_xml prooffile uri with
791 Cic.CurrentProof (_,metasenv,bo,ty) ->
792 typecheck_loaded_proof metasenv bo ty ;
794 Some (uri, metasenv, bo, ty) ;
798 | (metano,_,_)::_ -> Some metano
800 refresh_proof output ;
801 refresh_sequent proofw ;
802 output_html outputhtml
803 ("<h1 color=\"Green\">Current proof loaded from " ^
807 RefreshSequentException e ->
808 output_html outputhtml
809 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
810 "sequent: " ^ Printexc.to_string e ^ "</h1>")
811 | RefreshProofException e ->
812 output_html outputhtml
813 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
814 "proof: " ^ Printexc.to_string e ^ "</h1>")
816 output_html outputhtml
817 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
820 let proveit rendering_window () =
821 let module L = LogicalOperations in
822 let module G = Gdome in
823 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
824 match rendering_window#output#get_selection with
827 ((node : Gdome.element)#getAttributeNS
829 ((element : G.element)#getAttributeNS
832 ~localName:(G.domString "xref"))#to_string
834 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
838 match !current_cic_infos with
839 Some (ids_to_terms, ids_to_father_ids, _, _) ->
841 L.to_sequent id ids_to_terms ids_to_father_ids ;
842 refresh_proof rendering_window#output ;
843 refresh_sequent rendering_window#proofw
844 | None -> assert false (* "ERROR: No current term!!!" *)
846 RefreshSequentException e ->
847 output_html outputhtml
848 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
849 "sequent: " ^ Printexc.to_string e ^ "</h1>")
850 | RefreshProofException e ->
851 output_html outputhtml
852 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
853 "proof: " ^ Printexc.to_string e ^ "</h1>")
855 output_html outputhtml
856 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
858 | None -> assert false (* "ERROR: No selection!!!" *)
861 let focus rendering_window () =
862 let module L = LogicalOperations in
863 let module G = Gdome in
864 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
865 match rendering_window#output#get_selection with
868 ((node : Gdome.element)#getAttributeNS
870 ((element : G.element)#getAttributeNS
873 ~localName:(G.domString "xref"))#to_string
875 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
879 match !current_cic_infos with
880 Some (ids_to_terms, ids_to_father_ids, _, _) ->
882 L.focus id ids_to_terms ids_to_father_ids ;
883 refresh_sequent rendering_window#proofw
884 | None -> assert false (* "ERROR: No current term!!!" *)
886 RefreshSequentException e ->
887 output_html outputhtml
888 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
889 "sequent: " ^ Printexc.to_string e ^ "</h1>")
890 | RefreshProofException e ->
891 output_html outputhtml
892 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
893 "proof: " ^ Printexc.to_string e ^ "</h1>")
895 output_html outputhtml
896 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
898 | None -> assert false (* "ERROR: No selection!!!" *)
901 exception NoPrevGoal;;
902 exception NoNextGoal;;
904 let prevgoal metasenv metano =
908 | [(m,_,_)] -> raise NoPrevGoal
909 | (n,_,_)::(m,_,_)::_ when m=metano -> n
915 let nextgoal metasenv metano =
919 | [(m,_,_)] when m = metano -> raise NoNextGoal
920 | (m,_,_)::(n,_,_)::_ when m=metano -> n
926 let prev_or_next_goal select_goal rendering_window () =
927 let module L = LogicalOperations in
928 let module G = Gdome in
929 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
931 match !ProofEngine.proof with
933 | Some (_,metasenv,_,_) -> metasenv
936 match !ProofEngine.goal with
941 ProofEngine.goal := Some (select_goal metasenv metano) ;
942 refresh_sequent rendering_window#proofw
944 RefreshSequentException e ->
945 output_html outputhtml
946 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
947 "sequent: " ^ Printexc.to_string e ^ "</h1>")
949 output_html outputhtml
950 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
953 exception NotADefinition;;
955 let open_ rendering_window () =
956 let inputt = (rendering_window#inputt : GEdit.text) in
957 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
958 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
959 let output = (rendering_window#output : GMathView.math_view) in
960 let proofw = (rendering_window#proofw : GMathView.math_view) in
961 let inputlen = inputt#length in
962 let input = inputt#get_chars 0 inputlen ^ "\n" in
964 let uri = UriManager.uri_of_string ("cic:" ^ input) in
965 CicTypeChecker.typecheck uri ;
967 match CicEnvironment.get_cooked_obj uri 0 with
968 Cic.Definition (_,bo,ty,_) -> [],bo,ty
969 | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
972 | Cic.InductiveDefinition _ -> raise NotADefinition
975 Some (uri, metasenv, bo, ty) ;
976 ProofEngine.goal := None ;
977 refresh_sequent proofw ;
978 refresh_proof output ;
979 inputt#delete_text 0 inputlen ;
980 ignore(oldinputt#insert_text input oldinputt#length)
982 RefreshSequentException e ->
983 output_html outputhtml
984 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
985 "sequent: " ^ Printexc.to_string e ^ "</h1>")
986 | RefreshProofException e ->
987 output_html outputhtml
988 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
989 "proof: " ^ Printexc.to_string e ^ "</h1>")
991 output_html outputhtml
992 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
995 let state rendering_window () =
996 let inputt = (rendering_window#inputt : GEdit.text) in
997 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
998 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
999 let output = (rendering_window#output : GMathView.math_view) in
1000 let proofw = (rendering_window#proofw : GMathView.math_view) in
1001 let inputlen = inputt#length in
1002 let input = inputt#get_chars 0 inputlen ^ "\n" in
1003 (* Do something interesting *)
1004 let lexbuf = Lexing.from_string input in
1007 (* Execute the actions *)
1008 match CicTextualParser.main CicTextualLexer.token lexbuf with
1011 let _ = CicTypeChecker.type_of_aux' [] [] expr in
1012 ProofEngine.proof :=
1013 Some (UriManager.uri_of_string "cic:/dummy.con",
1014 [1,[],expr], Cic.Meta (1,[]), expr) ;
1015 ProofEngine.goal := Some 1 ;
1016 refresh_sequent proofw ;
1017 refresh_proof output ;
1020 CicTextualParser0.Eof ->
1021 inputt#delete_text 0 inputlen ;
1022 ignore(oldinputt#insert_text input oldinputt#length)
1023 | RefreshSequentException e ->
1024 output_html outputhtml
1025 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1026 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1027 | RefreshProofException e ->
1028 output_html outputhtml
1029 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1030 "proof: " ^ Printexc.to_string e ^ "</h1>")
1032 output_html outputhtml
1033 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1036 let check rendering_window scratch_window () =
1037 let inputt = (rendering_window#inputt : GEdit.text) in
1038 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1039 let output = (rendering_window#output : GMathView.math_view) in
1040 let proofw = (rendering_window#proofw : GMathView.math_view) in
1041 let inputlen = inputt#length in
1042 let input = inputt#get_chars 0 inputlen ^ "\n" in
1044 match !ProofEngine.proof with
1045 None -> UriManager.uri_of_string "cic:/dummy.con", []
1046 | Some (curi,metasenv,_,_) -> curi,metasenv
1048 let context,names_context =
1050 match !ProofEngine.goal with
1053 let (_,canonical_context,_) =
1054 List.find (function (m,_,_) -> m=metano) metasenv
1061 Some (n,_) -> Some n
1065 (* Do something interesting *)
1066 let lexbuf = Lexing.from_string input in
1069 (* Execute the actions *)
1071 CicTextualParserContext.main curi names_context metasenv
1072 CicTextualLexer.token lexbuf
1075 | Some (metasenv',expr) ->
1077 let ty = CicTypeChecker.type_of_aux' metasenv' context expr in
1078 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1079 scratch_window#show () ;
1080 scratch_window#mmlwidget#load_tree ~dom:mml
1083 print_endline ("? " ^ CicPp.ppterm expr) ;
1087 CicTextualParser0.Eof -> ()
1089 output_html outputhtml
1090 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1093 exception NoObjectsLocated;;
1095 let user_uri_choice uris =
1098 [] -> raise NoObjectsLocated
1102 GToolbox.question_box ~title:"Ambiguous result."
1103 ~buttons:uris ~default:1
1104 "Ambiguous result. Please, choose one."
1106 List.nth uris (choice-1)
1108 String.sub uri 4 (String.length uri - 4)
1111 let locate rendering_window () =
1112 let inputt = (rendering_window#inputt : GEdit.text) in
1113 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1114 let inputlen = inputt#length in
1115 let input = inputt#get_chars 0 inputlen in
1117 match Str.split (Str.regexp "[ \t]+") input with
1120 inputt#delete_text 0 inputlen ;
1121 let MathQL.MQRefs uris, html = MQueryGenerator.locate head in
1122 output_html outputhtml html ;
1123 let uri' = user_uri_choice uris in
1124 ignore ((inputt#insert_text uri') ~pos:0)
1127 output_html outputhtml
1128 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1131 let backward rendering_window () =
1132 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1133 let inputt = (rendering_window#inputt : GEdit.text) in
1134 let inputlen = inputt#length in
1135 let input = inputt#get_chars 0 inputlen in
1136 let level = int_of_string input in
1138 match !ProofEngine.proof with
1139 None -> assert false
1140 | Some (_,metasenv,_,_) -> metasenv
1143 match !ProofEngine.goal with
1146 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1147 let MathQL.MQRefs uris, html =
1148 MQueryGenerator.backward metasenv ey ty level
1150 output_html outputhtml html ;
1151 let uri' = user_uri_choice uris in
1152 inputt#delete_text 0 inputlen ;
1153 ignore ((inputt#insert_text uri') ~pos:0)
1156 output_html outputhtml
1157 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1160 let choose_selection
1161 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1163 let module G = Gdome in
1164 let rec aux element =
1165 if element#hasAttributeNS
1166 ~namespaceURI:helmns
1167 ~localName:(G.domString "xref")
1169 mmlwidget#set_selection (Some element)
1171 match element#get_parentNode with
1172 None -> assert false
1173 (*CSC: OCAML DIVERGES!
1174 | Some p -> aux (new G.element_of_node p)
1176 | Some p -> aux (new Gdome.element_of_node p)
1180 | None -> mmlwidget#set_selection None
1183 (* STUFF TO BUILD THE GTK INTERFACE *)
1185 (* Stuff for the widget settings *)
1187 let export_to_postscript (output : GMathView.math_view) () =
1188 output#export_to_postscript ~filename:"output.ps" ();
1191 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1192 button_set_kerning button_set_transparency button_export_to_postscript
1195 let is_set = button_t1#active in
1196 output#set_font_manager_type
1197 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1200 button_set_anti_aliasing#misc#set_sensitive true ;
1201 button_set_kerning#misc#set_sensitive true ;
1202 button_set_transparency#misc#set_sensitive true ;
1203 button_export_to_postscript#misc#set_sensitive true ;
1207 button_set_anti_aliasing#misc#set_sensitive false ;
1208 button_set_kerning#misc#set_sensitive false ;
1209 button_set_transparency#misc#set_sensitive false ;
1210 button_export_to_postscript#misc#set_sensitive false ;
1214 let set_anti_aliasing output button_set_anti_aliasing () =
1215 output#set_anti_aliasing button_set_anti_aliasing#active
1218 let set_kerning output button_set_kerning () =
1219 output#set_kerning button_set_kerning#active
1222 let set_transparency output button_set_transparency () =
1223 output#set_transparency button_set_transparency#active
1226 let changefont output font_size_spinb () =
1227 output#set_font_size font_size_spinb#value_as_int
1230 let set_log_verbosity output log_verbosity_spinb () =
1231 output#set_log_verbosity log_verbosity_spinb#value_as_int
1234 class settings_window (output : GMathView.math_view) sw
1235 button_export_to_postscript selection_changed_callback
1237 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1239 GPack.vbox ~packing:settings_window#add () in
1242 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1243 ~border_width:5 ~packing:vbox#add () in
1245 GButton.toggle_button ~label:"activate t1 fonts"
1246 ~packing:(table#attach ~left:0 ~top:0) () in
1247 let button_set_anti_aliasing =
1248 GButton.toggle_button ~label:"set_anti_aliasing"
1249 ~packing:(table#attach ~left:0 ~top:1) () in
1250 let button_set_kerning =
1251 GButton.toggle_button ~label:"set_kerning"
1252 ~packing:(table#attach ~left:1 ~top:1) () in
1253 let button_set_transparency =
1254 GButton.toggle_button ~label:"set_transparency"
1255 ~packing:(table#attach ~left:2 ~top:1) () in
1258 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1259 ~border_width:5 ~packing:vbox#add () in
1260 let font_size_label =
1261 GMisc.label ~text:"font size:"
1262 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1263 let font_size_spinb =
1265 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1268 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1269 let log_verbosity_label =
1270 GMisc.label ~text:"log verbosity:"
1271 ~packing:(table#attach ~left:0 ~top:1) () in
1272 let log_verbosity_spinb =
1274 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1277 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1279 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1281 GButton.button ~label:"Close"
1282 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1284 method show = settings_window#show
1286 button_set_anti_aliasing#misc#set_sensitive false ;
1287 button_set_kerning#misc#set_sensitive false ;
1288 button_set_transparency#misc#set_sensitive false ;
1289 (* Signals connection *)
1290 ignore(button_t1#connect#clicked
1291 (activate_t1 output button_set_anti_aliasing button_set_kerning
1292 button_set_transparency button_export_to_postscript button_t1)) ;
1293 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1294 ignore(button_set_anti_aliasing#connect#toggled
1295 (set_anti_aliasing output button_set_anti_aliasing));
1296 ignore(button_set_kerning#connect#toggled
1297 (set_kerning output button_set_kerning)) ;
1298 ignore(button_set_transparency#connect#toggled
1299 (set_transparency output button_set_transparency)) ;
1300 ignore(log_verbosity_spinb#connect#changed
1301 (set_log_verbosity output log_verbosity_spinb)) ;
1302 ignore(closeb#connect#clicked settings_window#misc#hide)
1305 (* Scratch window *)
1307 class scratch_window outputhtml =
1309 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1311 GPack.vbox ~packing:window#add () in
1313 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1315 GButton.button ~label:"Whd"
1316 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1318 GButton.button ~label:"Reduce"
1319 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1321 GButton.button ~label:"Simpl"
1322 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1323 let scrolled_window =
1324 GBin.scrolled_window ~border_width:10
1325 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1328 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1330 method outputhtml = outputhtml
1331 method mmlwidget = mmlwidget
1332 method show () = window#misc#hide () ; window#show ()
1334 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1335 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1336 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1337 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1338 ignore(simplb#connect#clicked (simpl_in_scratch self))
1343 class rendering_window output proofw (label : GMisc.label) =
1345 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1347 GPack.hbox ~packing:window#add () in
1349 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1350 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1351 let scrolled_window0 =
1352 GBin.scrolled_window ~border_width:10
1353 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1354 let _ = scrolled_window0#add output#coerce in
1356 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1358 GButton.button ~label:"Settings"
1359 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1360 let button_export_to_postscript =
1361 GButton.button ~label:"export_to_postscript"
1362 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1364 GButton.button ~label:"Qed"
1365 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1367 GButton.button ~label:"Save"
1368 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1370 GButton.button ~label:"Load"
1371 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1373 GButton.button ~label:"Close"
1374 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1376 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1378 GButton.button ~label:"Prove It"
1379 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1381 GButton.button ~label:"Focus"
1382 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1384 GButton.button ~label:"<"
1385 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1387 GButton.button ~label:">"
1388 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1389 let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1390 ~packing:(vbox#pack ~padding:5) () in
1392 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1394 GButton.button ~label:"State"
1395 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1397 GButton.button ~label:"Open"
1398 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1400 GButton.button ~label:"Check"
1401 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1403 GButton.button ~label:"Locate"
1404 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1406 GButton.button ~label:"Backward"
1407 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1408 let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1409 ~packing:(vbox#pack ~padding:5) () in
1411 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1412 let scrolled_window1 =
1413 GBin.scrolled_window ~border_width:10
1414 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1415 let _ = scrolled_window1#add proofw#coerce in
1417 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1419 GButton.button ~label:"Exact"
1420 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1422 GButton.button ~label:"Intros"
1423 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1425 GButton.button ~label:"Apply"
1426 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1427 let elimintrossimplb =
1428 GButton.button ~label:"ElimIntrosSimpl"
1429 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1431 GButton.button ~label:"ElimType"
1432 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1434 GButton.button ~label:"Whd"
1435 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1437 GButton.button ~label:"Reduce"
1438 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1440 GButton.button ~label:"Simpl"
1441 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1443 GButton.button ~label:"Fold"
1444 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1446 GButton.button ~label:"Cut"
1447 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1449 GButton.button ~label:"Change"
1450 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1452 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1454 GButton.button ~label:"Let ... In"
1455 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1457 GButton.button ~label:"Ring"
1458 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1460 GButton.button ~label:"ClearBody"
1461 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1463 GButton.button ~label:"Clear"
1464 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1466 GButton.button ~label:"Fourier"
1467 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1469 GButton.button ~label:"RewriteSimpl ->"
1470 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1473 ~source:"<html><body bgColor=\"white\"></body></html>"
1474 ~width:400 ~height: 200
1475 ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1477 let scratch_window = new scratch_window outputhtml in
1479 method outputhtml = outputhtml
1480 method oldinputt = oldinputt
1481 method inputt = inputt
1482 method output = (output : GMathView.math_view)
1483 method proofw = (proofw : GMathView.math_view)
1484 method show = window#show
1486 button_export_to_postscript#misc#set_sensitive false ;
1488 (* signal handlers here *)
1489 ignore(output#connect#selection_changed
1490 (function elem -> proofw#unload ; choose_selection output elem)) ;
1491 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1492 ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1493 let settings_window = new settings_window output scrolled_window0
1494 button_export_to_postscript (choose_selection output) in
1495 ignore(settingsb#connect#clicked settings_window#show) ;
1496 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1497 ignore(qedb#connect#clicked (qed self)) ;
1498 ignore(saveb#connect#clicked (save self)) ;
1499 ignore(loadb#connect#clicked (load self)) ;
1500 ignore(proveitb#connect#clicked (proveit self)) ;
1501 ignore(focusb#connect#clicked (focus self)) ;
1502 ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ;
1503 ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ;
1504 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1505 ignore(stateb#connect#clicked (state self)) ;
1506 ignore(openb#connect#clicked (open_ self)) ;
1507 ignore(checkb#connect#clicked (check self scratch_window)) ;
1508 ignore(locateb#connect#clicked (locate self)) ;
1509 ignore(backwardb#connect#clicked (backward self)) ;
1510 ignore(exactb#connect#clicked (exact self)) ;
1511 ignore(applyb#connect#clicked (apply self)) ;
1512 ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
1513 ignore(elimtypeb#connect#clicked (elimtype self)) ;
1514 ignore(whdb#connect#clicked (whd self)) ;
1515 ignore(reduceb#connect#clicked (reduce self)) ;
1516 ignore(simplb#connect#clicked (simpl self)) ;
1517 ignore(foldb#connect#clicked (fold self)) ;
1518 ignore(cutb#connect#clicked (cut self)) ;
1519 ignore(changeb#connect#clicked (change self)) ;
1520 ignore(letinb#connect#clicked (letin self)) ;
1521 ignore(ringb#connect#clicked (ring self)) ;
1522 ignore(clearbodyb#connect#clicked (clearbody self)) ;
1523 ignore(clearb#connect#clicked (clear self)) ;
1524 ignore(fourierb#connect#clicked (fourier self)) ;
1525 ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ;
1526 ignore(introsb#connect#clicked (intros self)) ;
1527 Logger.log_callback :=
1528 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1533 let rendering_window = ref None;;
1535 let initialize_everything () =
1536 let module U = Unix in
1537 let output = GMathView.math_view ~width:350 ~height:280 ()
1538 and proofw = GMathView.math_view ~width:400 ~height:275 ()
1539 and label = GMisc.label ~text:"gTopLevel" () in
1540 let rendering_window' =
1541 new rendering_window output proofw label
1543 rendering_window := Some rendering_window' ;
1544 rendering_window'#show () ;
1549 CicCooking.init () ;
1552 MQueryGenerator.init () ;
1553 CicTextualParser0.set_locate_object
1555 let MathQL.MQRefs uris, html = MQueryGenerator.locate id in
1557 match !rendering_window with
1558 None -> assert false
1559 | Some rw -> output_html rw#outputhtml html ;
1565 (GToolbox.input_string ~title:"Unknown input"
1566 ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
1569 | Some uri -> Some ("cic:" ^ uri)
1574 GToolbox.question_box ~title:"Ambiguous input."
1575 ~buttons:uris ~default:1 "Ambiguous input. Please, choose one."
1578 Some (List.nth uris (choice - 1))
1580 (* No choice from the user *)
1586 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
1587 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1588 Some (Cic.Const (UriManager.uri_of_string uri',0))
1591 (* Inductive Type *)
1592 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
1593 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1594 Some (Cic.MutInd (uri'',0,typeno))
1597 (* Constructor of an Inductive Type *)
1598 let uri'',typeno,consno =
1599 CicTextualLexer.indconuri_of_uri uri'
1601 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1602 Some (Cic.MutConstruct (uri'',0,typeno,consno))
1607 ignore (GtkMain.Main.init ()) ;
1608 initialize_everything () ;
1609 if !usedb then MQueryGenerator.close ();