X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=c29e15533ef1c6a71a10c06b04a46cec6f95481a;hb=9ff984b29ac963eef2f79521ce9dd7cbb9ae2c59;hp=e446b67f5503c9b00b5886ac379244643e43130a;hpb=c6ecfe8fff2265abfedbbe33a171c26b0d8c7c4e;p=helm.git diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index e446b67f5..c29e15533 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -402,14 +402,20 @@ let cic2grafite context menv t = let pres_term = TermContentPres.pp_ast content_term in let dummy_tbl = Hashtbl.create 1 in let markup = CicNotationPres.render dummy_tbl pres_term in - let s = "(" ^ BoxPp.render_to_string List.hd width markup ^ ")" in + let s = "(" ^ BoxPp.render_to_string + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + List.hd width markup ^ ")" in Pcre.substitute ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s in CicNotationPp.set_pp_term term_pp; let lazy_term_pp = fun x -> assert false in let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in - GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t + GrafiteAstPp.pp_statement + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~term_pp ~lazy_term_pp ~obj_pp t in let script = String.concat "" (List.map pp ast) in prerr_endline script; @@ -433,7 +439,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in TAPp.pp_macro ~term_pp:(fun x -> - ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x)) + ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x) + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex")) in match mac with (* WHELP's stuff *) @@ -470,7 +478,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length (* REAL macro *) - | TA.Hint loc -> + | TA.Hint (loc, rewrite) -> let user_goal' = match user_goal with Some n -> n @@ -478,35 +486,45 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status in let proof = GrafiteTypes.get_current_proof grafite_status in let proof_status = proof,user_goal' in - let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in - let selected = guistuff.urichooser l in - (match selected with - | [] -> [], "", parsed_text_length - | [uri] -> - let suri = UriManager.string_of_uri uri in - let ast loc = - TA.Executable (loc, (TA.Tactic (loc, - Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))), - TA.Dot loc))) in - let text = - comment parsed_text ^ "\n" ^ - pp_eager_statement_ast (ast HExtlib.dummy_floc) in - let text_len = MatitaGtkMisc.utf8_string_length text in - let loc = HExtlib.floc_of_loc (0,text_len) in - let statement = `Ast (GrafiteParser.LSome (ast loc),text) in - let res,_,_parsed_text_len = - eval_statement include_paths buffer guistuff lexicon_status - grafite_status user_goal script statement - in - (* we need to replace all the parsed_text *) - res,"",String.length parsed_text - | _ -> - HLog.error - "The result of the urichooser should be only 1 uri, not:\n"; - List.iter ( - fun u -> HLog.error (UriManager.string_of_uri u ^ "\n") - ) selected; - assert false) + if rewrite then + let l = MQ.equations_for_goal ~dbd proof_status in + let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in + let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; + [], "", parsed_text_length + else + let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in + let selected = guistuff.urichooser l in + (match selected with + | [] -> [], "", parsed_text_length + | [uri] -> + let suri = UriManager.string_of_uri uri in + let ast loc = + TA.Executable (loc, (TA.Tactic (loc, + Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))), + TA.Dot loc))) in + let text = + comment parsed_text ^ "\n" ^ + pp_eager_statement_ast (ast HExtlib.dummy_floc) + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + in + let text_len = MatitaGtkMisc.utf8_string_length text in + let loc = HExtlib.floc_of_loc (0,text_len) in + let statement = `Ast (GrafiteParser.LSome (ast loc),text) in + let res,_,_parsed_text_len = + eval_statement include_paths buffer guistuff lexicon_status + grafite_status user_goal script statement + in + (* we need to replace all the parsed_text *) + res,"",String.length parsed_text + | _ -> + HLog.error + "The result of the urichooser should be only 1 uri, not:\n"; + List.iter ( + fun u -> HLog.error (UriManager.string_of_uri u ^ "\n") + ) selected; + assert false) | TA.Check (_,term) -> let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in let context = @@ -548,8 +566,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status Auto.revision time size depth in let proof_script = - if true (* List.exists (fun (s,_) -> s = "paramodulation") params *) then - let proof_term = + if List.exists (fun (s,_) -> s = "paramodulation") params then + let proof_term, how_many_lambdas = Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc in @@ -564,9 +582,10 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[])) in ApplyTransformation.txt_of_cic_object - ~map_unicode_to_tex:false + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") ~skip_thm_and_qed:true - ~skip_initial_lambdas:true + ~skip_initial_lambdas:how_many_lambdas 80 GrafiteAst.Declarative "" obj else if true then @@ -574,7 +593,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status cic2grafite cc menv proof_term else (* alternative using FG stuff *) - let proof_term = + let proof_term, how_many_lambdas = Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc in @@ -588,9 +607,10 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" (strip_comments (ApplyTransformation.txt_of_cic_object - ~map_unicode_to_tex:false + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") ~skip_thm_and_qed:true - ~skip_initial_lambdas:true + ~skip_initial_lambdas:how_many_lambdas 80 (GrafiteAst.Procedural None) "" obj)) in let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in @@ -600,7 +620,12 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status raise exn (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) | TA.Inline (_,style,suri,prefix) -> - let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + let str = + ApplyTransformation.txt_of_inline_macro + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + style suri prefix + in [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff @@ -616,7 +641,7 @@ script ex loc | TA.Command (_,TA.Set (_,"baseuri",u)) -> if Http_getter_storage.is_read_only u then raise (ActionCancelled ("baseuri " ^ u ^ " is readonly")); - if not (Http_getter_storage.is_empty u) then + if not (Http_getter_storage.is_empty ~local:true u) then (match guistuff.ask_confirmation ~title:"Baseuri redefinition"