-(* Copyright (C) 2000-2002, HELM Team.
+(* Copyright (C) 2000-2004, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* MA 02111-1307, USA.
*
* For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
+ * http://helm.cs.unibo.it/
*)
(******************************************************************************)
(* *)
(******************************************************************************)
-open Printf;;
+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 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_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
-(*
-let mqi_flags = [] (* default MathQL interpreter options *)
-*)
-let mqi_handle = MQIC.init mqi_flags prerr_string
+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 htmlheader =
- "<html>" ^
- " <body bgColor=\"white\">"
-;;
+let restore_environment_on_boot = true ;;
+let notify_hbugs_on_goal_change = false ;;
-let htmlfooter =
- " </body>" ^
- "</html>"
-;;
-
-let prooffile =
- try
- Sys.getenv "GTOPLEVEL_PROOFFILE"
- with
- Not_found -> "/public/currentproof"
-;;
-
-let prooffiletype =
- try
- Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
- with
- Not_found -> "/public/currentprooftype"
-;;
+let auto_disambiguation = ref true ;;
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
-let htmlheader_and_content = ref htmlheader;;
-
let check_term = ref (fun _ _ _ -> assert false);;
exception RenderingWindowsNotInitialized;;
)
;;
-exception OutputHtmlNotInitialized;;
-
-let set_outputhtml,outputhtml =
- let outputhtml_ref = ref None in
- (function rw -> outputhtml_ref := Some rw),
- (function () ->
- match !outputhtml_ref with
- None -> raise OutputHtmlNotInitialized
- | Some outputhtml -> outputhtml
- )
-;;
-
exception QedSetSensitiveNotInitialized;;
let qed_set_sensitive =
ref (function _ -> raise QedSetSensitiveNotInitialized)
String.sub uri' 4 (String.length uri' - 4)
;;
-let output_html outputhtml msg =
- htmlheader_and_content := !htmlheader_and_content ^ msg ;
- outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
- outputhtml#set_topline (-1)
-;;
-
(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
(* Check window *)
-let check_window outputhtml uris =
+let check_window uris =
let window =
GWindow.window
~width:800 ~modal:true ~title:"Check" ~border_width:2 () 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 =
mmlwidget#load_sequent [] (111,[],expr)
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log (`Error (`T (Printexc.to_string e)))
)
) uris
in
ignore
(notebook#connect#switch_page
- (function i -> Lazy.force (List.nth render_terms i)))
+ (function i ->
+ Lazy.force (List.nth render_terms i)))
;;
exception NoChoice;;
-let
- interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
- ?(enable_button_for_non_vars=false) ~title ~msg uris
+let interactive_user_uri_choice
+ ~(selection_mode:[ `SINGLE | `MULTIPLE ])
+ ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris
=
- 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 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 (outputhtml ()) !choices
+ let only_constant_choices =
+ lazy
+ (List.filter
+ (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+ uris)
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 (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 () ;
+ 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 ;
- clist#misc#set_sensitive false
- end));
- window#set_position `CENTER ;
- window#show () ;
- GtkThread.main ();
- if !chosen then
- if !use_only_constants then
- List.filter
- (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
- uris
- else
- if List.length !choices > 0 then !choices else raise NoChoice
- else
- raise NoChoice
+ 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 =
GtkThread.main ();
match !chosen with
None -> raise NoChoice
- | Some n -> n
+ | Some n -> [n]
;;
(* innertypes *)
let innertypesuri = UriManager.innertypesuri_of_uri uri in
Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
- Getter.register innertypesuri
- (Configuration.annotations_url ^
+ 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")) ;
- Getter.register uri
- (Configuration.annotations_url ^
+ Http_getter.register' uri
+ (Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri uri) ^ ".xml"
) ;
| Some bodyuri -> bodyuri
in
Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
- Getter.register bodyuri
- (Configuration.annotations_url ^
+ Http_getter.register' bodyuri
+ (Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri bodyuri) ^ ".xml"
)
exception WrongProof;;
let pathname_of_annuri uristring =
- Configuration.annotations_dir ^
+ Helm_registry.get "local_library.dir" ^
Str.replace_first (Str.regexp "^cic:") "" uristring
;;
(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
+ 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
;;
let qed () =
- match !ProofEngine.proof with
+ 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
(** save an unfinished proof on the filesystem *)
let save_unfinished_proof () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
- Xml.pp ~quiet:true xml (Some prooffiletype) ;
- output_html outputhtml
- ("<h1 color=\"Green\">Current proof type saved to " ^
- prooffiletype ^ "</h1>") ;
- Xml.pp ~quiet:true bodyxml (Some prooffile) ;
- output_html outputhtml
- ("<h1 color=\"Green\">Current proof body saved to " ^
- prooffile ^ "</h1>")
+ 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 *)
CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
| _ -> assert false)
(interactive_user_uri_choice
- ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
+ ~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,_) ->
)
;;
-let mk_fresh_name_callback context name ~typ =
+let mk_fresh_name_callback metasenv context name ~typ =
let fresh_name =
- match ProofEngineHelpers.mk_fresh_name context name ~typ with
+ match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with
Cic.Name fresh_name -> fresh_name
| Cic.Anonymous -> assert false
in
let refresh_proof (output : TermViewer.proof_viewer) =
try
let uri,currentproof =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- let bo_fixed = Eta_fixing.eta_fix metasenv bo in
- let ty_fixed = Eta_fixing.eta_fix metasenv ty in
- ProofEngine.proof := Some(uri,metasenv,bo_fixed,ty_fixed);
+ ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ;
if List.length metasenv = 0 then
begin
!qed_set_sensitive true ;
-prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ;
Hbugs.clear ()
end
else
-begin
-prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ;
Hbugs.notify () ;
-end ;
(*CSC: Wrong: [] is just plainly wrong *)
- uri,
- (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo_fixed, ty_fixed, []))
+ 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.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
-prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
- raise (InvokeTactics.RefreshProofException e)
+ 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
notebook#proofw#unload
| Some metano ->
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
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
+ 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 =
| Some m -> m
in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
try
-let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
- prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
- raise (InvokeTactics.RefreshSequentException e)
-with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
+ 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 decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
- let output_html msg = output_html (outputhtml ()) msg
+ 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 outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
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.con"
+ 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
- match CicParser.obj_of_xml prooffiletype (Some prooffile) with
+ 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.proof :=
- Some (uri, metasenv, bo, ty) ;
- ProofEngine.goal :=
+ ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty));
+ refresh_proof output ;
+ set_proof_engine_goal
(match metasenv with
[] -> None
| (metano,_,_)::_ -> Some metano
) ;
- refresh_proof output ;
refresh_goals notebook ;
- output_html outputhtml
- ("<h1 color=\"Green\">Current proof type loaded from " ^
- prooffiletype ^ "</h1>") ;
- output_html outputhtml
- ("<h1 color=\"Green\">Current proof body loaded from " ^
- prooffile ^ "</h1>") ;
+ 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 ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ 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 id_to_uris = inputt#id_to_uris in
- let chosen = ref false 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 scrolled_window =
GBin.scrolled_window ~border_width:10
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
- let input = GEdit.text ~editable:true ~width:400 ~height:100
+ let input = GText.view ~editable:true ~width:400 ~height:100
~packing:scrolled_window#add () in
let hbox =
GPack.hbox ~border_width:0
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
- (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
- let dom,resolve_id = !id_to_uris in
+ 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#insert_text ~pos:0
- (String.concat "\n"
- (List.map
- (function v ->
- let uri =
- match resolve_id v with
- None -> assert false
- | Some (CicTextualParser0.Uri uri) -> uri
- | Some (CicTextualParser0.Term _)
- | Some CicTextualParser0.Implicit -> assert false
- in
- "alias " ^
- (match v with
- CicTextualParser0.Id id -> id
- | CicTextualParser0.Symbol (descr,_) ->
- (* CSC: To be implemented *)
- assert false
- )^ " " ^ (string_of_cic_textual_parser_uri uri)
- ) dom))) ;
+ (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
+ (DisambiguatingParser.EnvironmentP3.to_string !disambiguation_env ^ "\n"));
window#show () ;
GtkThread.main ();
- if !chosen then
- let dom,resolve_id =
- let inputtext = input#get_chars 0 input#length in
- let regexpr =
- let alfa = "[a-zA-Z_-]" in
- let digit = "[0-9]" in
- let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
- let blanks = "\( \|\t\|\n\)+" in
- let nonblanks = "[^ \t\n]+" in
- let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
- Str.regexp
- ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
- in
- let rec aux n =
- try
- let n' = Str.search_forward regexpr inputtext n in
- let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
- let uri =
- MQueryMisc.cic_textual_parser_uri_of_string
- ("cic:" ^ (Str.matched_group 5 inputtext))
- in
- let dom,resolve_id = aux (n' + 1) in
- if List.mem id dom then
- dom,resolve_id
- else
- id::dom,
- (function id' ->
- if id = id' then
- Some (CicTextualParser0.Uri uri)
- else resolve_id id')
- with
- Not_found -> TermEditor.empty_id_to_uris
- in
- aux 0
- in
- id_to_uris := (dom,resolve_id)
+ 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 G = Gdome in
let notebook = (rendering_window ())#notebook in
let output = (rendering_window ())#output in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
output#make_sequent_of_selected_term ;
refresh_proof output ;
refresh_goals notebook
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ 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 outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = (rendering_window ())#output in
try
output#focus_sequent_of_selected_term ;
refresh_goals notebook
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
exception NoPrevGoal;;
let module L = LogicalOperations in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window ())#output in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
refresh_goals ~empty_notebook:false notebook
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let
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 =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let
(acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
Cic2acic.acic_object_of_cic_object obj
in
let mml =
- ApplyStylesheets.mml_of_cic_object
+ 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) ;
mmlwidget#load_doc mml ;
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
in
let show_in_show_window_uri uri =
let obj = CicEnvironment.get_obj uri in
;;
let locate_callback id =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let out = output_html outputhtml in
let query = MQG.locate id in
let result = MQI.execute mqi_handle query in
let uris =
(function uri,_ ->
MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
- out "<h1>Locate Query: </h1><pre>";
- MQueryUtil.text_of_query out query "";
- out "<h1>Result:</h1>";
- MQueryUtil.text_of_result out result "<br>";
+ 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 ^
ignore
(cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
let check_callback () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let uri = "cic:" ^ manual_input#text in
try
- ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
- output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
+ ignore (Http_getter.resolve' (UriManager.uri_of_string uri)) ;
+ HelmLogger.log (`Msg (`T "OK")) ;
true
with
- Getter.Unresolved ->
- output_html outputhtml
- ("<h1 color=\"Red\">URI " ^ uri ^
- " does not correspond to any object.</h1>") ;
+ Http_getter_types.Unresolvable_URI _ ->
+ HelmLogger.log
+ (`Error (`T ("URI " ^ uri ^
+ " does not correspond to any object."))) ;
false
| UriManager.IllFormedUri _ ->
- output_html outputhtml
- ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
+ HelmLogger.log
+ (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ;
false
| e ->
- output_html outputhtml
- ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e))) ;
false
in
ignore
(* A WIDGET TO ENTER CIC TERMS *)
-module ChosenTermEditor = TexTermEditor;;
-module ChosenTextualParser0 = TexCicTextualParser0;;
-(*
-module ChosenTermEditor = TermEditor;;
-module ChosenTextualParser0 = CicTextualParser0;;
-*)
-
-module Callbacks =
+module DisambiguateCallbacks =
struct
- let get_metasenv () = !ChosenTextualParser0.metasenv
- let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
-
- let output_html msg = output_html (outputhtml ()) msg;;
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 = input_or_locate_uri;;
+ ?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 TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
+module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);;
(* OTHER FUNCTIONS *)
let locate () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
match
GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
inputt#set_term uri
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let new_inductive () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
begin
try
- ignore (Getter.resolve uri) ;
+ ignore (Http_getter.resolve' uri) ;
raise UriAlreadyInUse
- with
- Getter.Unresolved ->
+ with Http_getter_types.Unresolvable_URI _ ->
get_uri := (function () -> uri) ;
get_names := (function () -> names) ;
inductive := inductiveb#active ;
end
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
))
(* Second phase *)
and phase2 () =
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TexTermEditor'.term_editor
+ TermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(*non_empty_type := b ;*)
window#destroy ()
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
))
(* Third phase *)
and phase3 name cons =
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TexTermEditor'.term_editor
+ TermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(* (*non_empty_type := b ;*)
window2#destroy ()
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
)) ;
window2#show () ;
GtkThread.main ();
(*CSC: Da finire *)
let params = [] in
let tys = !get_types_and_cons () in
- let obj = Cic.InductiveDefinition tys params !paramsno in
+ let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
begin
try
- prerr_endline (CicPp.ppobj obj) ;
+ debug_print (CicPp.ppobj obj);
CicTypeChecker.typecheck_mutual_inductive_defs uri
(tys,params,!paramsno) ;
with
e ->
- prerr_endline "Offending mutual (co)inductive type declaration:" ;
- prerr_endline (CicPp.ppobj obj) ;
+ 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 *)
show_in_show_window_obj uri obj
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let new_proof () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook 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
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- TexTermEditor'.term_editor
+ TermEditor'.term_editor
mqi_handle
~width:400 ~height:100 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
non_empty_type := b ;
okb#misc#set_sensitive (b && uri_entry#text <> ""))
in
let _ =
-let xxx = inputt#get_as_string in
-prerr_endline ("######################## " ^ xxx) ;
- newinputt#set_term xxx ;
-(*
- newinputt#set_term inputt#get_as_string ;
-*)
+ newinputt#set_term inputt#get_as_string ;
inputt#reset in
let _ =
uri_entry#connect#changed
else
begin
try
- ignore (Getter.resolve uri) ;
+ ignore (Http_getter.resolve' uri) ;
raise UriAlreadyInUse
- with
- Getter.Unresolved ->
+ with Http_getter_types.Unresolvable_URI _ ->
get_metasenv_and_term := (function () -> metasenv,parsed) ;
get_uri := (function () -> uri) ;
window#destroy ()
end
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
)) ;
window#show () ;
GtkThread.main ();
try
let metasenv,expr = !get_metasenv_and_term () in
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
- ProofEngine.proof :=
- Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
- ProofEngine.goal := Some 1 ;
+ 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 ;
refresh_proof output
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let check_term_in_scratch scratch_window metasenv context expr =
let check scratch_window () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> []
| Some (_,metasenv,_,_) -> metasenv
in
check_term_in_scratch scratch_window metasenv' context expr
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let show () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
show_in_show_window_uri (input_or_locate_uri ~title:"Show")
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
exception NotADefinition;;
let open_ () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
in
- ProofEngine.proof :=
- Some (uri, metasenv, bo, ty) ;
- ProofEngine.goal := None ;
+ 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 ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let show_query_results results =
let completeSearchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
- let must = MQueryLevels2.get_constraints expr in
+ let must = CGSearchPattern.get_constraints expr in
let must',only = refine_constraints must in
let query =
- MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
+ MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
in
let results = MQI.execute mqi_handle query in
show_query_results results
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let insertQuery () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let chosen = ref None in
let window =
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 = GEdit.text ~editable:true
+ 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
ignore
(okb#connect#clicked
(function () ->
- chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
+ chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ;
ignore
(loadb#connect#clicked
(function () ->
End_of_file -> ""
in
let text = read_file () in
- input#delete_text 0 input#length ;
- ignore (input#insert_text text ~pos:0))) ;
+ input#buffer#delete input#buffer#start_iter input#buffer#end_iter ;
+ ignore (input#buffer#insert text))) ;
window#set_position `CENTER ;
window#show () ;
GtkThread.main ();
show_query_results results
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let choose_must list_of_must only =
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:false n
) must
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
let clist =
GList.clist ~columns:2 ~packing:scrolled_window#add
- ~selection_mode:`EXTENDED
+ ~selection_mode:`MULTIPLE
~titles:["URI" ; "Position"] ()
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:true n
) only
let searchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let proof =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some proof -> proof
in
| None -> ()
| Some metano ->
let uris' =
- TacticChaser.matchConclusion
- mqi_handle
- ~output_html:(output_html outputhtml) ~choose_must ()
- ~status:(proof, metano)
+ TacticChaser.matchConclusion mqi_handle
+ ~choose_must () (proof, metano)
in
let uri' =
user_uri_choice ~title:"Ambiguous input."
InvokeTactics'.apply ()
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
;;
let choose_selection mmlwidget (element : Gdome.element option) =
| Some p -> aux (new Gdome.element_of_node p)
with
GdomeInit.DOMCastException _ ->
- prerr_endline
+ debug_print
"******* trying to select above the document root ********"
in
match element with
(* Stuff for the widget settings *)
+(*
let export_to_postscript output =
let lastdir = ref (Unix.getcwd ()) in
function () ->
(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 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
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)
~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 *)
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- TermViewer.sequent_viewer ~width:400 ~height:275
- ~packing:(scrolled_window1#add) () in
+ 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 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 =
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) ;
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- TermViewer.sequent_viewer ~width:400 ~height:275
- ~packing:(scrolled_window1#add) () in
+ 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
if not skip then
try
let (metano,setgoal,page) = List.nth !pages i in
- ProofEngine.goal := Some metano ;
+ set_proof_engine_goal (Some metano) ;
Lazy.force (page#compute) ;
- Lazy.force setgoal
+ 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) =
(* 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 export_to_postscript_menu_item = *)
+ let _ =
begin
let _ =
factory1#add_item "New Block of (Co)Inductive Definitions..."
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
+ (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
(* hbugs menu *)
let hbugs_menu = factory0#add_submenu "HBugs" in
let factory6 = new GMenu.factory hbugs_menu ~accel_group in
- let toggle_hbugs_menu_item =
+ 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
factory3#add_item "Reload Stylesheets"
~callback:
(function _ ->
- ApplyStylesheets.reload_stylesheets () ;
- if !ProofEngine.proof <> None then
+ ChosenTransformer.reload_stylesheets () ;
+ if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
refresh_proof output
with
InvokeTactics.RefreshSequentException e ->
- output_html (outputhtml ())
- ("<h1 color=\"red\">An error occurred while refreshing the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ 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 ->
- output_html (outputhtml ())
- ("<h1 color=\"red\">An error occurred while refreshing the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ HelmLogger.log
+ (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ;
output#unload
) in
(* accel group *)
GBin.scrolled_window ~border_width:5
~packing:frame#add () in
let inputt =
- TexTermEditor'.term_editor
+ TermEditor'.term_editor
mqi_handle
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
let frame =
GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
in
- let outputhtml =
- GHtml.xmhtml
- ~source:"<html><body bgColor=\"white\"></body></html>"
- ~width:400 ~height: 100
- ~border_width:20
- ~packing:frame#add
- ~show:true () in
+ let _ =
+ new HelmGtkLogger.html_logger
+ ~width:400 ~height: 100 ~show:true ~packing:frame#add ()
+ in
object
- method outputhtml = outputhtml
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 ;
+ (*export_to_postscript_menu_item#misc#set_sensitive false ;*)
check_term := (check_term_in_scratch scratch_window) ;
(* signal handlers here *)
)) ;
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
+ (*export_to_postscript_menu_item*)() (choose_selection output) in
set_settings_window settings_window ;
- set_outputhtml outputhtml ;
- ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
- Logger.log_callback :=
- (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
-end;;
+ ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
+end
(* MAIN *)
let initialize_everything () =
- let module U = Unix in
- let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
+ 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
- set_rendering_window rendering_window' ;
- let print_error_as_html prefix msg =
- output_html (outputhtml ())
- ("<h1 color=\"red\">" ^ prefix ^ msg ^ "</h1>")
- 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 () ;
-(* Hbugs.toggle true; *)
- GtkThread.main ()
+ 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 () =
projects / helm.git / blobdiff