X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;fp=helm%2FgTopLevel%2FgTopLevel.ml;h=0000000000000000000000000000000000000000;hp=bda4c4b826126a2caf354bfdd5e7838227e6f8d6;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml deleted file mode 100644 index bda4c4b82..000000000 --- a/helm/gTopLevel/gTopLevel.ml +++ /dev/null @@ -1,2891 +0,0 @@ -(* Copyright (C) 2000-2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) - -let debug_level = ref 1 -let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s -let error s = prerr_endline ("E: " ^ s) -let warning s = prerr_endline ("W: " ^ s) - -open Printf - -(* DEBUGGING *) - -module MQI = MQueryInterpreter -module MQIC = MQIConn -module MQGT = MQGTypes -module MQGU = MQGUtil -module MQG = MQueryGenerator - - -(* first of all let's initialize the Helm_registry *) -let _ = - let configuration_file = "gTopLevel.conf.xml" in - if not (Sys.file_exists configuration_file) then begin - eprintf "E: Can't find configuration file '%s'\n" configuration_file; - exit 2 - end; - Helm_registry.load_from configuration_file -;; - -(* GLOBAL CONSTANTS *) - -let mqi_debug_fun s = debug_print ~level:2 s -let mqi_handle = MQIC.init ~log:mqi_debug_fun () - -let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; - -let restore_environment_on_boot = true ;; -let notify_hbugs_on_goal_change = false ;; - -let auto_disambiguation = ref true ;; - -(* GLOBAL REFERENCES (USED BY CALLBACKS) *) - -let check_term = ref (fun _ _ _ -> assert false);; - -exception RenderingWindowsNotInitialized;; - -let set_rendering_window,rendering_window = - let rendering_window_ref = ref None in - (function rw -> rendering_window_ref := Some rw), - (function () -> - match !rendering_window_ref with - None -> raise RenderingWindowsNotInitialized - | Some rw -> rw - ) -;; - -exception SettingsWindowsNotInitialized;; - -let set_settings_window,settings_window = - let settings_window_ref = ref None in - (function rw -> settings_window_ref := Some rw), - (function () -> - match !settings_window_ref with - None -> raise SettingsWindowsNotInitialized - | Some rw -> rw - ) -;; - -exception QedSetSensitiveNotInitialized;; -let qed_set_sensitive = - ref (function _ -> raise QedSetSensitiveNotInitialized) -;; - -exception SaveSetSensitiveNotInitialized;; -let save_set_sensitive = - ref (function _ -> raise SaveSetSensitiveNotInitialized) -;; - -(* COMMAND LINE OPTIONS *) - -let usedb = ref true - -let argspec = - [ - "-nodb", Arg.Clear usedb, "disable use of MathQL DB" - ] -in -Arg.parse argspec ignore "" - -(* MISC FUNCTIONS *) - -let term_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - match uri with - CTP.ConUri uri -> C.Const (uri,[]) - | CTP.VarUri uri -> C.Var (uri,[]) - | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) - | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) -;; - -let string_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - let uri' = - match uri with - CTP.ConUri uri -> UriManager.string_of_uri uri - | CTP.VarUri uri -> UriManager.string_of_uri uri - | CTP.IndTyUri (uri,tyno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) - | CTP.IndConUri (uri,tyno,consno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ - string_of_int consno - in - (* 4 = String.length "cic:" *) - String.sub uri' 4 (String.length uri' - 4) -;; - -(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) - -(* Check window *) - -let check_window uris = - let window = - GWindow.window - ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in - let notebook = - GPack.notebook ~scrollable:true ~packing:window#add () in - window#show () ; - let render_terms = - List.map - (function uri -> - let scrolled_window = - GBin.scrolled_window ~border_width:10 - ~packing: - (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce)) - () - in - lazy - (let mmlwidget = - TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent - ~packing:scrolled_window#add ~width:400 ~height:280 () in - let expr = - let term = - term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri) - in - (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) - in - try - mmlwidget#load_sequent [] (111,[],expr) - with - e -> - HelmLogger.log (`Error (`T (Printexc.to_string e))) - ) - ) uris - in - ignore - (notebook#connect#switch_page - (function i -> - Lazy.force (List.nth render_terms i))) -;; - -exception NoChoice;; - -let interactive_user_uri_choice - ~(selection_mode:[ `SINGLE | `MULTIPLE ]) - ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris -= - let only_constant_choices = - lazy - (List.filter - (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) - uris) - in - if selection_mode <> `SINGLE && !auto_disambiguation then - Lazy.force only_constant_choices - else begin - let choices = ref [] in - let chosen = ref false in - let use_only_constants = ref false in - let window = - GWindow.dialog ~modal:true ~title ~width:600 () in - let lMessage = - GMisc.label ~text:msg - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 - ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in - let clist = - let expected_height = 18 * List.length uris in - let height = if expected_height > 400 then 400 else expected_height in - GList.clist ~columns:1 ~packing:scrolled_window#add - ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in - let _ = List.map (function x -> clist#append [x]) uris in - let hbox2 = - GPack.hbox ~border_width:0 - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let explain_label = - GMisc.label ~text:"None of the above. Try this one:" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let manual_input = - GEdit.entry ~editable:true - ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in - let hbox = - GPack.hbox ~border_width:0 ~packing:window#action_area#add () in - let okb = - GButton.button ~label:ok - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive false in - let nonvarsb = - GButton.button - ~packing: - (function w -> - if enable_button_for_non_vars then - hbox#pack ~expand:false ~fill:false ~padding:5 w) - ~label:"Try constants only" () in - let autob = - GButton.button - ~packing: - (fun w -> - if enable_button_for_non_vars then - hbox#pack ~expand:false ~fill:false ~padding:5 w) - ~label:"Auto" () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox#pack ~padding:5) () in - let _ = checkb#misc#set_sensitive false in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - (* actions *) - let check_callback () = - assert (List.length !choices > 0) ; - check_window !choices - in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; - ignore - (nonvarsb#connect#clicked - (function () -> - use_only_constants := true ; - chosen := true ; - window#destroy () - )) ; - ignore (autob#connect#clicked (fun () -> - auto_disambiguation := true; - (rendering_window ())#set_auto_disambiguation true; - use_only_constants := true ; - chosen := true; - window#destroy ())); - ignore (checkb#connect#clicked check_callback) ; - ignore - (clist#connect#select_row - (fun ~row ~column ~event -> - checkb#misc#set_sensitive true ; - okb#misc#set_sensitive true ; - choices := (List.nth uris row)::!choices)) ; - ignore - (clist#connect#unselect_row - (fun ~row ~column ~event -> - choices := - List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; - ignore - (manual_input#connect#changed - (fun _ -> - if manual_input#text = "" then - begin - choices := [] ; - checkb#misc#set_sensitive false ; - okb#misc#set_sensitive false ; - clist#misc#set_sensitive true - end - else - begin - choices := [manual_input#text] ; - clist#unselect_all () ; - checkb#misc#set_sensitive true ; - okb#misc#set_sensitive true ; - clist#misc#set_sensitive false - end)); - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - if !chosen then - if !use_only_constants then - Lazy.force only_constant_choices - else - if List.length !choices > 0 then !choices else raise NoChoice - else - raise NoChoice - end -;; - -let interactive_interpretation_choice interpretations = - let chosen = ref None in - let window = - GWindow.window - ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in - let vbox = GPack.vbox ~packing:window#add () in - let lMessage = - GMisc.label - ~text: - ("Ambiguous input since there are many well-typed interpretations." ^ - " Please, choose one of them.") - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let notebook = - GPack.notebook ~scrollable:true - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let _ = - List.map - (function interpretation -> - let clist = - let expected_height = 18 * List.length interpretation in - let height = if expected_height > 400 then 400 else expected_height in - GList.clist ~columns:2 ~packing:notebook#append_page ~height - ~titles:["id" ; "URI"] () - in - ignore - (List.map - (function (id,uri) -> - let n = clist#append [id;uri] in - clist#set_row ~selectable:false n - ) interpretation - ) ; - clist#columns_autosize () - ) interpretations in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"Ok" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - (* actions *) - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked - (function () -> chosen := Some notebook#current_page ; window#destroy ())) ; - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - match !chosen with - None -> raise NoChoice - | Some n -> [n] -;; - - -(* MISC FUNCTIONS *) - -let - save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname -= - let name = - let struri = UriManager.string_of_uri uri in - let idx = (String.rindex struri '/') + 1 in - String.sub struri idx (String.length struri - idx) - in - let path = pathname ^ "/" ^ name in - let xml, bodyxml = - Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false - annobj - in - let xmlinnertypes = - Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types - ~ask_dtd_to_the_getter:false - in - (* innertypes *) - let innertypesuri = UriManager.innertypesuri_of_uri uri in - Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ; - Http_getter.register' innertypesuri - (Helm_registry.get "local_library.url" ^ - Str.replace_first (Str.regexp "^cic:") "" - (UriManager.string_of_uri innertypesuri) ^ ".xml" - ) ; - (* constant type / variable / mutual inductive types definition *) - Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ; - Http_getter.register' uri - (Helm_registry.get "local_library.url" ^ - Str.replace_first (Str.regexp "^cic:") "" - (UriManager.string_of_uri uri) ^ ".xml" - ) ; - match bodyxml with - None -> () - | Some bodyxml' -> - (* constant body *) - let bodyuri = - match UriManager.bodyuri_of_uri uri with - None -> assert false - | Some bodyuri -> bodyuri - in - Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; - Http_getter.register' bodyuri - (Helm_registry.get "local_library.url" ^ - Str.replace_first (Str.regexp "^cic:") "" - (UriManager.string_of_uri bodyuri) ^ ".xml" - ) -;; - - -(* CALLBACKS *) - -exception OpenConjecturesStillThere;; -exception WrongProof;; - -let pathname_of_annuri uristring = - Helm_registry.get "local_library.dir" ^ - Str.replace_first (Str.regexp "^cic:") "" uristring -;; - -let make_dirs dirpath = - ignore (Unix.system ("mkdir -p " ^ dirpath)) -;; - -let save_obj uri obj = - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object ~eta_fix:false obj - in - (* let's save the theorem and register it to the getter *) - let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in - make_dirs pathname ; - save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types - pathname -;; - -let qed () = - match ProofEngine.get_proof () with - None -> assert false - | Some (uri,[],bo,ty) -> - let uri = match uri with Some uri -> uri | _ -> assert false in - if - CicReduction.are_convertible [] - (CicTypeChecker.type_of_aux' [] [] bo) ty - then - begin - (*CSC: Wrong: [] is just plainly wrong *) - let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in - let (acic,ids_to_inner_types,ids_to_inner_sorts) = - (rendering_window ())#output#load_proof uri proof - in - !qed_set_sensitive false ; - (* let's save the theorem and register it to the getter *) - let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in - make_dirs pathname ; - save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types - pathname - end - else - raise WrongProof - | _ -> raise OpenConjecturesStillThere -;; - - (** save an unfinished proof on the filesystem *) -let save_unfinished_proof () = - let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in - let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in - let proof_file = Helm_registry.get "gtoplevel.proof_file" in - Xml.pp ~quiet:true xml (Some proof_file_type) ; - HelmLogger.log - (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ; - Xml.pp ~quiet:true bodyxml (Some proof_file) ; - HelmLogger.log - (`Msg (`T ("Current proof body saved to " ^ proof_file))) -;; - -(* Used to typecheck the loaded proofs *) -let typecheck_loaded_proof metasenv bo ty = - let module T = CicTypeChecker in - ignore ( - List.fold_left - (fun metasenv ((_,context,ty) as conj) -> - ignore (T.type_of_aux' metasenv context ty) ; - metasenv @ [conj] - ) [] metasenv) ; - ignore (T.type_of_aux' metasenv [] ty) ; - ignore (T.type_of_aux' metasenv [] bo) -;; - -let decompose_uris_choice_callback uris = -(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) - let module U = UriManager in - List.map - (function uri -> - match MQueryMisc.cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false) - (interactive_user_uri_choice - ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false - ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" - (List.map - (function (uri,typeno,_) -> - U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1) - ) uris) - ) -;; - -let mk_fresh_name_callback metasenv context name ~typ = - let fresh_name = - match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with - Cic.Name fresh_name -> fresh_name - | Cic.Anonymous -> assert false - in - match - GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name - ("Enter a fresh name for the hypothesis " ^ - CicPp.pp typ - (List.map (function None -> None | Some (n,_) -> Some n) context)) - with - Some fresh_name' -> Cic.Name fresh_name' - | None -> raise NoChoice -;; - -let refresh_proof (output : TermViewer.proof_viewer) = - try - let uri,currentproof = - match ProofEngine.get_proof () with - None -> assert false - | Some (uri,metasenv,bo,ty) -> - ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ; - if List.length metasenv = 0 then - begin - !qed_set_sensitive true ; - Hbugs.clear () - end - else - Hbugs.notify () ; - (*CSC: Wrong: [] is just plainly wrong *) - let uri = match uri with Some uri -> uri | _ -> assert false in - (uri, - Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) - in - ignore (output#load_proof uri currentproof) - with - e -> - match ProofEngine.get_proof () with - None -> assert false - | Some (uri,metasenv,bo,ty) -> - debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))); - raise (InvokeTactics.RefreshProofException e) - -let set_proof_engine_goal g = - ProofEngine.goal := g -;; - -let refresh_goals ?(empty_notebook=true) notebook = - try - match !ProofEngine.goal with - None -> - if empty_notebook then - begin - notebook#remove_all_pages ~skip_switch_page_event:false ; - notebook#set_empty_page - end - else - notebook#proofw#unload - | Some metano -> - let metasenv = - match ProofEngine.get_proof () with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let currentsequent = - List.find (function (m,_,_) -> m=metano) metasenv - in - let regenerate_notebook () = - let skip_switch_page_event = - match metasenv with - (m,_,_)::_ when m = metano -> false - | _ -> true - in - notebook#remove_all_pages ~skip_switch_page_event ; - List.iter (function (m,_,_) -> notebook#add_page m) metasenv ; - in - if empty_notebook then - begin - regenerate_notebook () ; - notebook#set_current_page - ~may_skip_switch_page_event:false metano - end - else - begin - notebook#set_current_page - ~may_skip_switch_page_event:true metano ; - notebook#proofw#load_sequent metasenv currentsequent - end - with - e -> -let metano = - match !ProofEngine.goal with - None -> assert false - | Some m -> m -in -let metasenv = - match ProofEngine.get_proof () with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv -in -try - let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in - debug_print - ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent); - raise (InvokeTactics.RefreshSequentException e) -with Not_found -> - debug_print ("Offending sequent " ^ string_of_int metano ^ " unknown."); - raise (InvokeTactics.RefreshSequentException e) - -module InvokeTacticsCallbacks = - struct - let sequent_viewer () = (rendering_window ())#notebook#proofw - let term_editor () = (rendering_window ())#inputt - let scratch_window () = (rendering_window ())#scratch_window - - let refresh_proof () = - let output = ((rendering_window ())#output : TermViewer.proof_viewer) in - refresh_proof output - - let refresh_goals () = - let notebook = (rendering_window ())#notebook in - refresh_goals notebook - - let decompose_uris_choice_callback = decompose_uris_choice_callback - let mk_fresh_name_callback = mk_fresh_name_callback - let mqi_handle = mqi_handle - end -;; -module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; -(* -(* Just to initialize the Hbugs module *) -module Ignore = Hbugs.Initialize (InvokeTactics');; -Hbugs.set_describe_hint_callback (fun hint -> - match hint with - | Hbugs_types.Use_apply_Luke term -> check_window [term] - | _ -> ()) -;; -*) -let dummy_uri = "/dummy.con" - - (** load an unfinished proof from filesystem *) -let load_unfinished_proof () = - let output = ((rendering_window ())#output : TermViewer.proof_viewer) in - let notebook = (rendering_window ())#notebook in - try - match - GToolbox.input_string ~title:"Load Unfinished Proof" ~text:dummy_uri - "Choose an URI:" - with - None -> raise NoChoice - | Some uri0 -> - let uri = UriManager.uri_of_string ("cic:" ^ uri0) in - let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in - let proof_file = Helm_registry.get "gtoplevel.proof_file" in - match CicParser.obj_of_xml proof_file_type (Some proof_file) with - Cic.CurrentProof (_,metasenv,bo,ty,_) -> - typecheck_loaded_proof metasenv bo ty ; - ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); - refresh_proof output ; - set_proof_engine_goal - (match metasenv with - [] -> None - | (metano,_,_)::_ -> Some metano - ) ; - refresh_goals notebook ; - HelmLogger.log - (`Msg (`T ("Current proof type loaded from " ^ proof_file_type))); - HelmLogger.log - (`Msg (`T ("Current proof body loaded from " ^ proof_file))) ; - !save_set_sensitive true; - | _ -> assert false - with - InvokeTactics.RefreshSequentException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e))) - | InvokeTactics.RefreshProofException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e))) - | e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let clear_aliases () = - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - inputt#environment := - DisambiguatingParser.EnvironmentP3.of_string - DisambiguatingParser.EnvironmentP3.empty -;; - -let edit_aliases () = - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let disambiguation_env = inputt#environment in - let chosen_aliases = ref None in - let window = - GWindow.window - ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in - let vbox = - GPack.vbox ~border_width:0 ~packing:window#add () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let input = GText.view ~editable:true ~width:400 ~height:100 - ~packing:scrolled_window#add () in - let hbox = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"Ok" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let clearb = - GButton.button ~label:"Clear" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let cancelb = - GButton.button ~label:"Cancel" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore (clearb#connect#clicked (fun () -> - input#buffer#set_text DisambiguatingParser.EnvironmentP3.empty)) ; - ignore (okb#connect#clicked (fun () -> - chosen_aliases := Some (input#buffer#get_text ()); - window#destroy ())); - ignore - (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0) - (DisambiguatingParser.EnvironmentP3.to_string !disambiguation_env ^ "\n")); - window#show () ; - GtkThread.main (); - match !chosen_aliases with - | None -> () - | Some raw_aliases -> - let new_disambiguation_env = - (try - DisambiguatingParser.EnvironmentP3.of_string raw_aliases - with e -> - HelmLogger.log - (`Error (`T - ("Error while parsing aliases: " ^ Printexc.to_string e))); - !disambiguation_env) - in - disambiguation_env := new_disambiguation_env -;; - -let proveit () = - let module L = LogicalOperations in - let module G = Gdome in - let notebook = (rendering_window ())#notebook in - let output = (rendering_window ())#output in - try - output#make_sequent_of_selected_term ; - refresh_proof output ; - refresh_goals notebook - with - InvokeTactics.RefreshSequentException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e))) - | InvokeTactics.RefreshProofException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e))) - | e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let focus () = - let module L = LogicalOperations in - let module G = Gdome in - let notebook = (rendering_window ())#notebook in - let output = (rendering_window ())#output in - try - output#focus_sequent_of_selected_term ; - refresh_goals notebook - with - InvokeTactics.RefreshSequentException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e))) - | InvokeTactics.RefreshProofException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e))) - | e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -exception NoPrevGoal;; -exception NoNextGoal;; - -let setgoal metano = - let module L = LogicalOperations in - let module G = Gdome in - let notebook = (rendering_window ())#notebook in - let output = (rendering_window ())#output in - let metasenv = - match ProofEngine.get_proof () with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - try - refresh_goals ~empty_notebook:false notebook - with - InvokeTactics.RefreshSequentException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e))) - | e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let - show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback -= - let window = - GWindow.window ~width:800 ~border_width:2 () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 ~packing:window#add () in - let mmlwidget = - GMathViewAux.single_selection_math_view - ~packing:scrolled_window#add ~width:600 ~height:400 () - in - let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in - let href = Gdome.domString "href" in - let show_in_show_window_obj uri obj = - try - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object obj - in - let mml = - ChosenTransformer.mml_of_cic_object - ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types - in - window#set_title (UriManager.string_of_uri uri) ; - window#misc#hide () ; window#show () ; - mmlwidget#load_doc mml ; - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) - in - let show_in_show_window_uri uri = - let obj = CicEnvironment.get_obj uri in - show_in_show_window_obj uri obj - in - let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ = - match n with - None -> () - | Some n' -> - if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then - let uri = - (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string - in - show_in_show_window_uri (UriManager.uri_of_string uri) - else - ignore (mmlwidget#action_toggle n') - in - let _ = - mmlwidget#connect#click (show_in_show_window_callback mmlwidget) - in - show_in_show_window_obj, show_in_show_window_uri, - show_in_show_window_callback -;; - -exception NoObjectsLocated;; - -let user_uri_choice ~title ~msg uris = - let uri = - match uris with - [] -> raise NoObjectsLocated - | [uri] -> uri - | uris -> - match - interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris - with - [uri] -> uri - | _ -> assert false - in - String.sub uri 4 (String.length uri - 4) -;; - -let locate_callback id = - let query = MQG.locate id in - let result = MQI.execute mqi_handle query in - let uris = - List.map - (function uri,_ -> - MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri) - result in - HelmLogger.log (`Msg (`T "Locate Query:")) ; - MQueryUtil.text_of_query (fun m -> HelmLogger.log (`Msg (`T m))) "" query; - HelmLogger.log (`Msg (`T "Result:")) ; - MQueryUtil.text_of_result (fun m -> HelmLogger.log (`Msg (`T m))) "" result; - user_uri_choice ~title:"Ambiguous input." - ~msg: - ("Ambiguous input \"" ^ id ^ - "\". Please, choose one interpetation:") - uris -;; - - -let input_or_locate_uri ~title = - let uri = ref None in - let window = - GWindow.window - ~width:400 ~modal:true ~title ~border_width:2 () in - let vbox = GPack.vbox ~packing:window#add () in - let hbox1 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in - let manual_input = - GEdit.entry ~editable:true - ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let _ = checkb#misc#set_sensitive false in - let hbox2 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:"You can also enter an indentifier to locate:" - ~packing:(hbox2#pack ~padding:5) () in - let locate_input = - GEdit.entry ~editable:true - ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in - let locateb = - GButton.button ~label:"Locate" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let _ = locateb#misc#set_sensitive false in - let hbox3 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"Ok" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive false in - let cancelb = - GButton.button ~label:"Cancel" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () - in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore - (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ; - let check_callback () = - let uri = "cic:" ^ manual_input#text in - try - ignore (Http_getter.resolve' (UriManager.uri_of_string uri)) ; - HelmLogger.log (`Msg (`T "OK")) ; - true - with - Http_getter_types.Unresolvable_URI _ -> - HelmLogger.log - (`Error (`T ("URI " ^ uri ^ - " does not correspond to any object."))) ; - false - | UriManager.IllFormedUri _ -> - HelmLogger.log - (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ; - false - | e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) ; - false - in - ignore - (okb#connect#clicked - (function () -> - if check_callback () then - begin - uri := Some manual_input#text ; - window#destroy () - end - )) ; - ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ; - ignore - (manual_input#connect#changed - (fun _ -> - if manual_input#text = "" then - begin - checkb#misc#set_sensitive false ; - okb#misc#set_sensitive false - end - else - begin - checkb#misc#set_sensitive true ; - okb#misc#set_sensitive true - end)); - ignore - (locate_input#connect#changed - (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ; - ignore - (locateb#connect#clicked - (function () -> - let id = locate_input#text in - manual_input#set_text (locate_callback id) ; - locate_input#delete_text 0 (String.length id) - )) ; - window#show () ; - GtkThread.main (); - match !uri with - None -> raise NoChoice - | Some uri -> UriManager.uri_of_string ("cic:" ^ uri) -;; - -exception AmbiguousInput;; - -(* A WIDGET TO ENTER CIC TERMS *) - -module DisambiguateCallbacks = - struct - let interactive_user_uri_choice = - fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id -> - interactive_user_uri_choice ~selection_mode ?ok - ?enable_button_for_non_vars ~title ~msg - let interactive_interpretation_choice = interactive_interpretation_choice - let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title - end -;; - -module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);; - -(* OTHER FUNCTIONS *) - -let locate () = - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - try - match - GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" - with - None -> raise NoChoice - | Some input -> - let uri = locate_callback input in - inputt#set_term uri - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - - -exception UriAlreadyInUse;; -exception NotAUriToAConstant;; - -let new_inductive () = - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let output = ((rendering_window ())#output : TermViewer.proof_viewer) in - let notebook = (rendering_window ())#notebook in - - let chosen = ref false in - let inductive = ref true in - let paramsno = ref 0 in - let get_uri = ref (function _ -> assert false) in - let get_base_uri = ref (function _ -> assert false) in - let get_names = ref (function _ -> assert false) in - let get_types_and_cons = ref (function _ -> assert false) in - let get_context_and_subst = ref (function _ -> assert false) in - let window = - GWindow.window - ~width:600 ~modal:true ~position:`CENTER - ~title:"New Block of Mutual (Co)Inductive Definitions" - ~border_width:2 () in - let vbox = GPack.vbox ~packing:window#add () in - let hbox = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:"Enter the URI for the new block:" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let uri_entry = - GEdit.entry ~editable:true - ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in - let hbox0 = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label - ~text: - "Enter the number of left parameters in every arity and constructor type:" - ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in - let paramsno_entry = - GEdit.entry ~editable:true ~text:"0" - ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in - let hbox1 = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:"Are the definitions inductive or coinductive?" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let inductiveb = - GButton.radio_button ~label:"Inductive" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let coinductiveb = - GButton.radio_button ~label:"Coinductive" - ~group:inductiveb#group - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let hbox2 = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:"Enter the list of the names of the types:" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let names_entry = - GEdit.entry ~editable:true - ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in - let hboxn = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"> Next" - ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive true in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - (* First phase *) - let rec phase1 () = - ignore - (okb#connect#clicked - (function () -> - try - let uristr = "cic:" ^ uri_entry#text in - let namesstr = names_entry#text in - let paramsno' = int_of_string (paramsno_entry#text) in - match Str.split (Str.regexp " +") namesstr with - [] -> assert false - | (he::tl) as names -> - let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in - begin - try - ignore (Http_getter.resolve' uri) ; - raise UriAlreadyInUse - with Http_getter_types.Unresolvable_URI _ -> - get_uri := (function () -> uri) ; - get_names := (function () -> names) ; - inductive := inductiveb#active ; - paramsno := paramsno' ; - phase2 () - end - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) - )) - (* Second phase *) - and phase2 () = - let type_widgets = - List.map - (function name -> - let frame = - GBin.frame ~label:name - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let vbox = GPack.vbox ~packing:frame#add () in - let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in - let _ = - GMisc.label ~text:("Enter its type:") - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:5 - ~packing:(vbox#pack ~expand:true ~padding:0) () in - let newinputt = - TermEditor'.term_editor - mqi_handle - ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_environment_with:inputt () - ~isnotempty_callback: - (function b -> - (*non_empty_type := b ;*) - okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) - in - let hbox = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:("Enter the list of its constructors:") - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let cons_names_entry = - GEdit.entry ~editable:true - ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in - (newinputt,cons_names_entry) - ) (!get_names ()) - in - vbox#remove hboxn#coerce ; - let hboxn = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"> Next" - ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked - (function () -> - try - let names = !get_names () in - let types_and_cons = - List.map2 - (fun name (newinputt,cons_names_entry) -> - let consnamesstr = cons_names_entry#text in - let cons_names = Str.split (Str.regexp " +") consnamesstr in - let metasenv,expr = - newinputt#get_metasenv_and_term ~context:[] ~metasenv:[] - in - match metasenv with - [] -> expr,cons_names - | _ -> raise AmbiguousInput - ) names type_widgets - in - let uri = !get_uri () in - let _ = - (* Let's see if so far the definition is well-typed *) - let params = [] in - let paramsno = 0 in - (* To test if the arities of the inductive types are well *) - (* typed, we check the inductive block definition where *) - (* no constructor is given to each type. *) - let tys = - List.map2 - (fun name (ty,cons) -> (name, !inductive, ty, [])) - names types_and_cons - in - CicTypeChecker.typecheck_mutual_inductive_defs uri - (tys,params,paramsno) - in - get_context_and_subst := - (function () -> - let i = ref 0 in - List.fold_left2 - (fun (context,subst) name (ty,_) -> - let res = - (Some (Cic.Name name, Cic.Decl ty))::context, - (Cic.MutInd (uri,!i,[]))::subst - in - incr i ; res - ) ([],[]) names types_and_cons) ; - let types_and_cons' = - List.map2 - (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons)) - names types_and_cons - in - get_types_and_cons := (function () -> types_and_cons') ; - chosen := true ; - window#destroy () - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) - )) - (* Third phase *) - and phase3 name cons = - let get_cons_types = ref (function () -> assert false) in - let window2 = - GWindow.window - ~width:600 ~modal:true ~position:`CENTER - ~title:(name ^ " Constructors") - ~border_width:2 () in - let vbox = GPack.vbox ~packing:window2#add () in - let cons_type_widgets = - List.map - (function consname -> - let hbox = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:("Enter the type of " ^ consname ^ ":") - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:5 - ~packing:(vbox#pack ~expand:true ~padding:0) () in - let newinputt = - TermEditor'.term_editor - mqi_handle - ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_environment_with:inputt () - ~isnotempty_callback: - (function b -> - (* (*non_empty_type := b ;*) - okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)()) - in - newinputt - ) cons in - let hboxn = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"> Next" - ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive true in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in - ignore (window2#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window2#destroy) ; - ignore - (okb#connect#clicked - (function () -> - try - chosen := true ; - let context,subst= !get_context_and_subst () in - let cons_types = - List.map2 - (fun name inputt -> - let metasenv,expr = - inputt#get_metasenv_and_term ~context ~metasenv:[] - in - match metasenv with - [] -> - let undebrujined_expr = - List.fold_left - (fun expr t -> CicSubstitution.subst t expr) expr subst - in - name, undebrujined_expr - | _ -> raise AmbiguousInput - ) cons cons_type_widgets - in - get_cons_types := (function () -> cons_types) ; - window2#destroy () - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) - )) ; - window2#show () ; - GtkThread.main (); - let okb_pressed = !chosen in - chosen := false ; - if (not okb_pressed) then - begin - window#destroy () ; - assert false (* The control never reaches this point *) - end - else - (!get_cons_types ()) - in - phase1 () ; - (* No more phases left or Abort pressed *) - window#show () ; - GtkThread.main (); - window#destroy () ; - if !chosen then - try - let uri = !get_uri () in -(*CSC: Da finire *) - let params = [] in - let tys = !get_types_and_cons () in - let obj = Cic.InductiveDefinition(tys,params,!paramsno) in - begin - try - debug_print (CicPp.ppobj obj); - CicTypeChecker.typecheck_mutual_inductive_defs uri - (tys,params,!paramsno) ; - with - e -> - debug_print "Offending mutual (co)inductive type declaration:" ; - debug_print (CicPp.ppobj obj) ; - end ; - (* We already know that obj is well-typed. We need to add it to the *) - (* environment in order to compute the inner-types without having to *) - (* debrujin it or having to modify lots of other functions to avoid *) - (* asking the environment for the MUTINDs we are defining now. *) - CicEnvironment.put_inductive_definition uri obj ; - save_obj uri obj ; - show_in_show_window_obj uri obj - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let new_proof () = - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let output = ((rendering_window ())#output : TermViewer.proof_viewer) in - let notebook = (rendering_window ())#notebook in - - let chosen = ref false in - let get_metasenv_and_term = ref (function _ -> assert false) in - let get_uri = ref (function _ -> assert false) in - let non_empty_type = ref false in - let window = - GWindow.window - ~width:600 ~modal:true ~title:"New Proof or Definition" - ~border_width:2 () in - let vbox = GPack.vbox ~packing:window#add () in - let hbox = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:"Enter the URI for the new theorem or definition:" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let uri_entry = - GEdit.entry ~editable:true - ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in - uri_entry#set_text dummy_uri; - uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri); - let hbox1 = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = - GMisc.label ~text:"Enter the theorem or definition type:" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:5 - ~packing:(vbox#pack ~expand:true ~padding:0) () in - (* the content of the scrolled_window is moved below (see comment) *) - let hbox = - GPack.hbox ~border_width:0 - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"Ok" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive false in - let cancelb = - GButton.button ~label:"Cancel" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - (* moved here to have visibility of the ok button *) - let newinputt = - TermEditor'.term_editor - mqi_handle - ~width:400 ~height:100 ~packing:scrolled_window#add - ~share_environment_with:inputt () - ~isnotempty_callback: - (function b -> - non_empty_type := b ; - okb#misc#set_sensitive (b && uri_entry#text <> "")) - in - let _ = - newinputt#set_term inputt#get_as_string ; - inputt#reset in - let _ = - uri_entry#connect#changed - (function () -> - okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> "")) - in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked - (function () -> - chosen := true ; - try - let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in - let uristr = "cic:" ^ uri_entry#text in - let uri = UriManager.uri_of_string uristr in - if String.sub uristr (String.length uristr - 4) 4 <> ".con" then - raise NotAUriToAConstant - else - begin - try - ignore (Http_getter.resolve' uri) ; - raise UriAlreadyInUse - with Http_getter_types.Unresolvable_URI _ -> - get_metasenv_and_term := (function () -> metasenv,parsed) ; - get_uri := (function () -> uri) ; - window#destroy () - end - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) - )) ; - window#show () ; - GtkThread.main (); - if !chosen then - try - let metasenv,expr = !get_metasenv_and_term () in - let _ = CicTypeChecker.type_of_aux' metasenv [] expr in - ProofEngine.set_proof - (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)); - set_proof_engine_goal (Some 1) ; - refresh_goals notebook ; - refresh_proof output ; - !save_set_sensitive true ; - inputt#reset ; - ProofEngine.intros ~mk_fresh_name_callback () ; - refresh_goals notebook ; - refresh_proof output - with - InvokeTactics.RefreshSequentException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e))) - | InvokeTactics.RefreshProofException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e))) - | e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let check_term_in_scratch scratch_window metasenv context expr = - try - let ty = CicTypeChecker.type_of_aux' metasenv context expr in - let expr = Cic.Cast (expr,ty) in - scratch_window#show () ; - scratch_window#set_term expr ; - scratch_window#set_context context ; - scratch_window#set_metasenv metasenv ; - scratch_window#sequent_viewer#load_sequent metasenv (111,context,expr) - with - e -> - print_endline ("? " ^ CicPp.ppterm expr) ; - raise e -;; - -let check scratch_window () = - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let metasenv = - match ProofEngine.get_proof () with - None -> [] - | Some (_,metasenv,_,_) -> metasenv - in - let context = - match !ProofEngine.goal with - None -> [] - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - in - try - let metasenv',expr = inputt#get_metasenv_and_term context metasenv in - check_term_in_scratch scratch_window metasenv' context expr - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let show () = - try - show_in_show_window_uri (input_or_locate_uri ~title:"Show") - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -exception NotADefinition;; - -let open_ () = - let output = ((rendering_window ())#output : TermViewer.proof_viewer) in - let notebook = (rendering_window ())#notebook in - try - let uri = input_or_locate_uri ~title:"Open" in - CicTypeChecker.typecheck uri ; - let metasenv,bo,ty = - match CicEnvironment.get_cooked_obj uri with - Cic.Constant (_,Some bo,ty,_) -> [],bo,ty - | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty - | Cic.Constant _ - | Cic.Variable _ - | Cic.InductiveDefinition _ -> raise NotADefinition - in - ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ; - set_proof_engine_goal None ; - refresh_goals notebook ; - refresh_proof output ; - !save_set_sensitive true - with - InvokeTactics.RefreshSequentException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e))) - | InvokeTactics.RefreshProofException e -> - HelmLogger.log - (`Error (`T ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e))) - | e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let show_query_results results = - let window = - GWindow.window - ~modal:false ~title:"Query results." ~border_width:2 () in - let vbox = GPack.vbox ~packing:window#add () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text:"Click on a URI to show that object" - ~packing:hbox#add () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 ~height:400 ~width:600 - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in - ignore - (List.map - (function (uri,_) -> - let n = - clist#append [uri] - in - clist#set_row ~selectable:false n - ) results - ) ; - clist#columns_autosize () ; - ignore - (clist#connect#select_row - (fun ~row ~column ~event -> - let (uristr,_) = List.nth results row in - match - MQueryMisc.cic_textual_parser_uri_of_string - (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' - uristr) - with - CicTextualParser0.ConUri uri - | CicTextualParser0.VarUri uri - | CicTextualParser0.IndTyUri (uri,_) - | CicTextualParser0.IndConUri (uri,_,_) -> - show_in_show_window_uri uri - ) - ) ; - window#show () -;; - -let refine_constraints (must_obj,must_rel,must_sort) = - let chosen = ref false in - let use_only = ref false in - let window = - GWindow.window - ~modal:true ~title:"Constraints refinement." - ~width:800 ~border_width:2 () in - let vbox = GPack.vbox ~packing:window#add () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text: "\"Only\" constraints can be enforced or not." - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let onlyb = - GButton.toggle_button ~label:"Enforce \"only\" constraints" - ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () - in - ignore - (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ; - (* Notebook for the constraints choice *) - let notebook = - GPack.notebook ~scrollable:true - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - (* Rel constraints *) - let label = - GMisc.label - ~text: "Constraints on Rels" () in - let vbox' = - GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) - () in - let hbox = - GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text: "You can now specify the constraints on Rels." - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let expected_height = 25 * (List.length must_rel + 2) in - let height = if expected_height > 400 then 400 else expected_height in - let scrolled_window = - GBin.scrolled_window ~border_width:10 ~height ~width:600 - ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in - let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in - let mk_depth_button (hbox:GPack.box) d = - let mutable_ref = ref (Some d) in - let depthb = - GButton.toggle_button - ~label:("depth = " ^ string_of_int d) - ~active:true - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () - in - ignore - (depthb#connect#toggled - (function () -> - let sel_depth = if depthb#active then Some d else None in - mutable_ref := sel_depth - )) ; mutable_ref - in - let rel_constraints = - List.map - (function p -> - let hbox = - GPack.hbox - ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text:(MQGU.text_of_position (p:>MQGT.full_position)) - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - match p with - | `MainHypothesis None - | `MainConclusion None -> p, ref None - | `MainHypothesis (Some depth') - | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth' - ) must_rel in - (* Sort constraints *) - let label = - GMisc.label - ~text: "Constraints on Sorts" () in - let vbox' = - GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) - () in - let hbox = - GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text: "You can now specify the constraints on Sorts." - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let expected_height = 25 * (List.length must_sort + 2) in - let height = if expected_height > 400 then 400 else expected_height in - let scrolled_window = - GBin.scrolled_window ~border_width:10 ~height ~width:600 - ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in - let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in - let sort_constraints = - List.map - (function (p, sort) -> - let hbox = - GPack.hbox - ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text:(MQGU.text_of_sort sort ^ " " ^ MQGU.text_of_position (p:>MQGT.full_position)) - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - match p with - | `MainHypothesis None - | `MainConclusion None -> p, ref None, sort - | `MainHypothesis (Some depth') - | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', sort - ) must_sort in - (* Obj constraints *) - let label = - GMisc.label - ~text: "Constraints on constants" () in - let vbox' = - GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) - () in - let hbox = - GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text: "You can now specify the constraints on constants." - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let expected_height = 25 * (List.length must_obj + 2) in - let height = if expected_height > 400 then 400 else expected_height in - let scrolled_window = - GBin.scrolled_window ~border_width:10 ~height ~width:600 - ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in - let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in - let obj_constraints = - List.map - (function (p, uri) -> - let hbox = - GPack.hbox - ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text:(uri ^ " " ^ (MQGU.text_of_position p)) - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - match p with - | `InBody - | `InHypothesis - | `InConclusion - | `MainHypothesis None - | `MainConclusion None -> p, ref None, uri - | `MainHypothesis (Some depth') - | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', uri - ) must_obj in - (* Confirm/abort buttons *) - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"Ok" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () - in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked (function () -> chosen := true ; window#destroy ())); - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - if !chosen then - let chosen_must_rel = - List.map - (function (position, ref_depth) -> MQGU.set_main_position position !ref_depth) - rel_constraints - in - let chosen_must_sort = - List.map - (function (position, ref_depth, sort) -> - MQGU.set_main_position position !ref_depth,sort) - sort_constraints - in - let chosen_must_obj = - List.map - (function (position, ref_depth, uri) -> MQGU.set_full_position position !ref_depth, uri) - obj_constraints - in - (chosen_must_obj,chosen_must_rel,chosen_must_sort), - (if !use_only then -(*CSC: ???????????????????????? I assume that must and only are the same... *) - Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort - else - None,None,None - ) - else - raise NoChoice -;; - -let completeSearchPattern () = - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - try - let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in - let must = CGSearchPattern.get_constraints expr in - let must',only = refine_constraints must in - let query = - MQG.query_of_constraints (Some CGSearchPattern.universe) must' only - in - let results = MQI.execute mqi_handle query in - show_query_results results - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let insertQuery () = - try - let chosen = ref None in - let window = - GWindow.window - ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in - let vbox = GPack.vbox ~packing:window#add () in - let label = - GMisc.label ~text:"Insert Query. For Experts Only." - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 ~height:400 ~width:600 - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let input = GText.view ~editable:true - ~packing:scrolled_window#add () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"Ok" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let loadb = - GButton.button ~label:"Load from file..." - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked - (function () -> - chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ; - ignore - (loadb#connect#clicked - (function () -> - match - GToolbox.select_file ~title:"Select Query File" () - with - None -> () - | Some filename -> - let inch = open_in filename in - let rec read_file () = - try - let line = input_line inch in - line ^ "\n" ^ read_file () - with - End_of_file -> "" - in - let text = read_file () in - input#buffer#delete input#buffer#start_iter input#buffer#end_iter ; - ignore (input#buffer#insert text))) ; - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - match !chosen with - None -> () - | Some q -> - let results = - MQI.execute mqi_handle (MQueryUtil.query_of_text (Lexing.from_string q)) - in - show_query_results results - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let choose_must list_of_must only = - let chosen = ref None in - let user_constraints = ref [] in - let window = - GWindow.window - ~modal:true ~title:"Query refinement." ~border_width:2 () in - let vbox = GPack.vbox ~packing:window#add () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text: - ("You can now specify the genericity of the query. " ^ - "The more generic the slower.") - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text: - "Suggestion: start with faster queries before moving to more generic ones." - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let notebook = - GPack.notebook ~scrollable:true - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let _ = - let page = ref 0 in - let last = List.length list_of_must in - List.map - (function must -> - incr page ; - let label = - GMisc.label ~text: - (if !page = 1 then "More generic" else - if !page = last then "More precise" else " ") () in - let expected_height = 25 * (List.length must + 2) in - let height = if expected_height > 400 then 400 else expected_height in - let scrolled_window = - GBin.scrolled_window ~border_width:10 ~height ~width:600 - ~packing:(notebook#append_page ~tab_label:label#coerce) () in - let clist = - GList.clist ~columns:2 ~packing:scrolled_window#add - ~titles:["URI" ; "Position"] () - in - ignore - (List.map - (function (position, uri) -> - let n = - clist#append - [uri; MQGUtil.text_of_position position] - in - clist#set_row ~selectable:false n - ) must - ) ; - clist#columns_autosize () - ) list_of_must in - let _ = - let label = GMisc.label ~text:"User provided" () in - let vbox = - GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let lMessage = - GMisc.label - ~text:"Select the constraints that must be satisfied and press OK." - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let expected_height = 25 * (List.length only + 2) in - let height = if expected_height > 400 then 400 else expected_height in - let scrolled_window = - GBin.scrolled_window ~border_width:10 ~height ~width:600 - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let clist = - GList.clist ~columns:2 ~packing:scrolled_window#add - ~selection_mode:`MULTIPLE - ~titles:["URI" ; "Position"] () - in - ignore - (List.map - (function (position, uri) -> - let n = - clist#append - [uri; MQGUtil.text_of_position position] - in - clist#set_row ~selectable:true n - ) only - ) ; - clist#columns_autosize () ; - ignore - (clist#connect#select_row - (fun ~row ~column ~event -> - user_constraints := (List.nth only row)::!user_constraints)) ; - ignore - (clist#connect#unselect_row - (fun ~row ~column ~event -> - user_constraints := - List.filter - (function uri -> uri != (List.nth only row)) !user_constraints)) ; - in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let okb = - GButton.button ~label:"Ok" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - (* actions *) - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked - (function () -> chosen := Some notebook#current_page ; window#destroy ())) ; - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - match !chosen with - None -> raise NoChoice - | Some n -> - if n = List.length list_of_must then - (* user provided constraints *) - !user_constraints - else - List.nth list_of_must n -;; - -let searchPattern () = - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - try - let proof = - match ProofEngine.get_proof () with - None -> assert false - | Some proof -> proof - in - match !ProofEngine.goal with - | None -> () - | Some metano -> - let uris' = - TacticChaser.matchConclusion mqi_handle - ~choose_must () (proof, metano) - in - let uri' = - user_uri_choice ~title:"Ambiguous input." - ~msg: "Many lemmas can be successfully applied. Please, choose one:" - uris' - in - inputt#set_term uri' ; - InvokeTactics'.apply () - with - e -> - HelmLogger.log - (`Error (`T (Printexc.to_string e))) -;; - -let choose_selection mmlwidget (element : Gdome.element option) = - let module G = Gdome in - let rec aux element = - if element#hasAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref") - then - mmlwidget#set_selection (Some element) - else - try - match element#get_parentNode with - None -> assert false - (*CSC: OCAML DIVERGES! - | Some p -> aux (new G.element_of_node p) - *) - | Some p -> aux (new Gdome.element_of_node p) - with - GdomeInit.DOMCastException _ -> - debug_print - "******* trying to select above the document root ********" - in - match element with - Some x -> aux x - | None -> mmlwidget#set_selection None -;; - -(* STUFF TO BUILD THE GTK INTERFACE *) - -(* Stuff for the widget settings *) - -(* -let export_to_postscript output = - let lastdir = ref (Unix.getcwd ()) in - function () -> - match - GToolbox.select_file ~title:"Export to PostScript" - ~dir:lastdir ~filename:"screenshot.ps" () - with - None -> () - | Some filename -> - (output :> GMathView.math_view)#export_to_postscript - ~filename:filename (); -;; -*) - -(* -let activate_t1 output button_set_anti_aliasing - button_set_transparency export_to_postscript_menu_item - button_t1 () -= - let is_set = button_t1#active in - output#set_font_manager_type - ~fm_type:(if is_set then `font_manager_t1 else `font_manager_gtk) ; - if is_set then - begin - button_set_anti_aliasing#misc#set_sensitive true ; - button_set_transparency#misc#set_sensitive true ; - export_to_postscript_menu_item#misc#set_sensitive true ; - end - else - begin - button_set_anti_aliasing#misc#set_sensitive false ; - button_set_transparency#misc#set_sensitive false ; - export_to_postscript_menu_item#misc#set_sensitive false ; - end -;; - -let set_anti_aliasing output button_set_anti_aliasing () = - output#set_anti_aliasing button_set_anti_aliasing#active -;; - -let set_transparency output button_set_transparency () = - output#set_transparency button_set_transparency#active -;; -*) - -let changefont output font_size_spinb () = - output#set_font_size font_size_spinb#value_as_int -;; - -let set_log_verbosity output log_verbosity_spinb () = - output#set_log_verbosity log_verbosity_spinb#value_as_int -;; - -class settings_window output sw - export_to_postscript_menu_item selection_changed_callback -= - let settings_window = GWindow.window ~title:"GtkMathView settings" () in - let vbox = - GPack.vbox ~packing:settings_window#add () in - let table = - GPack.table - ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 - ~border_width:5 ~packing:vbox#add () in - let button_t1 = - GButton.toggle_button ~label:"activate t1 fonts" - ~packing:(table#attach ~left:0 ~top:0) () in - let button_set_anti_aliasing = - GButton.toggle_button ~label:"set_anti_aliasing" - ~packing:(table#attach ~left:0 ~top:1) () in - let button_set_transparency = - GButton.toggle_button ~label:"set_transparency" - ~packing:(table#attach ~left:2 ~top:1) () in - let table = - GPack.table - ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 - ~border_width:5 ~packing:vbox#add () in - let font_size_label = - GMisc.label ~text:"font size:" - ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in - let font_size_spinb = - let sadj = - GData.adjustment ~value:(float_of_int output#get_font_size) - ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () - in - GEdit.spin_button - ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in - let log_verbosity_label = - GMisc.label ~text:"log verbosity:" - ~packing:(table#attach ~left:0 ~top:1) () in - let log_verbosity_spinb = - let sadj = - GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 () - in - GEdit.spin_button - ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let closeb = - GButton.button ~label:"Close" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in -object(self) - method show = settings_window#show - initializer - button_set_anti_aliasing#misc#set_sensitive false ; - button_set_transparency#misc#set_sensitive false ; - (* Signals connection *) - (* - ignore(button_t1#connect#clicked - (activate_t1 output button_set_anti_aliasing - button_set_transparency export_to_postscript_menu_item button_t1)) ; - *) - ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; - (* - ignore(button_set_anti_aliasing#connect#toggled - (set_anti_aliasing output button_set_anti_aliasing)); - ignore(button_set_transparency#connect#toggled - (set_transparency output button_set_transparency)) ; - *) - ignore(log_verbosity_spinb#connect#changed - (set_log_verbosity output log_verbosity_spinb)) ; - ignore(closeb#connect#clicked settings_window#misc#hide) -end;; - -(* Scratch window *) - -class scratch_window = - let window = - GWindow.window - ~title:"MathML viewer" - ~border_width:2 () in - let vbox = - GPack.vbox ~packing:window#add () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let whdb = - GButton.button ~label:"Whd" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let reduceb = - GButton.button ~label:"Reduce" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let simplb = - GButton.button ~label:"Simpl" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox#pack ~expand:true ~padding:5) () in - let sequent_viewer = - TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent - ~packing:(scrolled_window#add) ~width:400 ~height:280 () in -object(self) - val mutable term = Cic.Rel 1 (* dummy value *) - val mutable context = ([] : Cic.context) (* dummy value *) - val mutable metasenv = ([] : Cic.metasenv) (* dummy value *) - method sequent_viewer = sequent_viewer - method show () = window#misc#hide () ; window#show () - method term = term - method set_term t = term <- t - method context = context - method set_context t = context <- t - method metasenv = metasenv - method set_metasenv t = metasenv <- t - initializer - ignore - (sequent_viewer#connect#selection_changed (choose_selection sequent_viewer)); - ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ; - ignore(whdb#connect#clicked InvokeTactics'.whd_in_scratch) ; - ignore(reduceb#connect#clicked InvokeTactics'.reduce_in_scratch) ; - ignore(simplb#connect#clicked InvokeTactics'.simpl_in_scratch) -end;; - -let open_contextual_menu_for_selected_terms mmlwidget infos = - let button = GdkEvent.Button.button infos in - let terms_selected = List.length mmlwidget#get_selections > 0 in - if button = 3 then - begin - let time = GdkEvent.Button.time infos in - let menu = GMenu.menu () in - let f = new GMenu.factory menu in - let whd_menu_item = - f#add_item "Whd" ~key:GdkKeysyms._W ~callback:InvokeTactics'.whd in - let reduce_menu_item = - f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:InvokeTactics'.reduce in - let simpl_menu_item = - f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:InvokeTactics'.simpl in - let _ = f#add_separator () in - let generalize_menu_item = - f#add_item "Generalize" - ~key:GdkKeysyms._G ~callback:InvokeTactics'.generalize in - let _ = f#add_separator () in - let clear_menu_item = - f#add_item "Clear" ~key:GdkKeysyms._C ~callback:InvokeTactics'.clear in - let clearbody_menu_item = - f#add_item "ClearBody" - ~key:GdkKeysyms._B ~callback:InvokeTactics'.clearbody - in - whd_menu_item#misc#set_sensitive terms_selected ; - reduce_menu_item#misc#set_sensitive terms_selected ; - simpl_menu_item#misc#set_sensitive terms_selected ; - generalize_menu_item#misc#set_sensitive terms_selected ; - clear_menu_item#misc#set_sensitive terms_selected ; - clearbody_menu_item#misc#set_sensitive terms_selected ; - menu#popup ~button ~time - end ; - true -;; - -class page () = - let vbox1 = GPack.vbox () in -object(self) - val mutable proofw_ref = None - val mutable compute_ref = None - method proofw = - Lazy.force self#compute ; - match proofw_ref with - None -> assert false - | Some proofw -> proofw - method content = vbox1 - method compute = - match compute_ref with - None -> assert false - | Some compute -> compute - initializer - compute_ref <- - Some (lazy ( - let scrolled_window1 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox1#pack ~expand:true ~padding:5) () in - let proofw = - TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent - ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in - let _ = proofw_ref <- Some proofw in - let hbox3 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let ringb = - GButton.button ~label:"Ring" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let fourierb = - GButton.button ~label:"Fourier" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let reflexivityb = - GButton.button ~label:"Reflexivity" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let symmetryb = - GButton.button ~label:"Symmetry" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let assumptionb = - GButton.button ~label:"Assumption" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let contradictionb = - GButton.button ~label:"Contradiction" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let autob= - GButton.button ~label:"Auto" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let hbox4 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let existsb = - GButton.button ~label:"Exists" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let splitb = - GButton.button ~label:"Split" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let leftb = - GButton.button ~label:"Left" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let rightb = - GButton.button ~label:"Right" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let searchpatternb = - GButton.button ~label:"SearchPattern_Apply" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let hbox5 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let exactb = - GButton.button ~label:"Exact" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let introsb = - GButton.button ~label:"Intros" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let applyb = - GButton.button ~label:"Apply" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let elimintrossimplb = - GButton.button ~label:"ElimIntrosSimpl" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let elimtypeb = - GButton.button ~label:"ElimType" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let foldwhdb = - GButton.button ~label:"Fold_whd" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let foldreduceb = - GButton.button ~label:"Fold_reduce" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let hbox6 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let foldsimplb = - GButton.button ~label:"Fold_simpl" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in - let cutb = - GButton.button ~label:"Cut" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in - let changeb = - GButton.button ~label:"Change" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in - let letinb = - GButton.button ~label:"Let ... In" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in - let rewritesimplb = - GButton.button ~label:"RewriteSimpl ->" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in - let rewritebacksimplb = - GButton.button ~label:"RewriteSimpl <-" - ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in - let hbox7 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let absurdb = - GButton.button ~label:"Absurd" - ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in - let decomposeb = - GButton.button ~label:"Decompose" - ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in - let transitivityb = - GButton.button ~label:"Transitivity" - ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in - let replaceb = - GButton.button ~label:"Replace" - ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in - let injectionb = - GButton.button ~label:"Injection" - ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in - let discriminateb = - GButton.button ~label:"Discriminate" - ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in -(* Zack: spostare in una toolbar - let generalizeb = - GButton.button ~label:"Generalize" - ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in - let clearbodyb = - GButton.button ~label:"ClearBody" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let clearb = - GButton.button ~label:"Clear" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let whdb = - GButton.button ~label:"Whd" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let reduceb = - GButton.button ~label:"Reduce" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let simplb = - GButton.button ~label:"Simpl" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in -*) - - ignore(exactb#connect#clicked InvokeTactics'.exact) ; - ignore(applyb#connect#clicked InvokeTactics'.apply) ; - ignore(elimintrossimplb#connect#clicked InvokeTactics'.elimintrossimpl) ; - ignore(elimtypeb#connect#clicked InvokeTactics'.elimtype) ; - ignore(foldwhdb#connect#clicked InvokeTactics'.fold_whd) ; - ignore(foldreduceb#connect#clicked InvokeTactics'.fold_reduce) ; - ignore(foldsimplb#connect#clicked InvokeTactics'.fold_simpl) ; - ignore(cutb#connect#clicked InvokeTactics'.cut) ; - ignore(changeb#connect#clicked InvokeTactics'.change) ; - ignore(letinb#connect#clicked InvokeTactics'.letin) ; - ignore(ringb#connect#clicked InvokeTactics'.ring) ; - ignore(fourierb#connect#clicked InvokeTactics'.fourier) ; - ignore(rewritesimplb#connect#clicked InvokeTactics'.rewritesimpl) ; - ignore(rewritebacksimplb#connect#clicked InvokeTactics'.rewritebacksimpl) ; - ignore(replaceb#connect#clicked InvokeTactics'.replace) ; - ignore(reflexivityb#connect#clicked InvokeTactics'.reflexivity) ; - ignore(symmetryb#connect#clicked InvokeTactics'.symmetry) ; - ignore(transitivityb#connect#clicked InvokeTactics'.transitivity) ; - ignore(existsb#connect#clicked InvokeTactics'.exists) ; - ignore(splitb#connect#clicked InvokeTactics'.split) ; - ignore(leftb#connect#clicked InvokeTactics'.left) ; - ignore(rightb#connect#clicked InvokeTactics'.right) ; - ignore(assumptionb#connect#clicked InvokeTactics'.assumption) ; - ignore(absurdb#connect#clicked InvokeTactics'.absurd) ; - ignore(contradictionb#connect#clicked InvokeTactics'.contradiction) ; - ignore(introsb#connect#clicked InvokeTactics'.intros) ; - ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ; - ignore(searchpatternb#connect#clicked searchPattern) ; - ignore(injectionb#connect#clicked InvokeTactics'.injection) ; - ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ; - ignore(autob#connect#clicked InvokeTactics'.auto) ; -(* Zack: spostare in una toolbar - ignore(whdb#connect#clicked whd) ; - ignore(reduceb#connect#clicked reduce) ; - ignore(simplb#connect#clicked simpl) ; - ignore(clearbodyb#connect#clicked clearbody) ; - ignore(clearb#connect#clicked clear) ; - ignore(generalizeb#connect#clicked generalize) ; -*) - ignore(proofw#connect#selection_changed (choose_selection proofw)) ; - ignore - ((new GObj.event_ops proofw#as_widget)#connect#button_press - (open_contextual_menu_for_selected_terms proofw)) ; - )) -end -;; - -class empty_page = - let vbox1 = GPack.vbox () in - let scrolled_window1 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox1#pack ~expand:true ~padding:5) () in - let proofw = - TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent - ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in -object(self) - method proofw = (assert false : TermViewer.sequent_viewer) - method content = vbox1 - method compute = (assert false : unit) -end -;; - -let empty_page = new empty_page;; - -class notebook = -object(self) - val notebook = GPack.notebook () - val pages = ref [] - val mutable skip_switch_page_event = false - val mutable empty = true - method notebook = notebook - method add_page n = - let new_page = new page () in - empty <- false ; - pages := !pages @ [n,lazy (setgoal n),new_page] ; - notebook#append_page - ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce) - new_page#content#coerce - method remove_all_pages ~skip_switch_page_event:skip = - if empty then - notebook#remove_page 0 (* let's remove the empty page *) - else - List.iter (function _ -> notebook#remove_page 0) !pages ; - pages := [] ; - skip_switch_page_event <- skip - method set_current_page ~may_skip_switch_page_event n = - let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in - let new_page = notebook#page_num page#content#coerce in - if may_skip_switch_page_event && new_page <> notebook#current_page then - skip_switch_page_event <- true ; - notebook#goto_page new_page - method set_empty_page = - empty <- true ; - pages := [] ; - notebook#append_page - ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce) - empty_page#content#coerce - method proofw = - let (_,_,page) = List.nth !pages notebook#current_page in - page#proofw - initializer - ignore - (notebook#connect#switch_page - (function i -> - let skip = skip_switch_page_event in - skip_switch_page_event <- false ; - if not skip then - try - let (metano,setgoal,page) = List.nth !pages i in - set_proof_engine_goal (Some metano) ; - Lazy.force (page#compute) ; - Lazy.force setgoal; - if notify_hbugs_on_goal_change then - Hbugs.notify () - with _ -> () - )) -end -;; - -let dump_environment () = - try - let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in - HelmLogger.log (`Msg (`T "Dumping environment ...")); - CicEnvironment.dump_to_channel oc; - HelmLogger.log (`Msg (`T "... done!")) ; - close_out oc - with exc -> - HelmLogger.log - (`Error (`T (Printf.sprintf "Dump failure, uncaught exception:%s" - (Printexc.to_string exc)))) -;; -let restore_environment () = - try - let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in - HelmLogger.log (`Msg (`T "Restoring environment ... ")); - CicEnvironment.restore_from_channel ic; - HelmLogger.log (`Msg (`T "... done!")); - close_in ic - with exc -> - HelmLogger.log - (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s" - (Printexc.to_string exc)))) -;; - -(* Main window *) - -class rendering_window output (notebook : notebook) = - let scratch_window = new scratch_window in - let window = - GWindow.window - ~title:"gTopLevel - Helm's Proof Assistant" - ~border_width:0 ~allow_shrink:false () in - let vbox_for_menu = GPack.vbox ~packing:window#add () in - (* menus *) - let handle_box = GBin.handle_box ~border_width:2 - ~packing:(vbox_for_menu#pack ~padding:0) () in - let menubar = GMenu.menu_bar ~packing:handle_box#add () in - let factory0 = new GMenu.factory menubar in - let accel_group = factory0#accel_group in - (* file menu *) - let file_menu = factory0#add_submenu "File" in - let factory1 = new GMenu.factory file_menu ~accel_group in - (* let export_to_postscript_menu_item = *) - let _ = - begin - let _ = - factory1#add_item "New Block of (Co)Inductive Definitions..." - ~key:GdkKeysyms._B ~callback:new_inductive - in - let _ = - factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N - ~callback:new_proof - in - let reopen_menu_item = - factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R - ~callback:open_ - in - let qed_menu_item = - factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in - ignore (factory1#add_separator ()) ; - ignore - (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L - ~callback:load_unfinished_proof) ; - let save_menu_item = - factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S - ~callback:save_unfinished_proof - in - ignore (factory1#add_separator ()) ; - ignore (factory1#add_item "Clear Environment" ~callback:CicEnvironment.empty); - ignore (factory1#add_item "Dump Environment" ~callback:dump_environment); - ignore - (factory1#add_item "Restore Environment" ~callback:restore_environment); - ignore - (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b); - ignore (!save_set_sensitive false); - ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b); - ignore (!qed_set_sensitive false); - ignore (factory1#add_separator ()) ; - (* - let export_to_postscript_menu_item = - factory1#add_item "Export to PostScript..." - ~callback:(export_to_postscript output) in - *) - ignore (factory1#add_separator ()) ; - ignore - (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) (*; - export_to_postscript_menu_item *) - end in - (* edit menu *) - let edit_menu = factory0#add_submenu "Edit Current Proof" in - let factory2 = new GMenu.factory edit_menu ~accel_group in - let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in - let proveit_menu_item = - factory2#add_item "Prove It" ~key:GdkKeysyms._I - ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false) - in - let focus_menu_item = - factory2#add_item "Focus" ~key:GdkKeysyms._F - ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false) - in - let _ = - focus_and_proveit_set_sensitive := - function b -> - proveit_menu_item#misc#set_sensitive b ; - focus_menu_item#misc#set_sensitive b - in - let _ = !focus_and_proveit_set_sensitive false in - (* edit term menu *) - let edit_term_menu = factory0#add_submenu "Edit Term" in - let factory5 = new GMenu.factory edit_term_menu ~accel_group in - let check_menu_item = - factory5#add_item "Check Term" ~key:GdkKeysyms._C - ~callback:(check scratch_window) in - let _ = check_menu_item#misc#set_sensitive false in - (* search menu *) - let search_menu = factory0#add_submenu "Search" in - let factory4 = new GMenu.factory search_menu ~accel_group in - let _ = - factory4#add_item "Locate..." ~key:GdkKeysyms._T - ~callback:locate in - let searchPattern_menu_item = - factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D - ~callback:completeSearchPattern in - let _ = searchPattern_menu_item#misc#set_sensitive false in - let show_menu_item = - factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show - in - let insert_query_item = - factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._Y - ~callback:insertQuery in - (* hbugs menu *) - let hbugs_menu = factory0#add_submenu "HBugs" in - let factory6 = new GMenu.factory hbugs_menu ~accel_group in - let _ = - factory6#add_check_item - ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled" - in - let _ = - factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify - "(Re)Submit status!" - in - let _ = factory6#add_separator () in - let _ = - factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services" - in - let _ = - factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services" - in - (* settings menu *) - let settings_menu = factory0#add_submenu "Settings" in - let factory3 = new GMenu.factory settings_menu ~accel_group in - let _ = - factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A - ~callback:edit_aliases in - let _ = - factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K - ~callback:clear_aliases in - let autoitem = - factory3#add_check_item "Auto disambiguation" - ~callback:(fun checked -> auto_disambiguation := checked) in - let _ = factory3#add_separator () in - let _ = - factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P - ~callback:(function _ -> (settings_window ())#show ()) in - let _ = factory3#add_separator () in - let _ = - factory3#add_item "Reload Stylesheets" - ~callback: - (function _ -> - ChosenTransformer.reload_stylesheets () ; - if ProofEngine.get_proof () <> None then - try - refresh_goals notebook ; - refresh_proof output - with - InvokeTactics.RefreshSequentException e -> - HelmLogger.log - (`Error (`T ("An error occurred while refreshing the " ^ - "sequent: " ^ Printexc.to_string e))) ; - (*notebook#remove_all_pages ~skip_switch_page_event:false ;*) - notebook#set_empty_page - | InvokeTactics.RefreshProofException e -> - HelmLogger.log - (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ; - output#unload - ) in - (* accel group *) - let _ = window#add_accel_group accel_group in - (* end of menus *) - let hbox0 = - GPack.hbox - ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in - let vbox = - GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in - let scrolled_window0 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox#pack ~expand:true ~padding:5) () in - let _ = scrolled_window0#add output#coerce in - let frame = - GBin.frame ~label:"Insert Term" - ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let scrolled_window1 = - GBin.scrolled_window ~border_width:5 - ~packing:frame#add () in - let inputt = - TermEditor'.term_editor - mqi_handle - ~width:400 ~height:100 ~packing:scrolled_window1#add () - ~isnotempty_callback: - (function b -> - check_menu_item#misc#set_sensitive b ; - searchPattern_menu_item#misc#set_sensitive b) in - let vboxl = - GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in - let _ = - vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in - let frame = - GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) () - in - let _ = - new HelmGtkLogger.html_logger - ~width:400 ~height: 100 ~show:true ~packing:frame#add () - in -object - method inputt = inputt - method output = (output : TermViewer.proof_viewer) - method scratch_window = scratch_window - method notebook = notebook - method show = window#show - method set_auto_disambiguation set = autoitem#set_active set - initializer - notebook#set_empty_page ; - (*export_to_postscript_menu_item#misc#set_sensitive false ;*) - check_term := (check_term_in_scratch scratch_window) ; - - (* signal handlers here *) - ignore(output#connect#selection_changed - (function elem -> - choose_selection output elem ; - !focus_and_proveit_set_sensitive true - )) ; - ignore (output#connect#click (show_in_show_window_callback output)) ; - let settings_window = new settings_window output scrolled_window0 - (*export_to_postscript_menu_item*)() (choose_selection output) in - set_settings_window settings_window ; - ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) -end - -(* MAIN *) - -let initialize_everything () = - let output = - TermViewer.proof_viewer - ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object - ~width:350 ~height:280 () - in - let notebook = new notebook in - let rendering_window' = new rendering_window output notebook in - rendering_window'#set_auto_disambiguation !auto_disambiguation; - set_rendering_window rendering_window'; - let print_error_as_html prefix msg = - HelmLogger.log (`Error (`T (prefix ^ msg))) - in - Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: ")); - Gdome_xslt.setDebugCallback - (Some (print_error_as_html "XSLT Debug Message: ")); - rendering_window'#show () ; - if restore_environment_on_boot && - Sys.file_exists (Helm_registry.get "gtoplevel.environment_file") - then - restore_environment (); - GtkThread.main () -;; - -let main () = - ignore (GtkMain.Main.init ()) ; - initialize_everything () ; - MQIC.close mqi_handle; - Hbugs.quit () -;; - -try - Sys.catch_break true; - main (); -with Sys.Break -> () (* exit nicely, invoking at_exit functions *) -