- moved applyTransformation initialization code to the relevant library

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 8643ec313ed053896d57eebe739c09836f29731f..e70946564a53b64b1d3b754b0e3b854429210993 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -62,8 +62,7 @@ let _ =
 (* GLOBAL CONSTANTS *)
 
 let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
-let mqi_handle = MQIC.init mqi_flags mqi_debug_fun
+let mqi_handle = MQIC.init ~log:mqi_debug_fun ()
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
@@ -173,6 +172,7 @@ let check_window uris =
       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 =
@@ -197,9 +197,9 @@ let check_window uris =
 
 exception NoChoice;;
 
-let
- interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(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 only_constant_choices =
    lazy
@@ -380,7 +380,7 @@ let interactive_interpretation_choice interpretations =
  GtkThread.main ();
  match !chosen with
     None -> raise NoChoice
-  | Some n -> n
+  | Some n -> [n]
 ;;
 
 
@@ -659,6 +659,7 @@ module InvokeTacticsCallbacks =
 
   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);;
@@ -1055,7 +1056,7 @@ module DisambiguateCallbacks =
     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
+  let input_or_locate_uri ~title ?id = input_or_locate_uri ~title
  end
 ;;
 
@@ -2076,7 +2077,7 @@ let searchPattern () =
       | Some metano ->
          let uris' =
            TacticChaser.matchConclusion mqi_handle
-            ~choose_must () ~status:(proof, metano)
+            ~choose_must () (proof, metano)
          in
          let uri' =
           user_uri_choice ~title:"Ambiguous input."
@@ -2270,6 +2271,7 @@ class scratch_window =
    ~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 *)
@@ -2350,8 +2352,9 @@ object(self)
     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
@@ -2373,6 +2376,9 @@ object(self)
    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 =
@@ -2504,6 +2510,7 @@ object(self)
    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) ;
@@ -2526,8 +2533,9 @@ class empty_page =
   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
@@ -2844,7 +2852,11 @@ end
 (* MAIN *)
 
 let initialize_everything () =
-  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
   rendering_window'#set_auto_disambiguation !auto_disambiguation;