(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
+
(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
+
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
(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)
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
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
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
| 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
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);
(** 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
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) ->
| _ -> 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 *)
self#notify
with
| Margin -> self#notify
+ | Not_found -> assert false
| exc -> self#notify; raise exc
method retract () =
projects / helm.git / commitdiff