X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=e0e0bfca3385ec92996bd07da6ad0a4c4b8be674;hb=8dc254e60fb7ee127568bf1b0e5050f49b5167e1;hp=76ebe6cc6f453ed657e0ac683f9f1773302eb5b7;hpb=12809955a4a6c693072f5b924603165f83cc382e;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 76ebe6cc6..e0e0bfca3 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -33,7 +33,10 @@
 (*                                                                            *)
 (******************************************************************************)
 
-open Printf;;
+let debug_level = ref 1
+let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s
+
+open Printf
 
 (* DEBUGGING *)
 
@@ -45,11 +48,9 @@ module MQG  = MQueryGenerator
 
 (* 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_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
+let mqi_handle = MQIC.init mqi_flags mqi_debug_fun
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
@@ -77,6 +78,8 @@ let environmentfile =
 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);;
@@ -221,110 +224,131 @@ let
  interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(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 !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 (outputhtml ()) !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 =
@@ -572,8 +596,8 @@ let refresh_proof (output : TermViewer.proof_viewer) =
  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
@@ -633,10 +657,13 @@ let metasenv =
   | 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
@@ -717,10 +744,17 @@ let load_unfinished_proof () =
        (`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#environment 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
@@ -737,21 +771,37 @@ let edit_aliases () =
  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 ())) ;
+ 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.Environment.to_string !id_to_uris)) ;
+     (DisambiguatingParser.EnvironmentP3.to_string !disambiguation_env ^ "\n"));
   window#show () ;
   GtkThread.main ();
-  if !chosen then
-   id_to_uris :=
-    DisambiguatingParser.Environment.of_string (input#buffer#get_text ())
+  match !chosen_aliases with
+  | None -> ()
+  | Some raw_aliases ->
+      let new_disambiguation_env =
+        (try
+          DisambiguatingParser.EnvironmentP3.of_string raw_aliases
+        with e ->
+          output_html (outputhtml ())
+            (`Error (`T
+              ("Error while parsing aliases: " ^ Printexc.to_string e)));
+          !disambiguation_env)
+      in
+      disambiguation_env := new_disambiguation_env
 ;;
 
 let proveit () =
@@ -759,7 +809,7 @@ 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
+ let outputhtml = (rendering_window ())#outputhtml in
   try
    output#make_sequent_of_selected_term ;
    refresh_proof output ;
@@ -1043,7 +1093,7 @@ module Callbacks =
  end
 ;;
 
-module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
+module TermEditor' = ChosenTermEditor.Make(Callbacks);;
 
 (* OTHER FUNCTIONS *)
 
@@ -1189,7 +1239,7 @@ let new_inductive () =
        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_environment_with:inputt ()
@@ -1301,7 +1351,7 @@ let new_inductive () =
        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_environment_with:inputt ()
@@ -1379,13 +1429,13 @@ let new_inductive () =
      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 *)
@@ -1448,7 +1498,7 @@ let new_proof () =
    ~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_environment_with:inputt ()
@@ -2106,7 +2156,7 @@ 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
@@ -2748,6 +2798,12 @@ class rendering_window output (notebook : notebook) =
  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
@@ -2793,7 +2849,7 @@ class rendering_window output (notebook : notebook) =
   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:
@@ -2808,10 +2864,9 @@ class rendering_window output (notebook : notebook) =
   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
  in
  let outputhtml =
-  new Ui_logger.html_logger
-   ~width:400 ~height: 100
-   ~packing:frame#add
-   ~show:true () in
+   new Ui_logger.html_logger
+    ~width:400 ~height: 100 ~show:true ~packing:frame#add ()
+ in
 object
  method outputhtml = outputhtml
  method inputt = inputt
@@ -2819,6 +2874,7 @@ object
  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 ;*)
@@ -2846,6 +2902,7 @@ let initialize_everything () =
   let output = TermViewer.proof_viewer ~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 =
      output_html (outputhtml ()) (`Error (`T (prefix ^ msg)))