From 863eeec8251791046ea6ea487286eb1434520725 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 12 Apr 2006 15:48:08 +0000 Subject: [PATCH] some fixes for whelp macros (concerning pprint...) --- helm/software/matita/applyTransformation.ml | 14 +++++++++ helm/software/matita/applyTransformation.mli | 5 +++ helm/software/matita/matitaGtkMisc.ml | 10 +++--- helm/software/matita/matitaMathView.ml | 32 +++++++++++++++----- helm/software/matita/matitaMisc.ml | 5 ++- helm/software/matita/matitaScript.ml | 19 ++++++------ 6 files changed, 62 insertions(+), 23 deletions(-) diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 83e5f3c18..fe8d9e569 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/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/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 8e023aea6..8e2d51b5b 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/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/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml index 553406635..a41dbffe3 100644 --- a/helm/software/matita/matitaGtkMisc.ml +++ b/helm/software/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/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 746ef8ffa..aa1b16a28 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/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/helm/software/matita/matitaMisc.ml b/helm/software/matita/matitaMisc.ml index 266aec526..bb745f703 100644 --- a/helm/software/matita/matitaMisc.ml +++ b/helm/software/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/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 891d09a50..6c4dedd08 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/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 () = -- 2.39.2