(* DEBUGGING *)
-let debug_print =
- let debug = true in
- fun s -> prerr_endline (sprintf "DEBUG: %s" s)
-;;
+module MQI = MQueryInterpreter
+module MQIC = MQIConn
(* GLOBAL CONSTANTS *)
+let mqi_flags = [] (* default MathQL interpreter options *)
+let mqi_handle = MQIC.init mqi_flags prerr_string
+
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
let htmlheader =
Not_found -> "/public/currentprooftype"
;;
-let postgresqlconnectionstring =
- try
- Sys.getenv "POSTGRESQL_CONNECTION_STRING"
- with
- Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
-;;
-
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
let htmlheader_and_content = ref htmlheader;;
(* CALLBACKS *)
-(*
-ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
- ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
-*)
-
exception OpenConjecturesStillThere;;
exception WrongProof;;
match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- !qed_set_sensitive (List.length metasenv = 0) ;
+ 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, ty, []))
raise (InvokeTactics.RefreshSequentException e)
with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
-let __notify_hbugs = ref None;;
module InvokeTacticsCallbacks =
struct
let sequent_viewer () = (rendering_window ())#notebook#proofw
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 notify_hbugs () =
- match !__notify_hbugs with
- | Some f -> f ()
- | None -> assert false
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
-module Hbugs' = Hbugs.Make (InvokeTactics');;
-__notify_hbugs := Some Hbugs'.notify;;
+(* Just to initialize the Hbugs module *)
+module Ignore = Hbugs.Initialize (InvokeTactics');;
(** load an unfinished proof from filesystem *)
let load_unfinished_proof () =
("<h1 color=\"Green\">Current proof body loaded from " ^
prooffile ^ "</h1>") ;
!save_set_sensitive true;
- Hbugs'.notify ()
| _ -> assert false
with
InvokeTactics.RefreshSequentException e ->
let uri =
match resolve_id v with
None -> assert false
- | Some uri -> uri
+ | Some (CicTextualParser0.Uri uri) -> uri
+ | Some (CicTextualParser0.Term _)
+ | Some CicTextualParser0.Implicit -> assert false
in
- "alias " ^ v ^ " " ^
- (string_of_cic_textual_parser_uri uri)
+ "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))) ;
window#show () ;
GtkThread.main ();
let rec aux n =
try
let n' = Str.search_forward regexpr inputtext n in
- let id = Str.matched_group 2 inputtext 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))
dom,resolve_id
else
id::dom,
- (function id' -> if id = id' then Some uri else resolve_id id')
+ (function id' ->
+ if id = id' then
+ Some (CicTextualParser0.Uri uri)
+ else resolve_id id')
with
Not_found -> TermEditor.empty_id_to_uris
in
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) _ =
- 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)
+ 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)
let locate_callback id =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let result = MQueryGenerator.locate id in
+ let result = MQueryGenerator.locate mqi_handle id in
let uris =
List.map
(function uri,_ ->
(* A WIDGET TO ENTER CIC TERMS *)
+module ChosenTermEditor = TexTermEditor;;
+module ChosenTextualParser0 = TexCicTextualParser0;;
+(*
+module ChosenTermEditor = TermEditor;;
+module ChosenTextualParser0 = CicTextualParser0;;
+*)
+
module Callbacks =
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 ->
end
;;
-module Disambiguate' = Disambiguate.Make(Callbacks);;
-
-module TermEditor' = TermEditor.Make(Callbacks);;
+module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
(* OTHER FUNCTIONS *)
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
+ mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
+ mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+ TexTermEditor'.term_editor
+ mqi_handle
+ ~width:400 ~height:100 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function 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 ;
+*)
inputt#reset in
let _ =
uri_entry#connect#changed
!save_set_sensitive true ;
inputt#reset ;
ProofEngine.intros ~mk_fresh_name_callback () ;
- Hbugs'.notify ();
refresh_goals notebook ;
refresh_proof output
with
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
let must = MQueryLevels2.get_constraints expr in
let must',only = refine_constraints must in
- let results = MQueryGenerator.searchPattern must' only in
+ let results = MQueryGenerator.searchPattern mqi_handle must' only in
show_query_results results
with
e ->
None -> ()
| Some q ->
let results =
- Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
+ MQI.execute mqi_handle (MQueryUtil.query_of_text (Lexing.from_string q))
in
show_query_results results
with
| Some metano ->
let uris' =
TacticChaser.searchPattern
+ mqi_handle
~output_html:(output_html outputhtml) ~choose_must ()
~status:(proof, metano)
in
factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
in
let insert_query_item =
- factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
+ 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 toggle_hbugs_menu_item =
factory6#add_check_item
- ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs'.toggle "HBugs enabled"
+ ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
in
(* settings menu *)
let settings_menu = factory0#add_submenu "Settings" in
GBin.scrolled_window ~border_width:5
~packing:frame#add () in
let inputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
+ mqi_handle
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
- rendering_window'#show () ;
-(* Hbugs'.toggle true; *)
- GtkThread.main ()
+ 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 main () =
- if !usedb then
- begin
- Mqint.set_database Mqint.postgres_db ;
- Mqint.init postgresqlconnectionstring ;
- end ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
- if !usedb then Mqint.close ();
- prerr_endline "FOO";
- Hbugs'.quit ()
+ MQIC.close mqi_handle;
+ Hbugs.quit ()
;;
try
projects / helm.git / blobdiff