some fixes for whelp macros (concerning pprint...)

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index 83e5f3c18e42dd97a04222180ddb57f5bc1684a2..fe8d9e569d24a38a62c77b1d2bc1c1b310e62288 100644 (file)
--- a/matita/applyTransformation.ml
+++ b/matita/applyTransformation.ml
@@ -70,3 +70,17 @@ let mml_of_cic_object obj =
    (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
   ids_to_inner_sorts,ids_to_inner_types)))
 
+let txt_of_cic_sequent_conclusion size metasenv sequent = 
+  let _,(asequent,_,_,ids_to_inner_sorts,_) = 
+    Cic2acic.asequent_of_sequent metasenv sequent 
+  in
+  let _,_,_,t = Acic2content.map_sequent asequent in 
+  let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in
+  let t = TermContentPres.pp_ast t in
+  let t = CicNotationPres.render ids_to_uris t in
+  BoxPp.render_to_string size t
+
+let txt_of_cic_term size metasenv context t = 
+  let fake_sequent = (-1,context,t) in
+  txt_of_cic_sequent_conclusion size metasenv fake_sequent 
+

diff --git a/matita/applyTransformation.mli b/matita/applyTransformation.mli
index 8e023aea626f366cbfdc7cdf6778fa01f5854903..8e2d51b5b6713e06ad4b9f1b04cfefb11552409e 100644 (file)
--- a/matita/applyTransformation.mli
+++ b/matita/applyTransformation.mli
@@ -55,3 +55,8 @@ val mml_of_cic_object:
        (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
        (Cic.id, Cic2acic.anntypes) Hashtbl.t))  (* ids_to_inner_types *)
 
+val txt_of_cic_term: 
+  int -> Cic.metasenv -> Cic.context -> Cic.term -> string 
+val txt_of_cic_sequent_conclusion: 
+  int -> Cic.metasenv -> Cic.conjecture -> string
+

diff --git a/matita/matitaGtkMisc.ml b/matita/matitaGtkMisc.ml
index 553406635aac812e87ba39576f566bbe747f1e08..a41dbffe373713d3ca3fa5858e215f801afe5a58 100644 (file)
--- a/matita/matitaGtkMisc.ml
+++ b/matita/matitaGtkMisc.ml
@@ -28,16 +28,18 @@
 exception PopupClosed
 open Printf
 
-let wrap_callback f = f
+let wrap_callback0 f = fun _ -> try f () with Not_found -> assert false
+let wrap_callback1 f = fun _ -> try f () with Not_found -> assert false
+let wrap_callback2 f = fun _ -> try f () with Not_found -> assert false
 
 let connect_button (button: #GButton.button) callback =
-  ignore (button#connect#clicked (wrap_callback callback))
+  ignore (button#connect#clicked (wrap_callback0 callback))
 
 let connect_toggle_button (button: #GButton.toggle_button) callback =
-  ignore (button#connect#toggled (wrap_callback callback))
+  ignore (button#connect#toggled (wrap_callback1 callback))
 
 let connect_menu_item (menu_item: #GMenu.menu_item) callback =
-  ignore (menu_item#connect#activate (wrap_callback callback))
+  ignore (menu_item#connect#activate (wrap_callback2 callback))
 
 let connect_key (ev:GObj.event_ops) ?(modifiers = []) ?(stop = false) key
   callback

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 746ef8ffa67c74c7bdc455ca7e23d25e0d976d4e..aa1b16a2871da2dd07959af03b24da61fe19716e 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -338,7 +338,8 @@ object (self)
                 (fun uri ->
                   let menu_item =
                     GMenu.menu_item ~label:uri ~packing:menu#append () in
-                  connect_menu_item menu_item (fun () -> f uri))
+                  connect_menu_item menu_item 
+                  (fun () -> try f uri with Not_found -> assert false))
                 uris;
               menu#popup ~button ~time)
 
@@ -424,6 +425,7 @@ object (self)
     let script = MatitaScript.current () in
     let metasenv =
       if script#onGoingProof () then script#proofMetasenv else [] in
+    (*
     let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
       Cic2acic.asequent_of_sequent metasenv cic_sequent in
     let _, _, _, annterm = acic_sequent in
@@ -432,6 +434,9 @@ object (self)
     let pped_ast = TermContentPres.pp_ast ast in
     let markup = CicNotationPres.render ids_to_uris pped_ast in
     BoxPp.render_to_string text_width markup
+    *)
+    ApplyTransformation.txt_of_cic_sequent_conclusion 
+      text_width metasenv cic_sequent
 
   method private pattern_of term context unsh_sequent =
     let context_len = List.length context in
@@ -765,6 +770,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   in
   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
   let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
+  let do_not_execute_whelp_query = ref false in
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
@@ -779,17 +785,18 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       | h::_ when String.lowercase h = q' -> i
       | _::tl -> aux (i+1) tl
     in
+    win#queryInputText#set_text input;
+    do_not_execute_whelp_query:=true;
     combo#set_active (aux 0 queries);
-    win#queryInputText#set_text input
   in
   let set_whelp_query txt =
     let query, arg = 
       try
         let q = Pcre.extract ~rex:whelp_query_RE txt in
         q.(1), q.(2)
-      with Invalid_argument _ -> failwith "Malformed Whelp query"
+      with Not_found -> failwith "Malformed Whelp query"
     in
-    activate_combo_query arg query
+    activate_combo_query arg query;
   in
   let toplevel = win#toplevel in
   let mathView = cicMathView ~packing:win#scrolledBrowser#add () in
@@ -822,10 +829,19 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       activate_combo_query "" "locate";
       win#whelpBarComboVbox#add combo#coerce;
       let start_query () = 
-        let query = String.lowercase (List.nth queries combo#active) in
-        let input = win#queryInputText#text in
-        let statement = "whelp " ^ query ^ " " ^ input ^ "." in
-        (MatitaScript.current ())#advance ~statement ()
+        if !do_not_execute_whelp_query then
+          do_not_execute_whelp_query := false
+        else
+          begin
+          let query = 
+            try
+              String.lowercase (List.nth queries combo#active) 
+            with Not_found -> assert false
+          in
+          let input = win#queryInputText#text in
+          let statement = "whelp " ^ query ^ " (" ^ input ^ ")." in
+          (MatitaScript.current ())#advance ~statement ()
+          end
       in
       ignore(win#queryInputText#connect#activate ~callback:start_query);
       ignore(combo#connect#changed ~callback:start_query);

diff --git a/matita/matitaMisc.ml b/matita/matitaMisc.ml
index 266aec526920ad8d96bda49f7cca4cd0d29a2861..bb745f7030f968817f544fa4a49d1828eba4795e 100644 (file)
--- a/matita/matitaMisc.ml
+++ b/matita/matitaMisc.ml
@@ -30,7 +30,10 @@ open Printf
 (** Functions "imported" from Http_getter_misc *)
 
 let normalize_dir = Http_getter_misc.normalize_dir
-let strip_suffix = Http_getter_misc.strip_suffix
+let strip_suffix ~suffix s = 
+  try 
+    Http_getter_misc.strip_suffix ~suffix s
+  with Invalid_argument _ -> s
 
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 891d09a50b20495e9c5da8f3c70d6f0d70792f68..6c4dedd086f34c140656de930ce7ca1735b2152a 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -222,26 +222,24 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
   (* XXX use a real CIC -> string pretty printer *)
-  let pp_macro = TAPp.pp_macro ~term_pp:CicPp.ppterm in
+  let pp_macro = 
+    TAPp.pp_macro ~term_pp:(ApplyTransformation.txt_of_cic_term max_int [] []) 
+  in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
      let l =  Whelp.match_term ~dbd term in
-     let query_url =
-       MatitaMisc.strip_suffix ~suffix:"."
-         (HExtlib.trim_blanks unparsed_text)
-     in
-     let entry = `Whelp (query_url, l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   | TA.WInstance (loc, term) ->
      let l = Whelp.instance ~dbd term in
-     let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   | TA.WLocate (loc, s) -> 
      let l = Whelp.locate ~dbd s in
-     let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   | TA.WElim (loc, term) ->
@@ -251,13 +249,13 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
        | _ -> failwith "Not a MutInd"
      in
      let l = Whelp.elim ~dbd uri in
-     let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   | TA.WHint (loc, term) ->
      let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
      let l = List.map fst (MQ.experimental_hint ~dbd s) in
-     let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in
+     let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], parsed_text_length
   (* REAL macro *)
@@ -535,6 +533,7 @@ object (self)
       self#notify
     with 
     | Margin -> self#notify
+    | Not_found -> assert false
     | exc -> self#notify; raise exc
 
   method retract () =