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 (* GLOBAL CONSTANTS *)
39 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
40 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
44 " <body bgColor=\"white\">"
54 Sys.getenv "GTOPLEVEL_PROOFFILE"
56 Not_found -> "/public/currentproof"
61 Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
63 Not_found -> "/public/currentprooftype"
66 (*CSC: the getter should handle the innertypes, not the FS *)
70 Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
72 Not_found -> "/public/innertypes"
75 let constanttypefile =
77 Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
79 Not_found -> "/public/constanttype"
82 let postgresqlconnectionstring =
84 Sys.getenv "POSTGRESQL_CONNECTION_STRING"
86 Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
89 let empty_id_to_uris = ([],function _ -> None);;
92 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
94 let htmlheader_and_content = ref htmlheader;;
96 let current_cic_infos = ref None;;
97 let current_goal_infos = ref None;;
98 let current_scratch_infos = ref None;;
100 let id_to_uris = ref empty_id_to_uris;;
102 let check_term = ref (fun _ _ _ -> assert false);;
103 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
105 exception RenderingWindowsNotInitialized;;
107 let set_rendering_window,rendering_window =
108 let rendering_window_ref = ref None in
109 (function rw -> rendering_window_ref := Some rw),
111 match !rendering_window_ref with
112 None -> raise RenderingWindowsNotInitialized
117 exception SettingsWindowsNotInitialized;;
119 let set_settings_window,settings_window =
120 let settings_window_ref = ref None in
121 (function rw -> settings_window_ref := Some rw),
123 match !settings_window_ref with
124 None -> raise SettingsWindowsNotInitialized
129 exception OutputHtmlNotInitialized;;
131 let set_outputhtml,outputhtml =
132 let outputhtml_ref = ref None in
133 (function rw -> outputhtml_ref := Some rw),
135 match !outputhtml_ref with
136 None -> raise OutputHtmlNotInitialized
137 | Some outputhtml -> outputhtml
141 exception QedSetSensitiveNotInitialized;;
142 let qed_set_sensitive =
143 ref (function _ -> raise QedSetSensitiveNotInitialized)
146 exception SaveSetSensitiveNotInitialized;;
147 let save_set_sensitive =
148 ref (function _ -> raise SaveSetSensitiveNotInitialized)
151 (* COMMAND LINE OPTIONS *)
157 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
160 Arg.parse argspec ignore ""
164 let term_of_cic_textual_parser_uri uri =
165 let module C = Cic in
166 let module CTP = CicTextualParser0 in
168 CTP.ConUri uri -> C.Const (uri,[])
169 | CTP.VarUri uri -> C.Var (uri,[])
170 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
171 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
174 let string_of_cic_textual_parser_uri uri =
175 let module C = Cic in
176 let module CTP = CicTextualParser0 in
179 CTP.ConUri uri -> UriManager.string_of_uri uri
180 | CTP.VarUri uri -> UriManager.string_of_uri uri
181 | CTP.IndTyUri (uri,tyno) ->
182 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
183 | CTP.IndConUri (uri,tyno,consno) ->
184 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
187 (* 4 = String.length "cic:" *)
188 String.sub uri' 4 (String.length uri' - 4)
191 let output_html outputhtml msg =
192 htmlheader_and_content := !htmlheader_and_content ^ msg ;
193 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
194 outputhtml#set_topline (-1)
197 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
201 let check_window outputhtml uris =
204 ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
206 GPack.notebook ~scrollable:true ~packing:window#add () in
211 let scrolled_window =
212 GBin.scrolled_window ~border_width:10
214 (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
219 GMathViewAux.single_selection_math_view
220 ~packing:scrolled_window#add ~width:400 ~height:280 () in
223 term_of_cic_textual_parser_uri
224 (Disambiguate.cic_textual_parser_uri_of_string uri)
226 (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
229 let mml = !mml_of_cic_term_ref 111 expr in
230 mmlwidget#load_doc ~dom:mml
233 output_html outputhtml
234 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
239 (notebook#connect#switch_page
240 (function i -> Lazy.force (List.nth render_terms i)))
246 interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
247 ?(enable_button_for_non_vars=false) ~title ~msg uris
249 let choices = ref [] in
250 let chosen = ref false in
251 let use_only_constants = ref false in
253 GWindow.dialog ~modal:true ~title ~width:600 () in
255 GMisc.label ~text:msg
256 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
257 let scrolled_window =
258 GBin.scrolled_window ~border_width:10
259 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
261 let expected_height = 18 * List.length uris in
262 let height = if expected_height > 400 then 400 else expected_height in
263 GList.clist ~columns:1 ~packing:scrolled_window#add
264 ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
265 let _ = List.map (function x -> clist#append [x]) uris in
267 GPack.hbox ~border_width:0
268 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
270 GMisc.label ~text:"None of the above. Try this one:"
271 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
273 GEdit.entry ~editable:true
274 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
276 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
278 GButton.button ~label:ok
279 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
280 let _ = okb#misc#set_sensitive false in
285 if enable_button_for_non_vars then
286 hbox#pack ~expand:false ~fill:false ~padding:5 w)
287 ~label:"Try constants only" () in
289 GButton.button ~label:"Check"
290 ~packing:(hbox#pack ~padding:5) () in
291 let _ = checkb#misc#set_sensitive false in
293 GButton.button ~label:"Abort"
294 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
296 let check_callback () =
297 assert (List.length !choices > 0) ;
298 check_window (outputhtml ()) !choices
300 ignore (window#connect#destroy GMain.Main.quit) ;
301 ignore (cancelb#connect#clicked window#destroy) ;
303 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
305 (nonvarsb#connect#clicked
307 use_only_constants := true ;
311 ignore (checkb#connect#clicked check_callback) ;
313 (clist#connect#select_row
314 (fun ~row ~column ~event ->
315 checkb#misc#set_sensitive true ;
316 okb#misc#set_sensitive true ;
317 choices := (List.nth uris row)::!choices)) ;
319 (clist#connect#unselect_row
320 (fun ~row ~column ~event ->
322 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
324 (manual_input#connect#changed
326 if manual_input#text = "" then
329 checkb#misc#set_sensitive false ;
330 okb#misc#set_sensitive false ;
331 clist#misc#set_sensitive true
335 choices := [manual_input#text] ;
336 clist#unselect_all () ;
337 checkb#misc#set_sensitive true ;
338 okb#misc#set_sensitive true ;
339 clist#misc#set_sensitive false
341 window#set_position `CENTER ;
345 if !use_only_constants then
347 (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
350 if List.length !choices > 0 then !choices else raise NoChoice
355 let interactive_interpretation_choice interpretations =
356 let chosen = ref None in
359 ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
360 let vbox = GPack.vbox ~packing:window#add () in
364 ("Ambiguous input since there are many well-typed interpretations." ^
365 " Please, choose one of them.")
366 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
368 GPack.notebook ~scrollable:true
369 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
372 (function interpretation ->
374 let expected_height = 18 * List.length interpretation in
375 let height = if expected_height > 400 then 400 else expected_height in
376 GList.clist ~columns:2 ~packing:notebook#append_page ~height
377 ~titles:["id" ; "URI"] ()
381 (function (id,uri) ->
382 let n = clist#append [id;uri] in
383 clist#set_row ~selectable:false n
386 clist#columns_autosize ()
389 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
391 GButton.button ~label:"Ok"
392 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
394 GButton.button ~label:"Abort"
395 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
397 ignore (window#connect#destroy GMain.Main.quit) ;
398 ignore (cancelb#connect#clicked window#destroy) ;
401 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
402 window#set_position `CENTER ;
406 None -> raise NoChoice
413 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
415 let query = ref "" in
416 MQueryGenerator.set_confirm_query
417 (function q -> query := MQueryUtil.text_of_query q ; true) ;
418 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
421 let domImpl = Gdome.domImplementation ();;
423 let parseStyle name =
425 domImpl#createDocumentFromURI
427 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
429 ~uri:("styles/" ^ name) ()
431 Gdome_xslt.processStylesheet style
434 let d_c = parseStyle "drop_coercions.xsl";;
435 let tc1 = parseStyle "objtheorycontent.xsl";;
436 let hc2 = parseStyle "content_to_html.xsl";;
437 let l = parseStyle "link.xsl";;
439 let c1 = parseStyle "rootcontent.xsl";;
440 let g = parseStyle "genmmlid.xsl";;
441 let c2 = parseStyle "annotatedpres.xsl";;
444 let getterURL = Configuration.getter_url;;
445 let processorURL = Configuration.processor_url;;
447 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
448 let mml_args ~explode_all =
449 ("explodeall",(if explode_all then "true()" else "false()"))::
450 ["processorURL", "'" ^ processorURL ^ "'" ;
451 "getterURL", "'" ^ getterURL ^ "'" ;
452 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
453 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
454 "UNICODEvsSYMBOL", "'symbol'" ;
455 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
456 "encoding", "'iso-8859-1'" ;
457 "media-type", "'text/html'" ;
458 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
459 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
460 "naturalLanguage", "'yes'" ;
461 "annotations", "'no'" ;
462 "URLs_or_URIs", "'URIs'" ;
463 "topurl", "'http://phd.cs.unibo.it/helm'" ;
464 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
467 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
469 ["processorURL", "'" ^ processorURL ^ "'" ;
470 "getterURL", "'" ^ getterURL ^ "'" ;
471 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
472 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
473 "UNICODEvsSYMBOL", "'symbol'" ;
474 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
475 "encoding", "'iso-8859-1'" ;
476 "media-type", "'text/html'" ;
477 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
478 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
479 "naturalLanguage", "'no'" ;
480 "annotations", "'no'" ;
481 "explodeall", "true()" ;
482 "URLs_or_URIs", "'URIs'" ;
483 "topurl", "'http://phd.cs.unibo.it/helm'" ;
484 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
487 let parse_file filename =
488 let inch = open_in filename in
489 let rec read_lines () =
491 let line = input_line inch in
499 let applyStylesheets input styles args =
500 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
505 mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
507 (*CSC: ????????????????? *)
509 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
513 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
514 ~ask_dtd_to_the_getter:true
518 None -> Xml2Gdome.document_of_xml domImpl xml
520 Xml.pp xml (Some constanttypefile) ;
521 Xml2Gdome.document_of_xml domImpl bodyxml'
523 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
524 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
526 Xml.pp xmlinnertypes (Some innertypesfile) ;
527 let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
532 save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
535 let struri = UriManager.string_of_uri uri in
536 let idx = (String.rindex struri '/') + 1 in
537 String.sub struri idx (String.length struri - idx)
539 let path = pathname ^ "/" ^ name in
541 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
545 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
546 ~ask_dtd_to_the_getter:false
549 let innertypesuri = UriManager.innertypesuri_of_uri uri in
550 Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
551 Getter.register innertypesuri
552 (Configuration.annotations_url ^
553 Str.replace_first (Str.regexp "^cic:") ""
554 (UriManager.string_of_uri innertypesuri) ^ ".xml"
556 (* constant type / variable / mutual inductive types definition *)
557 Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
559 (Configuration.annotations_url ^
560 Str.replace_first (Str.regexp "^cic:") ""
561 (UriManager.string_of_uri uri) ^ ".xml"
568 match UriManager.bodyuri_of_uri uri with
570 | Some bodyuri -> bodyuri
572 Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
573 Getter.register bodyuri
574 (Configuration.annotations_url ^
575 Str.replace_first (Str.regexp "^cic:") ""
576 (UriManager.string_of_uri bodyuri) ^ ".xml"
583 exception RefreshSequentException of exn;;
584 exception RefreshProofException of exn;;
586 let refresh_proof (output : GMathViewAux.single_selection_math_view) =
588 let uri,currentproof =
589 match !ProofEngine.proof with
591 | Some (uri,metasenv,bo,ty) ->
592 !qed_set_sensitive (List.length metasenv = 0) ;
593 (*CSC: Wrong: [] is just plainly wrong *)
594 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
597 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
598 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
600 Cic2acic.acic_object_of_cic_object currentproof
603 mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
606 output#load_doc ~dom:mml ;
608 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
611 match !ProofEngine.proof with
613 | Some (uri,metasenv,bo,ty) ->
614 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
615 raise (RefreshProofException e)
618 let refresh_sequent ?(empty_notebook=true) notebook =
620 match !ProofEngine.goal with
622 if empty_notebook then
624 notebook#remove_all_pages ~skip_switch_page_event:false ;
625 notebook#set_empty_page
628 notebook#proofw#unload
631 match !ProofEngine.proof with
633 | Some (_,metasenv,_,_) -> metasenv
635 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
636 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
637 SequentPp.XmlPp.print_sequent metasenv currentsequent
639 let regenerate_notebook () =
640 let skip_switch_page_event =
642 (m,_,_)::_ when m = metano -> false
645 notebook#remove_all_pages ~skip_switch_page_event ;
646 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
648 if empty_notebook then
650 regenerate_notebook () ;
651 notebook#set_current_page ~may_skip_switch_page_event:false metano
655 let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
657 applyStylesheets sequent_doc sequent_styles sequent_args
659 notebook#set_current_page ~may_skip_switch_page_event:true metano;
660 notebook#proofw#load_doc ~dom:sequent_mml
662 current_goal_infos :=
663 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
667 match !ProofEngine.goal with
672 match !ProofEngine.proof with
674 | Some (_,metasenv,_,_) -> metasenv
677 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
678 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
679 raise (RefreshSequentException e)
680 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
684 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
685 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
688 let mml_of_cic_term metano term =
690 match !ProofEngine.proof with
692 | Some (_,metasenv,_,_) -> metasenv
695 match !ProofEngine.goal with
698 let (_,canonical_context,_) =
699 List.find (function (m,_,_) -> m=metano) metasenv
703 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
704 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
707 Xml2Gdome.document_of_xml domImpl sequent_gdome
710 applyStylesheets sequent_doc sequent_styles sequent_args ;
712 current_scratch_infos :=
713 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
717 exception OpenConjecturesStillThere;;
718 exception WrongProof;;
720 let pathname_of_annuri uristring =
721 Configuration.annotations_dir ^
722 Str.replace_first (Str.regexp "^cic:") "" uristring
725 let make_dirs dirpath =
726 ignore (Unix.system ("mkdir -p " ^ dirpath))
729 let save_obj uri obj =
731 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
732 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
734 Cic2acic.acic_object_of_cic_object obj
736 (* let's save the theorem and register it to the getter *)
737 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
739 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
744 match !ProofEngine.proof with
746 | Some (uri,[],bo,ty) ->
748 CicReduction.are_convertible []
749 (CicTypeChecker.type_of_aux' [] [] bo) ty
752 (*CSC: Wrong: [] is just plainly wrong *)
753 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
755 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
756 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
758 Cic2acic.acic_object_of_cic_object proof
761 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
764 ((rendering_window ())#output : GMathViewAux.single_selection_math_view)#load_doc mml ;
765 !qed_set_sensitive false ;
766 (* let's save the theorem and register it to the getter *)
767 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
769 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
773 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
778 | _ -> raise OpenConjecturesStillThere
782 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
783 match !ProofEngine.proof with
785 | Some (uri, metasenv, bo, ty) ->
787 (*CSC: Wrong: [] is just plainly wrong *)
788 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
790 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
791 Cic2acic.acic_object_of_cic_object currentproof
795 Cic2Xml.print_object uri ~ids_to_inner_sorts
796 ~ask_dtd_to_the_getter:true acurrentproof
798 xml,Some bodyxml -> xml,bodyxml
799 | _,None -> assert false
801 Xml.pp ~quiet:true xml (Some prooffiletype) ;
802 output_html outputhtml
803 ("<h1 color=\"Green\">Current proof type saved to " ^
804 prooffiletype ^ "</h1>") ;
805 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
806 output_html outputhtml
807 ("<h1 color=\"Green\">Current proof body saved to " ^
811 (* Used to typecheck the loaded proofs *)
812 let typecheck_loaded_proof metasenv bo ty =
813 let module T = CicTypeChecker in
816 (fun metasenv ((_,context,ty) as conj) ->
817 ignore (T.type_of_aux' metasenv context ty) ;
820 ignore (T.type_of_aux' metasenv [] ty) ;
821 ignore (T.type_of_aux' metasenv [] bo)
825 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
826 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
827 let notebook = (rendering_window ())#notebook in
830 GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
833 None -> raise NoChoice
835 let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
836 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
837 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
838 typecheck_loaded_proof metasenv bo ty ;
840 Some (uri, metasenv, bo, ty) ;
844 | (metano,_,_)::_ -> Some metano
846 refresh_proof output ;
847 refresh_sequent notebook ;
848 output_html outputhtml
849 ("<h1 color=\"Green\">Current proof type loaded from " ^
850 prooffiletype ^ "</h1>") ;
851 output_html outputhtml
852 ("<h1 color=\"Green\">Current proof body loaded from " ^
853 prooffile ^ "</h1>") ;
854 !save_set_sensitive true
857 RefreshSequentException e ->
858 output_html outputhtml
859 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
860 "sequent: " ^ Printexc.to_string e ^ "</h1>")
861 | RefreshProofException e ->
862 output_html outputhtml
863 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
864 "proof: " ^ Printexc.to_string e ^ "</h1>")
866 output_html outputhtml
867 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
870 let edit_aliases () =
871 let chosen = ref false in
874 ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
876 GPack.vbox ~border_width:0 ~packing:window#add () in
877 let scrolled_window =
878 GBin.scrolled_window ~border_width:10
879 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
880 let input = GEdit.text ~editable:true ~width:400 ~height:100
881 ~packing:scrolled_window#add () in
883 GPack.hbox ~border_width:0
884 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
886 GButton.button ~label:"Ok"
887 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
889 GButton.button ~label:"Cancel"
890 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
891 ignore (window#connect#destroy GMain.Main.quit) ;
892 ignore (cancelb#connect#clicked window#destroy) ;
894 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
895 let dom,resolve_id = !id_to_uris in
897 (input#insert_text ~pos:0
902 match resolve_id v with
907 (string_of_cic_textual_parser_uri uri)
913 let inputtext = input#get_chars 0 input#length in
915 let alfa = "[a-zA-Z_-]" in
916 let digit = "[0-9]" in
917 let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
918 let blanks = "\( \|\t\|\n\)+" in
919 let nonblanks = "[^ \t\n]+" in
920 let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
922 ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
926 let n' = Str.search_forward regexpr inputtext n in
927 let id = Str.matched_group 2 inputtext in
929 Disambiguate.cic_textual_parser_uri_of_string
930 ("cic:" ^ (Str.matched_group 5 inputtext))
932 let dom,resolve_id = aux (n' + 1) in
933 if List.mem id dom then
937 (function id' -> if id = id' then Some uri else resolve_id id')
939 Not_found -> empty_id_to_uris
943 id_to_uris := dom,resolve_id
947 let module L = LogicalOperations in
948 let module G = Gdome in
949 let notebook = (rendering_window ())#notebook in
950 let output = (rendering_window ())#output in
951 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
952 match (rendering_window ())#output#get_selection with
955 ((node : Gdome.element)#getAttributeNS
957 ((element : G.element)#getAttributeNS
960 ~localName:(G.domString "xref"))#to_string
962 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
966 match !current_cic_infos with
967 Some (ids_to_terms, ids_to_father_ids, _, _) ->
969 L.to_sequent id ids_to_terms ids_to_father_ids ;
970 refresh_proof output ;
971 refresh_sequent notebook
972 | None -> assert false (* "ERROR: No current term!!!" *)
974 RefreshSequentException e ->
975 output_html outputhtml
976 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
977 "sequent: " ^ Printexc.to_string e ^ "</h1>")
978 | RefreshProofException e ->
979 output_html outputhtml
980 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
981 "proof: " ^ Printexc.to_string e ^ "</h1>")
983 output_html outputhtml
984 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
986 | None -> assert false (* "ERROR: No selection!!!" *)
990 let module L = LogicalOperations in
991 let module G = Gdome in
992 let notebook = (rendering_window ())#notebook in
993 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
994 match (rendering_window ())#output#get_selection with
997 ((node : Gdome.element)#getAttributeNS
999 ((element : G.element)#getAttributeNS
1001 ~namespaceURI:helmns
1002 ~localName:(G.domString "xref"))#to_string
1004 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1008 match !current_cic_infos with
1009 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1011 L.focus id ids_to_terms ids_to_father_ids ;
1012 refresh_sequent notebook
1013 | None -> assert false (* "ERROR: No current term!!!" *)
1015 RefreshSequentException e ->
1016 output_html outputhtml
1017 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1018 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1019 | RefreshProofException e ->
1020 output_html outputhtml
1021 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1022 "proof: " ^ Printexc.to_string e ^ "</h1>")
1024 output_html outputhtml
1025 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1027 | None -> assert false (* "ERROR: No selection!!!" *)
1030 exception NoPrevGoal;;
1031 exception NoNextGoal;;
1033 let setgoal metano =
1034 let module L = LogicalOperations in
1035 let module G = Gdome in
1036 let notebook = (rendering_window ())#notebook in
1037 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1039 match !ProofEngine.proof with
1040 None -> assert false
1041 | Some (_,metasenv,_,_) -> metasenv
1044 refresh_sequent ~empty_notebook:false notebook
1046 RefreshSequentException e ->
1047 output_html outputhtml
1048 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1049 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1051 output_html outputhtml
1052 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1056 show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
1059 GWindow.window ~width:800 ~border_width:2 () in
1060 let scrolled_window =
1061 GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1063 GMathViewAux.single_selection_math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1064 let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1065 let href = Gdome.domString "href" in
1066 let show_in_show_window_obj uri obj =
1067 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1070 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1071 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1073 Cic2acic.acic_object_of_cic_object obj
1076 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1079 window#set_title (UriManager.string_of_uri uri) ;
1080 window#misc#hide () ; window#show () ;
1081 mmlwidget#load_doc mml ;
1084 output_html outputhtml
1085 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1087 let show_in_show_window_uri uri =
1088 let obj = CicEnvironment.get_obj uri in
1089 show_in_show_window_obj uri obj
1091 let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
1092 if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1094 (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1096 show_in_show_window_uri (UriManager.uri_of_string uri)
1098 ignore (mmlwidget#action_toggle n)
1101 mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
1103 show_in_show_window_obj, show_in_show_window_uri,
1104 show_in_show_window_callback
1107 exception NoObjectsLocated;;
1109 let user_uri_choice ~title ~msg uris =
1112 [] -> raise NoObjectsLocated
1116 interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1121 String.sub uri 4 (String.length uri - 4)
1124 let locate_callback id =
1125 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1126 let result = MQueryGenerator.locate id in
1130 Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri)
1133 (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1135 output_html outputhtml html ;
1136 user_uri_choice ~title:"Ambiguous input."
1138 ("Ambiguous input \"" ^ id ^
1139 "\". Please, choose one interpetation:")
1144 let input_or_locate_uri ~title =
1145 let uri = ref None in
1148 ~width:400 ~modal:true ~title ~border_width:2 () in
1149 let vbox = GPack.vbox ~packing:window#add () in
1151 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1153 GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1155 GEdit.entry ~editable:true
1156 ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1158 GButton.button ~label:"Check"
1159 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1160 let _ = checkb#misc#set_sensitive false in
1162 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1164 GMisc.label ~text:"You can also enter an indentifier to locate:"
1165 ~packing:(hbox2#pack ~padding:5) () in
1167 GEdit.entry ~editable:true
1168 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1170 GButton.button ~label:"Locate"
1171 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1172 let _ = locateb#misc#set_sensitive false in
1174 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1176 GButton.button ~label:"Ok"
1177 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1178 let _ = okb#misc#set_sensitive false in
1180 GButton.button ~label:"Cancel"
1181 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1183 ignore (window#connect#destroy GMain.Main.quit) ;
1185 (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1186 let check_callback () =
1187 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1188 let uri = "cic:" ^ manual_input#text in
1190 ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1191 output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1194 Getter.Unresolved ->
1195 output_html outputhtml
1196 ("<h1 color=\"Red\">URI " ^ uri ^
1197 " does not correspond to any object.</h1>") ;
1199 | UriManager.IllFormedUri _ ->
1200 output_html outputhtml
1201 ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1204 output_html outputhtml
1205 ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1209 (okb#connect#clicked
1211 if check_callback () then
1213 uri := Some manual_input#text ;
1217 ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1219 (manual_input#connect#changed
1221 if manual_input#text = "" then
1223 checkb#misc#set_sensitive false ;
1224 okb#misc#set_sensitive false
1228 checkb#misc#set_sensitive true ;
1229 okb#misc#set_sensitive true
1232 (locate_input#connect#changed
1233 (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1235 (locateb#connect#clicked
1237 let id = locate_input#text in
1238 manual_input#set_text (locate_callback id) ;
1239 locate_input#delete_text 0 (String.length id)
1242 GMain.Main.main () ;
1244 None -> raise NoChoice
1245 | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1248 exception AmbiguousInput;;
1250 (* A WIDGET TO ENTER CIC TERMS *)
1254 let output_html msg = output_html (outputhtml ()) msg;;
1255 let interactive_user_uri_choice =
1256 fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
1257 interactive_user_uri_choice ~selection_mode ?ok
1258 ?enable_button_for_non_vars ~title ~msg;;
1259 let interactive_interpretation_choice = interactive_interpretation_choice;;
1260 let input_or_locate_uri = input_or_locate_uri;;
1264 module Disambiguate' = Disambiguate.Make(Callbacks);;
1266 class term_editor ?packing ?width ?height ?isnotempty_callback () =
1267 let input = GEdit.text ~editable:true ?width ?height ?packing () in
1269 match isnotempty_callback with
1272 ignore(input#connect#changed (function () -> callback (input#length > 0)))
1275 method coerce = input#coerce
1277 input#delete_text 0 input#length
1278 (* CSC: txt is now a string, but should be of type Cic.term *)
1279 method set_term txt =
1281 ignore ((input#insert_text txt) ~pos:0)
1282 (* CSC: this method should disappear *)
1283 method get_as_string =
1284 input#get_chars 0 input#length
1285 method get_metasenv_and_term ~context ~metasenv =
1289 Some (n,_) -> Some n
1293 let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
1294 let dom,mk_metasenv_and_expr =
1295 CicTextualParserContext.main
1296 ~context:name_context ~metasenv CicTextualLexer.token lexbuf
1298 let id_to_uris',metasenv,expr =
1299 Disambiguate'.disambiguate_input context metasenv dom mk_metasenv_and_expr
1300 ~id_to_uris:!id_to_uris
1302 id_to_uris := id_to_uris' ;
1307 (* OTHER FUNCTIONS *)
1310 let inputt = ((rendering_window ())#inputt : term_editor) in
1311 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1314 GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1316 None -> raise NoChoice
1318 let uri = locate_callback input in
1322 output_html outputhtml
1323 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1327 exception UriAlreadyInUse;;
1328 exception NotAUriToAConstant;;
1330 let new_inductive () =
1331 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1332 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1333 let notebook = (rendering_window ())#notebook in
1335 let chosen = ref false in
1336 let inductive = ref true in
1337 let paramsno = ref 0 in
1338 let get_uri = ref (function _ -> assert false) in
1339 let get_base_uri = ref (function _ -> assert false) in
1340 let get_names = ref (function _ -> assert false) in
1341 let get_types_and_cons = ref (function _ -> assert false) in
1342 let get_context_and_subst = ref (function _ -> assert false) in
1345 ~width:600 ~modal:true ~position:`CENTER
1346 ~title:"New Block of Mutual (Co)Inductive Definitions"
1347 ~border_width:2 () in
1348 let vbox = GPack.vbox ~packing:window#add () in
1350 GPack.hbox ~border_width:0
1351 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1353 GMisc.label ~text:"Enter the URI for the new block:"
1354 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1356 GEdit.entry ~editable:true
1357 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1359 GPack.hbox ~border_width:0
1360 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1364 "Enter the number of left parameters in every arity and constructor type:"
1365 ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1366 let paramsno_entry =
1367 GEdit.entry ~editable:true ~text:"0"
1368 ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1370 GPack.hbox ~border_width:0
1371 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1373 GMisc.label ~text:"Are the definitions inductive or coinductive?"
1374 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1376 GButton.radio_button ~label:"Inductive"
1377 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1379 GButton.radio_button ~label:"Coinductive"
1380 ~group:inductiveb#group
1381 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1383 GPack.hbox ~border_width:0
1384 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1386 GMisc.label ~text:"Enter the list of the names of the types:"
1387 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1389 GEdit.entry ~editable:true
1390 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1392 GPack.hbox ~border_width:0
1393 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1395 GButton.button ~label:"> Next"
1396 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1397 let _ = okb#misc#set_sensitive true in
1399 GButton.button ~label:"Abort"
1400 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1401 ignore (window#connect#destroy GMain.Main.quit) ;
1402 ignore (cancelb#connect#clicked window#destroy) ;
1406 (okb#connect#clicked
1409 let uristr = "cic:" ^ uri_entry#text in
1410 let namesstr = names_entry#text in
1411 let paramsno' = int_of_string (paramsno_entry#text) in
1412 match Str.split (Str.regexp " +") namesstr with
1414 | (he::tl) as names ->
1415 let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1418 ignore (Getter.resolve uri) ;
1419 raise UriAlreadyInUse
1421 Getter.Unresolved ->
1422 get_uri := (function () -> uri) ;
1423 get_names := (function () -> names) ;
1424 inductive := inductiveb#active ;
1425 paramsno := paramsno' ;
1430 output_html outputhtml
1431 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1439 GBin.frame ~label:name
1440 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1441 let vbox = GPack.vbox ~packing:frame#add () in
1442 let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1444 GMisc.label ~text:("Enter its type:")
1445 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1446 let scrolled_window =
1447 GBin.scrolled_window ~border_width:5
1448 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1450 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1451 ~isnotempty_callback:
1453 (*non_empty_type := b ;*)
1454 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1457 GPack.hbox ~border_width:0
1458 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1460 GMisc.label ~text:("Enter the list of its constructors:")
1461 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1462 let cons_names_entry =
1463 GEdit.entry ~editable:true
1464 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1465 (newinputt,cons_names_entry)
1468 vbox#remove hboxn#coerce ;
1470 GPack.hbox ~border_width:0
1471 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1473 GButton.button ~label:"> Next"
1474 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1476 GButton.button ~label:"Abort"
1477 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1478 ignore (cancelb#connect#clicked window#destroy) ;
1480 (okb#connect#clicked
1483 let names = !get_names () in
1484 let types_and_cons =
1486 (fun name (newinputt,cons_names_entry) ->
1487 let consnamesstr = cons_names_entry#text in
1488 let cons_names = Str.split (Str.regexp " +") consnamesstr in
1490 newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
1493 [] -> expr,cons_names
1494 | _ -> raise AmbiguousInput
1495 ) names type_widgets
1497 let uri = !get_uri () in
1499 (* Let's see if so far the definition is well-typed *)
1502 (* To test if the arities of the inductive types are well *)
1503 (* typed, we check the inductive block definition where *)
1504 (* no constructor is given to each type. *)
1507 (fun name (ty,cons) -> (name, !inductive, ty, []))
1508 names types_and_cons
1510 CicTypeChecker.typecheck_mutual_inductive_defs uri
1511 (tys,params,paramsno)
1513 get_context_and_subst :=
1517 (fun (context,subst) name (ty,_) ->
1519 (Some (Cic.Name name, Cic.Decl ty))::context,
1520 (Cic.MutInd (uri,!i,[]))::subst
1523 ) ([],[]) names types_and_cons) ;
1524 let types_and_cons' =
1526 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1527 names types_and_cons
1529 get_types_and_cons := (function () -> types_and_cons') ;
1534 output_html outputhtml
1535 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1538 and phase3 name cons =
1539 let get_cons_types = ref (function () -> assert false) in
1542 ~width:600 ~modal:true ~position:`CENTER
1543 ~title:(name ^ " Constructors")
1544 ~border_width:2 () in
1545 let vbox = GPack.vbox ~packing:window2#add () in
1546 let cons_type_widgets =
1548 (function consname ->
1550 GPack.hbox ~border_width:0
1551 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1553 GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1554 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1555 let scrolled_window =
1556 GBin.scrolled_window ~border_width:5
1557 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1559 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1560 ~isnotempty_callback:
1562 (* (*non_empty_type := b ;*)
1563 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1568 GPack.hbox ~border_width:0
1569 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1571 GButton.button ~label:"> Next"
1572 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1573 let _ = okb#misc#set_sensitive true in
1575 GButton.button ~label:"Abort"
1576 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1577 ignore (window2#connect#destroy GMain.Main.quit) ;
1578 ignore (cancelb#connect#clicked window2#destroy) ;
1580 (okb#connect#clicked
1584 let context,subst= !get_context_and_subst () in
1589 inputt#get_metasenv_and_term ~context ~metasenv:[]
1593 let undebrujined_expr =
1595 (fun expr t -> CicSubstitution.subst t expr) expr subst
1597 name, undebrujined_expr
1598 | _ -> raise AmbiguousInput
1599 ) cons cons_type_widgets
1601 get_cons_types := (function () -> cons_types) ;
1605 output_html outputhtml
1606 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1609 GMain.Main.main () ;
1610 let okb_pressed = !chosen in
1612 if (not okb_pressed) then
1615 assert false (* The control never reaches this point *)
1618 (!get_cons_types ())
1621 (* No more phases left or Abort pressed *)
1623 GMain.Main.main () ;
1627 let uri = !get_uri () in
1630 let tys = !get_types_and_cons () in
1631 let obj = Cic.InductiveDefinition tys params !paramsno in
1634 prerr_endline (CicPp.ppobj obj) ;
1635 CicTypeChecker.typecheck_mutual_inductive_defs uri
1636 (tys,params,!paramsno) ;
1639 prerr_endline "Offending mutual (co)inductive type declaration:" ;
1640 prerr_endline (CicPp.ppobj obj) ;
1642 (* We already know that obj is well-typed. We need to add it to the *)
1643 (* environment in order to compute the inner-types without having to *)
1644 (* debrujin it or having to modify lots of other functions to avoid *)
1645 (* asking the environment for the MUTINDs we are defining now. *)
1646 CicEnvironment.put_inductive_definition uri obj ;
1648 show_in_show_window_obj uri obj
1651 output_html outputhtml
1652 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1655 let mk_fresh_name_callback context name ~typ =
1657 match ProofEngineHelpers.mk_fresh_name context name ~typ with
1658 Cic.Name fresh_name -> fresh_name
1659 | Cic.Anonymous -> assert false
1662 GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name
1663 ("Enter a fresh name for the hypothesis " ^
1665 (List.map (function None -> None | Some (n,_) -> Some n) context))
1667 Some fresh_name' -> Cic.Name fresh_name'
1668 | None -> raise NoChoice
1672 let inputt = ((rendering_window ())#inputt : term_editor) in
1673 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1674 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1675 let notebook = (rendering_window ())#notebook in
1677 let chosen = ref false in
1678 let get_metasenv_and_term = ref (function _ -> assert false) in
1679 let get_uri = ref (function _ -> assert false) in
1680 let non_empty_type = ref false in
1683 ~width:600 ~modal:true ~title:"New Proof or Definition"
1684 ~border_width:2 () in
1685 let vbox = GPack.vbox ~packing:window#add () in
1687 GPack.hbox ~border_width:0
1688 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1690 GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1691 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1693 GEdit.entry ~editable:true
1694 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1696 GPack.hbox ~border_width:0
1697 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1699 GMisc.label ~text:"Enter the theorem or definition type:"
1700 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1701 let scrolled_window =
1702 GBin.scrolled_window ~border_width:5
1703 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1704 (* the content of the scrolled_window is moved below (see comment) *)
1706 GPack.hbox ~border_width:0
1707 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1709 GButton.button ~label:"Ok"
1710 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1711 let _ = okb#misc#set_sensitive false in
1713 GButton.button ~label:"Cancel"
1714 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1715 (* moved here to have visibility of the ok button *)
1717 new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1718 ~isnotempty_callback:
1720 non_empty_type := b ;
1721 okb#misc#set_sensitive (b && uri_entry#text <> ""))
1724 newinputt#set_term inputt#get_as_string ;
1727 uri_entry#connect#changed
1729 okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1731 ignore (window#connect#destroy GMain.Main.quit) ;
1732 ignore (cancelb#connect#clicked window#destroy) ;
1734 (okb#connect#clicked
1738 let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
1739 let uristr = "cic:" ^ uri_entry#text in
1740 let uri = UriManager.uri_of_string uristr in
1741 if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1742 raise NotAUriToAConstant
1746 ignore (Getter.resolve uri) ;
1747 raise UriAlreadyInUse
1749 Getter.Unresolved ->
1750 get_metasenv_and_term := (function () -> metasenv,parsed) ;
1751 get_uri := (function () -> uri) ;
1756 output_html outputhtml
1757 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1760 GMain.Main.main () ;
1763 let metasenv,expr = !get_metasenv_and_term () in
1764 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1765 ProofEngine.proof :=
1766 Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1767 ProofEngine.goal := Some 1 ;
1768 refresh_sequent notebook ;
1769 refresh_proof output ;
1770 !save_set_sensitive true ;
1772 ProofEngine.intros ~mk_fresh_name_callback () ;
1773 refresh_sequent notebook ;
1774 refresh_proof output
1776 RefreshSequentException e ->
1777 output_html outputhtml
1778 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1779 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1780 | RefreshProofException e ->
1781 output_html outputhtml
1782 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1783 "proof: " ^ Printexc.to_string e ^ "</h1>")
1785 output_html outputhtml
1786 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1789 let check_term_in_scratch scratch_window metasenv context expr =
1791 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1792 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1793 scratch_window#show () ;
1794 scratch_window#mmlwidget#load_doc ~dom:mml
1797 print_endline ("? " ^ CicPp.ppterm expr) ;
1801 let check scratch_window () =
1802 let inputt = ((rendering_window ())#inputt : term_editor) in
1803 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1805 match !ProofEngine.proof with
1807 | Some (_,metasenv,_,_) -> metasenv
1810 match !ProofEngine.goal with
1813 let (_,canonical_context,_) =
1814 List.find (function (m,_,_) -> m=metano) metasenv
1819 let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
1820 check_term_in_scratch scratch_window metasenv' context expr
1823 output_html outputhtml
1824 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1827 let decompose_uris_choice_callback uris =
1828 (* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
1829 let module U = UriManager in
1832 match Disambiguate.cic_textual_parser_uri_of_string uri with
1833 CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
1834 | _ -> assert false)
1835 (interactive_user_uri_choice
1836 ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
1837 ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
1839 (function (uri,typeno,_) ->
1840 U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)
1845 (***********************)
1847 (***********************)
1849 let call_tactic tactic () =
1850 let notebook = (rendering_window ())#notebook in
1851 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1852 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1853 let savedproof = !ProofEngine.proof in
1854 let savedgoal = !ProofEngine.goal in
1858 refresh_sequent notebook ;
1859 refresh_proof output
1861 RefreshSequentException e ->
1862 output_html outputhtml
1863 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1864 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1865 ProofEngine.proof := savedproof ;
1866 ProofEngine.goal := savedgoal ;
1867 refresh_sequent notebook
1868 | RefreshProofException e ->
1869 output_html outputhtml
1870 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1871 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1872 ProofEngine.proof := savedproof ;
1873 ProofEngine.goal := savedgoal ;
1874 refresh_sequent notebook ;
1875 refresh_proof output
1877 output_html outputhtml
1878 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1879 ProofEngine.proof := savedproof ;
1880 ProofEngine.goal := savedgoal ;
1884 let call_tactic_with_input tactic () =
1885 let notebook = (rendering_window ())#notebook in
1886 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1887 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1888 let inputt = ((rendering_window ())#inputt : term_editor) in
1889 let savedproof = !ProofEngine.proof in
1890 let savedgoal = !ProofEngine.goal in
1891 let uri,metasenv,bo,ty =
1892 match !ProofEngine.proof with
1893 None -> assert false
1894 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1896 let canonical_context =
1897 match !ProofEngine.goal with
1898 None -> assert false
1900 let (_,canonical_context,_) =
1901 List.find (function (m,_,_) -> m=metano) metasenv
1906 let metasenv',expr =
1907 inputt#get_metasenv_and_term canonical_context metasenv
1909 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1911 refresh_sequent notebook ;
1912 refresh_proof output ;
1915 RefreshSequentException e ->
1916 output_html outputhtml
1917 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1918 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1919 ProofEngine.proof := savedproof ;
1920 ProofEngine.goal := savedgoal ;
1921 refresh_sequent notebook
1922 | RefreshProofException e ->
1923 output_html outputhtml
1924 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1925 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1926 ProofEngine.proof := savedproof ;
1927 ProofEngine.goal := savedgoal ;
1928 refresh_sequent notebook ;
1929 refresh_proof output
1931 output_html outputhtml
1932 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1933 ProofEngine.proof := savedproof ;
1934 ProofEngine.goal := savedgoal ;
1937 let call_tactic_with_goal_input tactic () =
1938 let module L = LogicalOperations in
1939 let module G = Gdome in
1940 let notebook = (rendering_window ())#notebook in
1941 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1942 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1943 let savedproof = !ProofEngine.proof in
1944 let savedgoal = !ProofEngine.goal in
1945 match notebook#proofw#get_selections with
1948 ((node : Gdome.element)#getAttributeNS
1949 ~namespaceURI:helmns
1950 ~localName:(G.domString "xref"))#to_string
1952 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1956 match !current_goal_infos with
1957 Some (ids_to_terms, ids_to_father_ids,_) ->
1959 tactic (Hashtbl.find ids_to_terms id) ;
1960 refresh_sequent notebook ;
1961 refresh_proof output
1962 | None -> assert false (* "ERROR: No current term!!!" *)
1964 RefreshSequentException e ->
1965 output_html outputhtml
1966 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1967 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1968 ProofEngine.proof := savedproof ;
1969 ProofEngine.goal := savedgoal ;
1970 refresh_sequent notebook
1971 | RefreshProofException e ->
1972 output_html outputhtml
1973 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1974 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1975 ProofEngine.proof := savedproof ;
1976 ProofEngine.goal := savedgoal ;
1977 refresh_sequent notebook ;
1978 refresh_proof output
1980 output_html outputhtml
1981 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1982 ProofEngine.proof := savedproof ;
1983 ProofEngine.goal := savedgoal ;
1986 output_html outputhtml
1987 ("<h1 color=\"red\">No term selected</h1>")
1989 output_html outputhtml
1990 ("<h1 color=\"red\">Many terms selected</h1>")
1993 let call_tactic_with_goal_inputs tactic () =
1994 let module L = LogicalOperations in
1995 let module G = Gdome in
1996 let notebook = (rendering_window ())#notebook in
1998 ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1999 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2000 let savedproof = !ProofEngine.proof in
2001 let savedgoal = !ProofEngine.goal in
2003 let term_of_node node =
2005 ((node : Gdome.element)#getAttributeNS
2006 ~namespaceURI:helmns
2007 ~localName:(G.domString "xref"))#to_string
2009 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2011 match !current_goal_infos with
2012 Some (ids_to_terms, ids_to_father_ids,_) ->
2014 (Hashtbl.find ids_to_terms id)
2015 | None -> assert false (* "ERROR: No current term!!!" *)
2017 match notebook#proofw#get_selections with
2019 output_html outputhtml
2020 ("<h1 color=\"red\">No term selected</h1>")
2022 let terms = List.map term_of_node l in
2023 match !current_goal_infos with
2024 Some (ids_to_terms, ids_to_father_ids,_) ->
2026 refresh_sequent notebook ;
2027 refresh_proof output
2028 | None -> assert false (* "ERROR: No current term!!!" *)
2030 RefreshSequentException e ->
2031 output_html outputhtml
2032 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2033 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2034 ProofEngine.proof := savedproof ;
2035 ProofEngine.goal := savedgoal ;
2036 refresh_sequent notebook
2037 | RefreshProofException e ->
2038 output_html outputhtml
2039 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2040 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2041 ProofEngine.proof := savedproof ;
2042 ProofEngine.goal := savedgoal ;
2043 refresh_sequent notebook ;
2044 refresh_proof output
2046 output_html outputhtml
2047 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2048 ProofEngine.proof := savedproof ;
2049 ProofEngine.goal := savedgoal
2052 let call_tactic_with_input_and_goal_input tactic () =
2053 let module L = LogicalOperations in
2054 let module G = Gdome in
2055 let notebook = (rendering_window ())#notebook in
2056 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2057 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2058 let inputt = ((rendering_window ())#inputt : term_editor) in
2059 let savedproof = !ProofEngine.proof in
2060 let savedgoal = !ProofEngine.goal in
2061 match notebook#proofw#get_selections with
2064 ((node : Gdome.element)#getAttributeNS
2065 ~namespaceURI:helmns
2066 ~localName:(G.domString "xref"))#to_string
2068 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2072 match !current_goal_infos with
2073 Some (ids_to_terms, ids_to_father_ids,_) ->
2075 let uri,metasenv,bo,ty =
2076 match !ProofEngine.proof with
2077 None -> assert false
2078 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2080 let canonical_context =
2081 match !ProofEngine.goal with
2082 None -> assert false
2084 let (_,canonical_context,_) =
2085 List.find (function (m,_,_) -> m=metano) metasenv
2087 canonical_context in
2088 let (metasenv',expr) =
2089 inputt#get_metasenv_and_term canonical_context metasenv
2091 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2092 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2094 refresh_sequent notebook ;
2095 refresh_proof output ;
2097 | None -> assert false (* "ERROR: No current term!!!" *)
2099 RefreshSequentException e ->
2100 output_html outputhtml
2101 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2102 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2103 ProofEngine.proof := savedproof ;
2104 ProofEngine.goal := savedgoal ;
2105 refresh_sequent notebook
2106 | RefreshProofException e ->
2107 output_html outputhtml
2108 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2109 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2110 ProofEngine.proof := savedproof ;
2111 ProofEngine.goal := savedgoal ;
2112 refresh_sequent notebook ;
2113 refresh_proof output
2115 output_html outputhtml
2116 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2117 ProofEngine.proof := savedproof ;
2118 ProofEngine.goal := savedgoal ;
2121 output_html outputhtml
2122 ("<h1 color=\"red\">No term selected</h1>")
2124 output_html outputhtml
2125 ("<h1 color=\"red\">Many terms selected</h1>")
2128 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2129 let module L = LogicalOperations in
2130 let module G = Gdome in
2132 (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
2133 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2134 let savedproof = !ProofEngine.proof in
2135 let savedgoal = !ProofEngine.goal in
2136 match mmlwidget#get_selections with
2139 ((node : Gdome.element)#getAttributeNS
2140 ~namespaceURI:helmns
2141 ~localName:(G.domString "xref"))#to_string
2143 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2147 match !current_scratch_infos with
2148 (* term is the whole goal in the scratch_area *)
2149 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2151 let expr = tactic term (Hashtbl.find ids_to_terms id) in
2152 let mml = mml_of_cic_term 111 expr in
2153 scratch_window#show () ;
2154 scratch_window#mmlwidget#load_doc ~dom:mml
2155 | None -> assert false (* "ERROR: No current term!!!" *)
2158 output_html outputhtml
2159 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2162 output_html outputhtml
2163 ("<h1 color=\"red\">No term selected</h1>")
2165 output_html outputhtml
2166 ("<h1 color=\"red\">Many terms selected</h1>")
2169 let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
2170 let module L = LogicalOperations in
2171 let module G = Gdome in
2173 (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
2174 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2175 let savedproof = !ProofEngine.proof in
2176 let savedgoal = !ProofEngine.goal in
2177 match mmlwidget#get_selections with
2179 output_html outputhtml
2180 ("<h1 color=\"red\">No term selected</h1>")
2183 match !current_scratch_infos with
2184 (* term is the whole goal in the scratch_area *)
2185 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2186 let term_of_node node =
2188 ((node : Gdome.element)#getAttributeNS
2189 ~namespaceURI:helmns
2190 ~localName:(G.domString "xref"))#to_string
2192 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2195 Hashtbl.find ids_to_terms id
2197 let terms = List.map term_of_node l in
2198 let expr = tactic terms term in
2199 let mml = mml_of_cic_term 111 expr in
2200 scratch_window#show () ;
2201 scratch_window#mmlwidget#load_doc ~dom:mml
2202 | None -> assert false (* "ERROR: No current term!!!" *)
2205 output_html outputhtml
2206 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2209 let call_tactic_with_hypothesis_input tactic () =
2210 let module L = LogicalOperations in
2211 let module G = Gdome in
2212 let notebook = (rendering_window ())#notebook in
2213 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2214 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2215 let savedproof = !ProofEngine.proof in
2216 let savedgoal = !ProofEngine.goal in
2217 match notebook#proofw#get_selections with
2220 ((node : Gdome.element)#getAttributeNS
2221 ~namespaceURI:helmns
2222 ~localName:(G.domString "xref"))#to_string
2224 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2228 match !current_goal_infos with
2229 Some (_,_,ids_to_hypotheses) ->
2231 tactic (Hashtbl.find ids_to_hypotheses id) ;
2232 refresh_sequent notebook ;
2233 refresh_proof output
2234 | None -> assert false (* "ERROR: No current term!!!" *)
2236 RefreshSequentException e ->
2237 output_html outputhtml
2238 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2239 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2240 ProofEngine.proof := savedproof ;
2241 ProofEngine.goal := savedgoal ;
2242 refresh_sequent notebook
2243 | RefreshProofException e ->
2244 output_html outputhtml
2245 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2246 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2247 ProofEngine.proof := savedproof ;
2248 ProofEngine.goal := savedgoal ;
2249 refresh_sequent notebook ;
2250 refresh_proof output
2252 output_html outputhtml
2253 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2254 ProofEngine.proof := savedproof ;
2255 ProofEngine.goal := savedgoal ;
2258 output_html outputhtml
2259 ("<h1 color=\"red\">No term selected</h1>")
2261 output_html outputhtml
2262 ("<h1 color=\"red\">Many terms selected</h1>")
2266 let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback);;
2267 let exact = call_tactic_with_input ProofEngine.exact;;
2268 let apply = call_tactic_with_input ProofEngine.apply;;
2269 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2270 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2271 let whd = call_tactic_with_goal_inputs ProofEngine.whd;;
2272 let reduce = call_tactic_with_goal_inputs ProofEngine.reduce;;
2273 let simpl = call_tactic_with_goal_inputs ProofEngine.simpl;;
2274 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2275 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2276 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2277 let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback);;
2278 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2279 let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback);;
2280 let ring = call_tactic ProofEngine.ring;;
2281 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2282 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2283 let fourier = call_tactic ProofEngine.fourier;;
2284 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2285 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
2286 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
2287 let reflexivity = call_tactic ProofEngine.reflexivity;;
2288 let symmetry = call_tactic ProofEngine.symmetry;;
2289 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2290 let exists = call_tactic ProofEngine.exists;;
2291 let split = call_tactic ProofEngine.split;;
2292 let left = call_tactic ProofEngine.left;;
2293 let right = call_tactic ProofEngine.right;;
2294 let assumption = call_tactic ProofEngine.assumption;;
2295 let generalize = call_tactic_with_goal_inputs ProofEngine.generalize;;
2296 let absurd = call_tactic_with_input ProofEngine.absurd;;
2297 let contradiction = call_tactic ProofEngine.contradiction;;
2299 call_tactic_with_input
2300 (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);;
2302 let whd_in_scratch scratch_window =
2303 call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
2306 let reduce_in_scratch scratch_window =
2307 call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
2310 let simpl_in_scratch scratch_window =
2311 call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
2317 (**********************)
2318 (* END OF TACTICS *)
2319 (**********************)
2323 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2325 show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2328 output_html outputhtml
2329 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2332 exception NotADefinition;;
2335 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2336 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2337 let notebook = (rendering_window ())#notebook in
2339 let uri = input_or_locate_uri ~title:"Open" in
2340 CicTypeChecker.typecheck uri ;
2341 let metasenv,bo,ty =
2342 match CicEnvironment.get_cooked_obj uri with
2343 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2344 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2347 | Cic.InductiveDefinition _ -> raise NotADefinition
2349 ProofEngine.proof :=
2350 Some (uri, metasenv, bo, ty) ;
2351 ProofEngine.goal := None ;
2352 refresh_sequent notebook ;
2353 refresh_proof output
2355 RefreshSequentException e ->
2356 output_html outputhtml
2357 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2358 "sequent: " ^ Printexc.to_string e ^ "</h1>")
2359 | RefreshProofException e ->
2360 output_html outputhtml
2361 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2362 "proof: " ^ Printexc.to_string e ^ "</h1>")
2364 output_html outputhtml
2365 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2368 let show_query_results results =
2371 ~modal:false ~title:"Query results." ~border_width:2 () in
2372 let vbox = GPack.vbox ~packing:window#add () in
2374 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2377 ~text:"Click on a URI to show that object"
2378 ~packing:hbox#add () in
2379 let scrolled_window =
2380 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2381 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2382 let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2385 (function (uri,_) ->
2389 clist#set_row ~selectable:false n
2392 clist#columns_autosize () ;
2394 (clist#connect#select_row
2395 (fun ~row ~column ~event ->
2396 let (uristr,_) = List.nth results row in
2398 Disambiguate.cic_textual_parser_uri_of_string
2399 (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
2402 CicTextualParser0.ConUri uri
2403 | CicTextualParser0.VarUri uri
2404 | CicTextualParser0.IndTyUri (uri,_)
2405 | CicTextualParser0.IndConUri (uri,_,_) ->
2406 show_in_show_window_uri uri
2412 let refine_constraints (must_obj,must_rel,must_sort) =
2413 let chosen = ref false in
2414 let use_only = ref false in
2417 ~modal:true ~title:"Constraints refinement."
2418 ~width:800 ~border_width:2 () in
2419 let vbox = GPack.vbox ~packing:window#add () in
2421 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2424 ~text: "\"Only\" constraints can be enforced or not."
2425 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2427 GButton.toggle_button ~label:"Enforce \"only\" constraints"
2428 ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2431 (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2432 (* Notebook for the constraints choice *)
2434 GPack.notebook ~scrollable:true
2435 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2436 (* Rel constraints *)
2439 ~text: "Constraints on Rels" () in
2441 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2444 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2447 ~text: "You can now specify the constraints on Rels."
2448 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2449 let expected_height = 25 * (List.length must_rel + 2) in
2450 let height = if expected_height > 400 then 400 else expected_height in
2451 let scrolled_window =
2452 GBin.scrolled_window ~border_width:10 ~height ~width:600
2453 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2454 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2455 let rel_constraints =
2457 (function (position,depth) ->
2460 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2464 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2466 None -> position, ref None
2468 let mutable_ref = ref (Some depth') in
2470 GButton.toggle_button
2471 ~label:("depth = " ^ string_of_int depth') ~active:true
2472 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2475 (depthb#connect#toggled
2477 let sel_depth = if depthb#active then Some depth' else None in
2478 mutable_ref := sel_depth
2480 position, mutable_ref
2482 (* Sort constraints *)
2485 ~text: "Constraints on Sorts" () in
2487 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2490 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2493 ~text: "You can now specify the constraints on Sorts."
2494 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2495 let expected_height = 25 * (List.length must_sort + 2) in
2496 let height = if expected_height > 400 then 400 else expected_height in
2497 let scrolled_window =
2498 GBin.scrolled_window ~border_width:10 ~height ~width:600
2499 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2500 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2501 let sort_constraints =
2503 (function (position,depth,sort) ->
2506 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2509 ~text:(sort ^ " " ^ position)
2510 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2512 None -> position, ref None, sort
2514 let mutable_ref = ref (Some depth') in
2516 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2518 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2521 (depthb#connect#toggled
2523 let sel_depth = if depthb#active then Some depth' else None in
2524 mutable_ref := sel_depth
2526 position, mutable_ref, sort
2528 (* Obj constraints *)
2531 ~text: "Constraints on constants" () in
2533 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2536 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2539 ~text: "You can now specify the constraints on constants."
2540 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2541 let expected_height = 25 * (List.length must_obj + 2) in
2542 let height = if expected_height > 400 then 400 else expected_height in
2543 let scrolled_window =
2544 GBin.scrolled_window ~border_width:10 ~height ~width:600
2545 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2546 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2547 let obj_constraints =
2549 (function (uri,position,depth) ->
2552 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2555 ~text:(uri ^ " " ^ position)
2556 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2558 None -> uri, position, ref None
2560 let mutable_ref = ref (Some depth') in
2562 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2564 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2567 (depthb#connect#toggled
2569 let sel_depth = if depthb#active then Some depth' else None in
2570 mutable_ref := sel_depth
2572 uri, position, mutable_ref
2574 (* Confirm/abort buttons *)
2576 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2578 GButton.button ~label:"Ok"
2579 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2581 GButton.button ~label:"Abort"
2582 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2584 ignore (window#connect#destroy GMain.Main.quit) ;
2585 ignore (cancelb#connect#clicked window#destroy) ;
2587 (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2588 window#set_position `CENTER ;
2590 GMain.Main.main () ;
2592 let chosen_must_rel =
2594 (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2595 let chosen_must_sort =
2597 (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2600 let chosen_must_obj =
2602 (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2605 (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2607 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2608 Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2616 let completeSearchPattern () =
2617 let inputt = ((rendering_window ())#inputt : term_editor) in
2618 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2620 let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
2621 let must = MQueryLevels2.get_constraints expr in
2622 let must',only = refine_constraints must in
2623 let results = MQueryGenerator.searchPattern must' only in
2624 show_query_results results
2627 output_html outputhtml
2628 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2631 let insertQuery () =
2632 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2634 let chosen = ref None in
2637 ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
2638 let vbox = GPack.vbox ~packing:window#add () in
2640 GMisc.label ~text:"Insert Query. For Experts Only."
2641 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2642 let scrolled_window =
2643 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2644 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2645 let input = GEdit.text ~editable:true
2646 ~packing:scrolled_window#add () in
2648 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2650 GButton.button ~label:"Ok"
2651 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2653 GButton.button ~label:"Load from file..."
2654 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2656 GButton.button ~label:"Abort"
2657 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2658 ignore (window#connect#destroy GMain.Main.quit) ;
2659 ignore (cancelb#connect#clicked window#destroy) ;
2661 (okb#connect#clicked
2663 chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
2665 (loadb#connect#clicked
2668 GToolbox.select_file ~title:"Select Query File" ()
2672 let inch = open_in filename in
2673 let rec read_file () =
2675 let line = input_line inch in
2676 line ^ "\n" ^ read_file ()
2680 let text = read_file () in
2681 input#delete_text 0 input#length ;
2682 ignore (input#insert_text text ~pos:0))) ;
2683 window#set_position `CENTER ;
2685 GMain.Main.main () ;
2690 Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
2692 show_query_results results
2695 output_html outputhtml
2696 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2699 let choose_must list_of_must only =
2700 let chosen = ref None in
2701 let user_constraints = ref [] in
2704 ~modal:true ~title:"Query refinement." ~border_width:2 () in
2705 let vbox = GPack.vbox ~packing:window#add () in
2707 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2711 ("You can now specify the genericity of the query. " ^
2712 "The more generic the slower.")
2713 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2715 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2719 "Suggestion: start with faster queries before moving to more generic ones."
2720 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2722 GPack.notebook ~scrollable:true
2723 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2726 let last = List.length list_of_must in
2732 (if !page = 1 then "More generic" else
2733 if !page = last then "More precise" else " ") () in
2734 let expected_height = 25 * (List.length must + 2) in
2735 let height = if expected_height > 400 then 400 else expected_height in
2736 let scrolled_window =
2737 GBin.scrolled_window ~border_width:10 ~height ~width:600
2738 ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2740 GList.clist ~columns:2 ~packing:scrolled_window#add
2741 ~titles:["URI" ; "Position"] ()
2745 (function (uri,position) ->
2748 [uri; if position then "MainConclusion" else "Conclusion"]
2750 clist#set_row ~selectable:false n
2753 clist#columns_autosize ()
2756 let label = GMisc.label ~text:"User provided" () in
2758 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2760 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2763 ~text:"Select the constraints that must be satisfied and press OK."
2764 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2765 let expected_height = 25 * (List.length only + 2) in
2766 let height = if expected_height > 400 then 400 else expected_height in
2767 let scrolled_window =
2768 GBin.scrolled_window ~border_width:10 ~height ~width:600
2769 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2771 GList.clist ~columns:2 ~packing:scrolled_window#add
2772 ~selection_mode:`EXTENDED
2773 ~titles:["URI" ; "Position"] ()
2777 (function (uri,position) ->
2780 [uri; if position then "MainConclusion" else "Conclusion"]
2782 clist#set_row ~selectable:true n
2785 clist#columns_autosize () ;
2787 (clist#connect#select_row
2788 (fun ~row ~column ~event ->
2789 user_constraints := (List.nth only row)::!user_constraints)) ;
2791 (clist#connect#unselect_row
2792 (fun ~row ~column ~event ->
2795 (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2798 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2800 GButton.button ~label:"Ok"
2801 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2803 GButton.button ~label:"Abort"
2804 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2806 ignore (window#connect#destroy GMain.Main.quit) ;
2807 ignore (cancelb#connect#clicked window#destroy) ;
2809 (okb#connect#clicked
2810 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2811 window#set_position `CENTER ;
2813 GMain.Main.main () ;
2815 None -> raise NoChoice
2817 if n = List.length list_of_must then
2818 (* user provided constraints *)
2821 List.nth list_of_must n
2824 let searchPattern () =
2825 let inputt = ((rendering_window ())#inputt : term_editor) in
2826 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2829 match !ProofEngine.proof with
2830 None -> assert false
2831 | Some (_,metasenv,_,_) -> metasenv
2833 match !ProofEngine.goal with
2836 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2837 let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2838 let must = choose_must list_of_must only in
2839 let torigth_restriction (u,b) =
2842 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2844 "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2848 let rigth_must = List.map torigth_restriction must in
2849 let rigth_only = Some (List.map torigth_restriction only) in
2851 MQueryGenerator.searchPattern
2852 (rigth_must,[],[]) (rigth_only,None,None) in
2856 Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri
2859 " <h1>Backward Query: </h1>" ^
2860 " <pre>" ^ get_last_query result ^ "</pre>"
2862 output_html outputhtml html ;
2864 let rec filter_out =
2868 let tl',exc = filter_out tl in
2871 ProofEngine.can_apply
2872 (term_of_cic_textual_parser_uri
2873 (Disambiguate.cic_textual_parser_uri_of_string uri))
2881 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2882 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2889 " <h1>Objects that can actually be applied: </h1> " ^
2890 String.concat "<br>" uris' ^ exc ^
2891 " <h1>Number of false matches: " ^
2892 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2893 " <h1>Number of good matches: " ^
2894 string_of_int (List.length uris') ^ "</h1>"
2896 output_html outputhtml html' ;
2898 user_uri_choice ~title:"Ambiguous input."
2900 "Many lemmas can be successfully applied. Please, choose one:"
2903 inputt#set_term uri' ;
2907 output_html outputhtml
2908 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2911 let choose_selection mmlwidget (element : Gdome.element option) =
2912 let module G = Gdome in
2913 let rec aux element =
2914 if element#hasAttributeNS
2915 ~namespaceURI:helmns
2916 ~localName:(G.domString "xref")
2918 mmlwidget#set_selection (Some element)
2921 match element#get_parentNode with
2922 None -> assert false
2923 (*CSC: OCAML DIVERGES!
2924 | Some p -> aux (new G.element_of_node p)
2926 | Some p -> aux (new Gdome.element_of_node p)
2928 GdomeInit.DOMCastException _ ->
2930 "******* trying to select above the document root ********"
2934 | None -> mmlwidget#set_selection None
2937 (* STUFF TO BUILD THE GTK INTERFACE *)
2939 (* Stuff for the widget settings *)
2941 let export_to_postscript (output : GMathViewAux.single_selection_math_view) =
2942 let lastdir = ref (Unix.getcwd ()) in
2945 GToolbox.select_file ~title:"Export to PostScript"
2946 ~dir:lastdir ~filename:"screenshot.ps" ()
2950 output#export_to_postscript ~filename:filename ();
2953 let activate_t1 (output : GMathViewAux.single_selection_math_view) button_set_anti_aliasing
2954 button_set_transparency export_to_postscript_menu_item
2957 let is_set = button_t1#active in
2958 output#set_font_manager_type
2959 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2962 button_set_anti_aliasing#misc#set_sensitive true ;
2963 button_set_transparency#misc#set_sensitive true ;
2964 export_to_postscript_menu_item#misc#set_sensitive true ;
2968 button_set_anti_aliasing#misc#set_sensitive false ;
2969 button_set_transparency#misc#set_sensitive false ;
2970 export_to_postscript_menu_item#misc#set_sensitive false ;
2974 let set_anti_aliasing output button_set_anti_aliasing () =
2975 output#set_anti_aliasing button_set_anti_aliasing#active
2978 let set_transparency output button_set_transparency () =
2979 output#set_transparency button_set_transparency#active
2982 let changefont output font_size_spinb () =
2983 output#set_font_size font_size_spinb#value_as_int
2986 let set_log_verbosity output log_verbosity_spinb () =
2987 output#set_log_verbosity log_verbosity_spinb#value_as_int
2990 class settings_window (output : GMathViewAux.single_selection_math_view) sw
2991 export_to_postscript_menu_item selection_changed_callback
2993 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2995 GPack.vbox ~packing:settings_window#add () in
2998 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2999 ~border_width:5 ~packing:vbox#add () in
3001 GButton.toggle_button ~label:"activate t1 fonts"
3002 ~packing:(table#attach ~left:0 ~top:0) () in
3003 let button_set_anti_aliasing =
3004 GButton.toggle_button ~label:"set_anti_aliasing"
3005 ~packing:(table#attach ~left:0 ~top:1) () in
3006 let button_set_transparency =
3007 GButton.toggle_button ~label:"set_transparency"
3008 ~packing:(table#attach ~left:2 ~top:1) () in
3011 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
3012 ~border_width:5 ~packing:vbox#add () in
3013 let font_size_label =
3014 GMisc.label ~text:"font size:"
3015 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
3016 let font_size_spinb =
3018 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
3021 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
3022 let log_verbosity_label =
3023 GMisc.label ~text:"log verbosity:"
3024 ~packing:(table#attach ~left:0 ~top:1) () in
3025 let log_verbosity_spinb =
3027 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
3030 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
3032 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3034 GButton.button ~label:"Close"
3035 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3037 method show = settings_window#show
3039 button_set_anti_aliasing#misc#set_sensitive false ;
3040 button_set_transparency#misc#set_sensitive false ;
3041 (* Signals connection *)
3042 ignore(button_t1#connect#clicked
3043 (activate_t1 output button_set_anti_aliasing
3044 button_set_transparency export_to_postscript_menu_item button_t1)) ;
3045 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
3046 ignore(button_set_anti_aliasing#connect#toggled
3047 (set_anti_aliasing output button_set_anti_aliasing));
3048 ignore(button_set_transparency#connect#toggled
3049 (set_transparency output button_set_transparency)) ;
3050 ignore(log_verbosity_spinb#connect#changed
3051 (set_log_verbosity output log_verbosity_spinb)) ;
3052 ignore(closeb#connect#clicked settings_window#misc#hide)
3055 (* Scratch window *)
3057 class scratch_window =
3059 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
3061 GPack.vbox ~packing:window#add () in
3063 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3065 GButton.button ~label:"Whd"
3066 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3068 GButton.button ~label:"Reduce"
3069 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3071 GButton.button ~label:"Simpl"
3072 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3073 let scrolled_window =
3074 GBin.scrolled_window ~border_width:10
3075 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3077 GMathViewAux.multi_selection_math_view
3078 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
3080 method mmlwidget = mmlwidget
3081 method show () = window#misc#hide () ; window#show ()
3083 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
3084 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
3085 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
3086 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
3087 ignore(simplb#connect#clicked (simpl_in_scratch self))
3090 let open_contextual_menu_for_selected_terms mmlwidget infos =
3091 let button = GdkEvent.Button.button infos in
3092 let terms_selected = List.length mmlwidget#get_selections > 0 in
3095 let time = GdkEvent.Button.time infos in
3096 let menu = GMenu.menu () in
3097 let f = new GMenu.factory menu in
3099 f#add_item "Whd" ~key:GdkKeysyms._W ~callback:whd in
3100 let reduce_menu_item =
3101 f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:reduce in
3102 let simpl_menu_item =
3103 f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:simpl in
3104 let _ = f#add_separator () in
3105 let generalize_menu_item =
3106 f#add_item "Generalize" ~key:GdkKeysyms._G ~callback:generalize
3108 whd_menu_item#misc#set_sensitive terms_selected ;
3109 reduce_menu_item#misc#set_sensitive terms_selected ;
3110 simpl_menu_item#misc#set_sensitive terms_selected ;
3111 generalize_menu_item#misc#set_sensitive terms_selected ;
3112 menu#popup ~button ~time
3118 let vbox1 = GPack.vbox () in
3120 val mutable proofw_ref = None
3121 val mutable compute_ref = None
3123 Lazy.force self#compute ;
3124 match proofw_ref with
3125 None -> assert false
3126 | Some proofw -> proofw
3127 method content = vbox1
3129 match compute_ref with
3130 None -> assert false
3131 | Some compute -> compute
3135 let scrolled_window1 =
3136 GBin.scrolled_window ~border_width:10
3137 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3139 GMathViewAux.multi_selection_math_view ~width:400 ~height:275
3140 ~packing:(scrolled_window1#add) () in
3141 let _ = proofw_ref <- Some proofw in
3143 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3145 GButton.button ~label:"Exact"
3146 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3148 GButton.button ~label:"Intros"
3149 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3151 GButton.button ~label:"Apply"
3152 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3153 let elimintrossimplb =
3154 GButton.button ~label:"ElimIntrosSimpl"
3155 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3157 GButton.button ~label:"ElimType"
3158 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3159 (* Zack: spostare in una toolbar
3161 GButton.button ~label:"Whd"
3162 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3164 GButton.button ~label:"Reduce"
3165 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3167 GButton.button ~label:"Simpl"
3168 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3171 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3173 GButton.button ~label:"Fold_whd"
3174 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3176 GButton.button ~label:"Fold_reduce"
3177 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3179 GButton.button ~label:"Fold_simpl"
3180 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3182 GButton.button ~label:"Cut"
3183 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3185 GButton.button ~label:"Change"
3186 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3188 GButton.button ~label:"Let ... In"
3189 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3191 GButton.button ~label:"Ring"
3192 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3194 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3196 GButton.button ~label:"ClearBody"
3197 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3199 GButton.button ~label:"Clear"
3200 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3202 GButton.button ~label:"Fourier"
3203 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3205 GButton.button ~label:"RewriteSimpl ->"
3206 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3207 let rewritebacksimplb =
3208 GButton.button ~label:"RewriteSimpl <-"
3209 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3211 GButton.button ~label:"Replace"
3212 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3214 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3216 GButton.button ~label:"Reflexivity"
3217 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3219 GButton.button ~label:"Symmetry"
3220 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3222 GButton.button ~label:"Transitivity"
3223 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3225 GButton.button ~label:"Exists"
3226 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3228 GButton.button ~label:"Split"
3229 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3231 GButton.button ~label:"Left"
3232 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3234 GButton.button ~label:"Right"
3235 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3237 GButton.button ~label:"Assumption"
3238 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3240 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3241 (* Zack: spostare in una toolbar
3243 GButton.button ~label:"Generalize"
3244 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3247 GButton.button ~label:"Absurd"
3248 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3249 let contradictionb =
3250 GButton.button ~label:"Contradiction"
3251 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3252 let searchpatternb =
3253 GButton.button ~label:"SearchPattern_Apply"
3254 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3256 GButton.button ~label:"Decompose"
3257 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3259 ignore(exactb#connect#clicked exact) ;
3260 ignore(applyb#connect#clicked apply) ;
3261 ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3262 ignore(elimtypeb#connect#clicked elimtype) ;
3263 (* Zack: spostare in una toolbar
3264 ignore(whdb#connect#clicked whd) ;
3265 ignore(reduceb#connect#clicked reduce) ;
3266 ignore(simplb#connect#clicked simpl) ;
3268 ignore(foldwhdb#connect#clicked fold_whd) ;
3269 ignore(foldreduceb#connect#clicked fold_reduce) ;
3270 ignore(foldsimplb#connect#clicked fold_simpl) ;
3271 ignore(cutb#connect#clicked cut) ;
3272 ignore(changeb#connect#clicked change) ;
3273 ignore(letinb#connect#clicked letin) ;
3274 ignore(ringb#connect#clicked ring) ;
3275 ignore(clearbodyb#connect#clicked clearbody) ;
3276 ignore(clearb#connect#clicked clear) ;
3277 ignore(fourierb#connect#clicked fourier) ;
3278 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3279 ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
3280 ignore(replaceb#connect#clicked replace) ;
3281 ignore(reflexivityb#connect#clicked reflexivity) ;
3282 ignore(symmetryb#connect#clicked symmetry) ;
3283 ignore(transitivityb#connect#clicked transitivity) ;
3284 ignore(existsb#connect#clicked exists) ;
3285 ignore(splitb#connect#clicked split) ;
3286 ignore(leftb#connect#clicked left) ;
3287 ignore(rightb#connect#clicked right) ;
3288 ignore(assumptionb#connect#clicked assumption) ;
3289 (* Zack: spostare in una toolbar
3290 ignore(generalizeb#connect#clicked generalize) ;
3292 ignore(absurdb#connect#clicked absurd) ;
3293 ignore(contradictionb#connect#clicked contradiction) ;
3294 ignore(introsb#connect#clicked intros) ;
3295 ignore(searchpatternb#connect#clicked searchPattern) ;
3296 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3298 ((new GObj.event_ops proofw#as_widget)#connect#button_press
3299 (open_contextual_menu_for_selected_terms proofw)) ;
3300 ignore(decomposeb#connect#clicked decompose) ;
3306 let vbox1 = GPack.vbox () in
3307 let scrolled_window1 =
3308 GBin.scrolled_window ~border_width:10
3309 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3311 GMathViewAux.single_selection_math_view ~width:400 ~height:275
3312 ~packing:(scrolled_window1#add) () in
3314 method proofw = (assert false : GMathViewAux.single_selection_math_view)
3315 method content = vbox1
3316 method compute = (assert false : unit)
3320 let empty_page = new empty_page;;
3324 val notebook = GPack.notebook ()
3326 val mutable skip_switch_page_event = false
3327 val mutable empty = true
3328 method notebook = notebook
3330 let new_page = new page () in
3332 pages := !pages @ [n,lazy (setgoal n),new_page] ;
3333 notebook#append_page
3334 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3335 new_page#content#coerce
3336 method remove_all_pages ~skip_switch_page_event:skip =
3338 notebook#remove_page 0 (* let's remove the empty page *)
3340 List.iter (function _ -> notebook#remove_page 0) !pages ;
3342 skip_switch_page_event <- skip
3343 method set_current_page ~may_skip_switch_page_event n =
3344 let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3345 let new_page = notebook#page_num page#content#coerce in
3346 if may_skip_switch_page_event && new_page <> notebook#current_page then
3347 skip_switch_page_event <- true ;
3348 notebook#goto_page new_page
3349 method set_empty_page =
3352 notebook#append_page
3353 ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3354 empty_page#content#coerce
3356 let (_,_,page) = List.nth !pages notebook#current_page in
3360 (notebook#connect#switch_page
3362 let skip = skip_switch_page_event in
3363 skip_switch_page_event <- false ;
3366 let (metano,setgoal,page) = List.nth !pages i in
3367 ProofEngine.goal := Some metano ;
3368 Lazy.force (page#compute) ;
3377 class rendering_window output (notebook : notebook) =
3378 let scratch_window = new scratch_window in
3380 GWindow.window ~title:"MathML viewer" ~border_width:0
3381 ~allow_shrink:false () in
3382 let vbox_for_menu = GPack.vbox ~packing:window#add () in
3384 let handle_box = GBin.handle_box ~border_width:2
3385 ~packing:(vbox_for_menu#pack ~padding:0) () in
3386 let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3387 let factory0 = new GMenu.factory menubar in
3388 let accel_group = factory0#accel_group in
3390 let file_menu = factory0#add_submenu "File" in
3391 let factory1 = new GMenu.factory file_menu ~accel_group in
3392 let export_to_postscript_menu_item =
3395 factory1#add_item "New Block of (Co)Inductive Definitions..."
3396 ~key:GdkKeysyms._B ~callback:new_inductive
3399 factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3402 let reopen_menu_item =
3403 factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3407 factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3408 ignore (factory1#add_separator ()) ;
3410 (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3412 let save_menu_item =
3413 factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3416 (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3417 ignore (!save_set_sensitive false);
3418 ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3419 ignore (!qed_set_sensitive false);
3420 ignore (factory1#add_separator ()) ;
3421 let export_to_postscript_menu_item =
3422 factory1#add_item "Export to PostScript..."
3423 ~callback:(export_to_postscript output) in
3424 ignore (factory1#add_separator ()) ;
3426 (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3427 export_to_postscript_menu_item
3430 let edit_menu = factory0#add_submenu "Edit Current Proof" in
3431 let factory2 = new GMenu.factory edit_menu ~accel_group in
3432 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3433 let proveit_menu_item =
3434 factory2#add_item "Prove It" ~key:GdkKeysyms._I
3435 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3437 let focus_menu_item =
3438 factory2#add_item "Focus" ~key:GdkKeysyms._F
3439 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3442 focus_and_proveit_set_sensitive :=
3444 proveit_menu_item#misc#set_sensitive b ;
3445 focus_menu_item#misc#set_sensitive b
3447 let _ = !focus_and_proveit_set_sensitive false in
3448 (* edit term menu *)
3449 let edit_term_menu = factory0#add_submenu "Edit Term" in
3450 let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3451 let check_menu_item =
3452 factory5#add_item "Check Term" ~key:GdkKeysyms._C
3453 ~callback:(check scratch_window) in
3454 let _ = check_menu_item#misc#set_sensitive false in
3456 let settings_menu = factory0#add_submenu "Search" in
3457 let factory4 = new GMenu.factory settings_menu ~accel_group in
3459 factory4#add_item "Locate..." ~key:GdkKeysyms._T
3461 let searchPattern_menu_item =
3462 factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3463 ~callback:completeSearchPattern in
3464 let _ = searchPattern_menu_item#misc#set_sensitive false in
3465 let show_menu_item =
3466 factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3468 let insert_query_item =
3469 factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
3470 ~callback:insertQuery in
3472 let settings_menu = factory0#add_submenu "Settings" in
3473 let factory3 = new GMenu.factory settings_menu ~accel_group in
3475 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3476 ~callback:edit_aliases in
3477 let _ = factory3#add_separator () in
3479 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3480 ~callback:(function _ -> (settings_window ())#show ()) in
3482 let _ = window#add_accel_group accel_group in
3486 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3488 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3489 let scrolled_window0 =
3490 GBin.scrolled_window ~border_width:10
3491 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3492 let _ = scrolled_window0#add output#coerce in
3494 GBin.frame ~label:"Insert Term"
3495 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3496 let scrolled_window1 =
3497 GBin.scrolled_window ~border_width:5
3498 ~packing:frame#add () in
3500 new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3501 ~isnotempty_callback:
3503 check_menu_item#misc#set_sensitive b ;
3504 searchPattern_menu_item#misc#set_sensitive b) in
3506 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3508 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3510 GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3514 ~source:"<html><body bgColor=\"white\"></body></html>"
3515 ~width:400 ~height: 100
3520 method outputhtml = outputhtml
3521 method inputt = inputt
3522 method output = (output : GMathViewAux.single_selection_math_view)
3523 method notebook = notebook
3524 method show = window#show
3526 notebook#set_empty_page ;
3527 export_to_postscript_menu_item#misc#set_sensitive false ;
3528 check_term := (check_term_in_scratch scratch_window) ;
3530 (* signal handlers here *)
3531 ignore(output#connect#selection_changed
3533 choose_selection output elem ;
3534 !focus_and_proveit_set_sensitive true
3536 ignore (output#connect#click (show_in_show_window_callback output)) ;
3537 let settings_window = new settings_window output scrolled_window0
3538 export_to_postscript_menu_item (choose_selection output) in
3539 set_settings_window settings_window ;
3540 set_outputhtml outputhtml ;
3541 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3542 Logger.log_callback :=
3543 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3548 let initialize_everything () =
3549 let module U = Unix in
3550 let output = GMathViewAux.single_selection_math_view ~width:350 ~height:280 () in
3551 let notebook = new notebook in
3552 let rendering_window' = new rendering_window output notebook in
3553 set_rendering_window rendering_window' ;
3554 mml_of_cic_term_ref := mml_of_cic_term ;
3555 rendering_window'#show () ;
3562 Mqint.set_database Mqint.postgres_db ;
3563 Mqint.init postgresqlconnectionstring ;
3565 ignore (GtkMain.Main.init ()) ;
3566 initialize_everything () ;
3567 if !usedb then Mqint.close ();