From: Claudio Sacerdoti Coen Date: Thu, 19 Jul 2007 12:07:44 +0000 (+0000) Subject: map_unicode_to_tex is no longer optional and it always refers to the current X-Git-Tag: make_still_working~6152 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=397b5f9d848e63a9703a1f90faf9869092ec8893;p=helm.git map_unicode_to_tex is no longer optional and it always refers to the current user choice. --- diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index 1b8c640f8..93bd922ef 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -63,7 +63,7 @@ let out_command och cmd = let term_pp = NP.pp_term in let lazy_term_pp = NP.pp_term in let obj_pp = NP.pp_obj NP.pp_term in - let s = GP.pp_statement ~term_pp ~lazy_term_pp ~obj_pp cmd in + let s = GP.pp_statement ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp cmd in Printf.fprintf och "%s\n\n" s let command_of_obj obj = diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml index 5719f2b69..0c1847548 100644 --- a/helm/software/components/content_pres/boxPp.ml +++ b/helm/software/components/content_pres/boxPp.ml @@ -93,7 +93,7 @@ let fixed_rendering s = let s_len = String.length s in (fun _ -> s_len, [s]) -let render_to_strings ?(map_unicode_to_tex = true) choose_action size markup = +let render_to_strings ~map_unicode_to_tex choose_action size markup = let max_size = max_int in let rec aux_box = function @@ -240,7 +240,7 @@ let render_to_strings ?(map_unicode_to_tex = true) choose_action size markup = in snd (aux_mpres markup size) -let render_to_string ?map_unicode_to_tex choose_action size markup = +let render_to_string ~map_unicode_to_tex choose_action size markup = String.concat "\n" - (render_to_strings ?map_unicode_to_tex choose_action size markup) + (render_to_strings ~map_unicode_to_tex choose_action size markup) diff --git a/helm/software/components/content_pres/boxPp.mli b/helm/software/components/content_pres/boxPp.mli index 66ae8ec95..291c59a2a 100644 --- a/helm/software/components/content_pres/boxPp.mli +++ b/helm/software/components/content_pres/boxPp.mli @@ -28,7 +28,7 @@ * TeX-like macros (when possible). Default: true * @return rows list of rows *) val render_to_strings: - ?map_unicode_to_tex:bool -> + map_unicode_to_tex:bool -> (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> int -> CicNotationPres.markup -> string list @@ -37,7 +37,7 @@ val render_to_strings: * @return s, concatenation of the return value of render_to_strings above * with newlines as separators *) val render_to_string: - ?map_unicode_to_tex:bool -> + map_unicode_to_tex:bool -> (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> int -> CicNotationPres.markup -> string diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 4828d0379..6dc488816 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -44,7 +44,7 @@ let pp_reduction_kind ~term_pp = function | `Unfold None -> "unfold" | `Whd -> "whd" -let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) = +let pp_tactic_pattern ~map_unicode_to_tex ~term_pp ~lazy_term_pp (what, hyp, goal) = if what = None && hyp = [] && goal = None then "" else let what_text = match what with @@ -56,8 +56,11 @@ let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) = let goal_text = match goal with | None -> "" - | Some t -> Printf.sprintf "\\vdash (%s)" (term_pp t) in - Printf.sprintf "%sin %s%s" what_text hyp_text goal_text + | Some t -> + let vdash = if map_unicode_to_tex then "\\vdash" else "⊢" in + Printf.sprintf "%s (%s)" vdash (term_pp t) + in + Printf.sprintf "%sin %s%s" what_text hyp_text goal_text let pp_intros_specs s = function | None, [] -> "" @@ -71,24 +74,27 @@ let opt_string_pp = function | None -> "" | Some what -> what ^ " " -let rec pp_tactic ~term_pp ~lazy_term_pp = +let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = + let pp_tactic = pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp in + let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in let pp_reduction_kind = pp_reduction_kind ~term_pp in - let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in + let pp_tactic_pattern = + pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in function (* Higher order tactics *) | Do (_, count, tac) -> - Printf.sprintf "do %d %s" count (pp_tactic ~term_pp ~lazy_term_pp tac) - | Repeat (_, tac) -> "repeat " ^ pp_tactic ~term_pp ~lazy_term_pp tac - | Seq (_, tacs) -> pp_tactics ~term_pp ~lazy_term_pp ~sep:"; " tacs + Printf.sprintf "do %d %s" count (pp_tactic tac) + | Repeat (_, tac) -> "repeat " ^ pp_tactic tac + | Seq (_, tacs) -> pp_tactics ~sep:"; " tacs | Then (_, tac, tacs) -> - Printf.sprintf "%s; [%s]" (pp_tactic ~term_pp ~lazy_term_pp tac) - (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs) + Printf.sprintf "%s; [%s]" (pp_tactic tac) + (pp_tactics ~sep:" | " tacs) | First (_, tacs) -> - Printf.sprintf "tries [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs) - | Try (_, tac) -> "try " ^ pp_tactic ~term_pp ~lazy_term_pp tac + Printf.sprintf "tries [%s]" (pp_tactics ~sep:" | " tacs) + | Try (_, tac) -> "try " ^ pp_tactic tac | Solve (_, tac) -> - Printf.sprintf "solve [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tac) - | Progress (_, tac) -> "progress " ^ pp_tactic ~term_pp ~lazy_term_pp tac + Printf.sprintf "solve [%s]" (pp_tactics ~sep:" | " tac) + | Progress (_, tac) -> "progress " ^ pp_tactic tac (* First order tactics *) | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term @@ -194,8 +200,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^ ")") args) -and pp_tactics ~term_pp ~lazy_term_pp ~sep tacs = - String.concat sep (List.map (pp_tactic ~lazy_term_pp ~term_pp) tacs) +and pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~sep tacs = + String.concat sep + (List.map (pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp) tacs) let pp_search_kind = function | `Locate -> "locate" @@ -297,11 +304,11 @@ let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp = | Unfocus _ -> "unfocus" | Skip _ -> "skip" -let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = +let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function | Macro (_, macro) -> pp_macro ~term_pp macro ^ "." | Tactic (_, Some tac, punct) -> - pp_tactic ~lazy_term_pp ~term_pp tac + pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp tac ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct | Tactic (_, None, punct) -> pp_punctuation_tactical ~lazy_term_pp ~term_pp punct @@ -310,12 +317,12 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." -let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = +let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function | Note (_,"") -> Printf.sprintf "\n" | Note (_,str) -> Printf.sprintf "\n(* %s *)" str | Code (_,code) -> - Printf.sprintf "\n(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code) + Printf.sprintf "\n(** %s. **)" (pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp code) let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = function diff --git a/helm/software/components/grafite/grafiteAstPp.mli b/helm/software/components/grafite/grafiteAstPp.mli index 35ade2b23..647d38bbe 100644 --- a/helm/software/components/grafite/grafiteAstPp.mli +++ b/helm/software/components/grafite/grafiteAstPp.mli @@ -24,6 +24,7 @@ *) val pp_tactic: + map_unicode_to_tex:bool -> term_pp:('term -> string) -> lazy_term_pp:('lazy_term -> string) -> ('term, 'lazy_term, 'term GrafiteAst.reduction, string) @@ -31,6 +32,7 @@ val pp_tactic: string val pp_tactic_pattern: + map_unicode_to_tex:bool -> term_pp:('term -> string) -> lazy_term_pp:('lazy_term -> string) -> ('term, 'lazy_term, string) GrafiteAst.pattern -> @@ -47,6 +49,7 @@ val pp_command: ('term,'obj) GrafiteAst.command -> string val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string val pp_comment: + map_unicode_to_tex:bool -> term_pp:('term -> string) -> lazy_term_pp:('lazy_term -> string) -> obj_pp:('obj -> string) -> @@ -55,6 +58,7 @@ val pp_comment: string val pp_executable: + map_unicode_to_tex:bool -> term_pp:('term -> string) -> lazy_term_pp:('lazy_term -> string) -> obj_pp:('obj -> string) -> @@ -68,6 +72,7 @@ val pp_statement: obj_pp:('obj -> string) -> ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string) GrafiteAst.statement -> + map_unicode_to_tex:bool -> string val pp_punctuation_tactical: diff --git a/helm/software/components/grafite_parser/test_parser.ml b/helm/software/components/grafite_parser/test_parser.ml index 7e316879b..76c402c19 100644 --- a/helm/software/components/grafite_parser/test_parser.ml +++ b/helm/software/components/grafite_parser/test_parser.ml @@ -101,6 +101,8 @@ let process_stream istream = prerr_endline ("Unsupported statement: " ^ GrafiteAstPp.pp_statement + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:(fun _ -> "_lazy_term_here_") ~obj_pp:(fun _ -> "_obj_here_") diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index a7f3a8523..54a523ccc 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -339,14 +339,15 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam 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 List.hd width markup ~map_unicode_to_tex:false 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:false ~term_pp ~lazy_term_pp ~obj_pp t in let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in let extra_statements_start = [ diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 5d81d9224..19a409607 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -72,7 +72,7 @@ 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 ?map_unicode_to_tex size metasenv sequent = +let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent = let unsh_sequent,(asequent,ids_to_terms, ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses) = @@ -83,10 +83,10 @@ let txt_of_cic_sequent ?map_unicode_to_tex size metasenv sequent = CicNotationPres.mpres_of_box (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in - BoxPp.render_to_string ?map_unicode_to_tex + BoxPp.render_to_string ~map_unicode_to_tex (function x::_ -> x | _ -> assert false) size pres_sequent -let txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv sequent = +let txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv sequent = let _,(asequent,_,_,ids_to_inner_sorts,_) = Cic2acic.asequent_of_sequent metasenv sequent in @@ -94,12 +94,12 @@ let txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv sequent = 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 ?map_unicode_to_tex + BoxPp.render_to_string ~map_unicode_to_tex (function x::_ -> x | _ -> assert false) size t -let txt_of_cic_term ?map_unicode_to_tex size metasenv context t = +let txt_of_cic_term ~map_unicode_to_tex size metasenv context t = let fake_sequent = (-1,context,t) in - txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv fake_sequent + txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv fake_sequent ;; ignore ( @@ -109,7 +109,10 @@ ignore ( let context' = CicMetaSubst.apply_subst_context subst context in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in let term' = CicMetaSubst.apply_subst subst term in - let res = txt_of_cic_term 30 metasenv context' term' in + let res = + txt_of_cic_term + ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") + 30 metasenv context' term' in if String.contains res '\n' then "\n" ^ res ^ "\n" else @@ -143,7 +146,7 @@ ignore ( let remove_closed_substs s = Pcre.replace ~pat:"{...}" ~templ:"" s -let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm = +let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = let ast, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in @@ -155,11 +158,11 @@ let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm = in let render = function _::x::_ -> x | _ -> assert false in let mpres = CicNotationPres.mpres_of_box bobj in - let s = BoxPp.render_to_string ?map_unicode_to_tex render n mpres in + let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in remove_closed_substs s let txt_of_cic_object - ?map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj + ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj = let get_aobj obj = try @@ -183,24 +186,25 @@ let txt_of_cic_object ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj in remove_closed_substs ("\n\n" ^ - BoxPp.render_to_string ?map_unicode_to_tex + BoxPp.render_to_string ~map_unicode_to_tex (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) ) | G.Procedural depth -> let obj = ProceduralOptimizer.optimize_obj obj in let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in - let term_pp = term2pres (n - 8) ids_to_inner_sorts in + let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in let lazy_term_pp = term_pp in let obj_pp = CicNotationPp.pp_obj term_pp in - let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in + let aux = GrafiteAstPp.pp_statement + ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in let script = Acic2Procedural.acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed prefix aobj in String.concat "" (List.map aux script) ^ "\n\n" -let txt_of_inline_macro ?map_unicode_to_tex style suri prefix = +let txt_of_inline_macro ~map_unicode_to_tex style suri prefix = let print_exc = function | ProofEngineHelpers.Bad_pattern s as e -> Printexc.to_string e ^ " " ^ Lazy.force s @@ -211,7 +215,7 @@ let txt_of_inline_macro ?map_unicode_to_tex style suri prefix = let map uri = try txt_of_cic_object - ?map_unicode_to_tex 78 style prefix + ~map_unicode_to_tex 78 style prefix (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) with | e -> diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 9307f1e18..7156d9867 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -56,18 +56,18 @@ val mml_of_cic_object: (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *) val txt_of_cic_term: - ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term -> + map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term -> string val txt_of_cic_sequent: - ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> + map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> string val txt_of_cic_sequent_conclusion: - ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> + map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> string (* columns, rendering style, name prefix, object *) val txt_of_cic_object: - ?map_unicode_to_tex:bool -> + map_unicode_to_tex:bool -> ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:int -> int -> GrafiteAst.presentation_style -> string -> @@ -76,5 +76,5 @@ val txt_of_cic_object: (* presentation_style, uri or baseuri, name prefix *) val txt_of_inline_macro: - ?map_unicode_to_tex:bool -> + map_unicode_to_tex:bool -> GrafiteAst.presentation_style -> string -> string -> string diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 5873b2251..58d404888 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -174,6 +174,8 @@ let _ = (fun _ -> prerr_endline (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative "" + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") (match (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status with diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 8ffa5fc91..95d0a7631 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -968,7 +968,10 @@ class gui () = if (MatitaScript.current ())#onGoingProof () then (MatitaScript.current ())#advance ~statement:("\n" - ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term + ^ GrafiteAstPp.pp_tactic + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:CicNotationPp.pp_term ast) () in @@ -978,6 +981,8 @@ class gui () = buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) ("\n" ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") ~lazy_term_pp:CicNotationPp.pp_term ast) in let tbar = main in diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 534431287..5c0bc9534 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -303,6 +303,8 @@ object (self) "\n" ^ GrafiteAstPp.pp_executable ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") (GrafiteAst.Tactic (loc, Some (GrafiteAst.Reduce (loc, kind, pat)), GrafiteAst.Semicolon loc)) in @@ -434,6 +436,8 @@ object (self) let tactic_text_pattern = self#tactic_text_pattern_of_node node in GrafiteAstPp.pp_tactic_pattern ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false) + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") tactic_text_pattern | `Term -> self#tactic_text_of_node node else string_of_dom_node node @@ -453,8 +457,8 @@ object (self) BoxPp.render_to_string text_width markup *) let map_unicode_to_tex = - Helm_registry.get_opt Helm_registry.bool "matita.paste_unicode_as_tex" in - ApplyTransformation.txt_of_cic_sequent_conclusion ?map_unicode_to_tex + Helm_registry.get_bool "matita.paste_unicode_as_tex" in + ApplyTransformation.txt_of_cic_sequent_conclusion ~map_unicode_to_tex text_width metasenv cic_sequent method private pattern_of term context unsh_sequent = diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 69e92518d..fca45c026 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/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 *) @@ -490,7 +498,10 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status TA.Dot loc))) in let text = comment parsed_text ^ "\n" ^ - pp_eager_statement_ast (ast HExtlib.dummy_floc) in + 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 diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index bbe8d2ed7..3c5607bd7 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -167,6 +167,8 @@ let rec interactive_loop () = (List.map (fun i -> ApplyTransformation.txt_of_cic_sequent 80 metasenv + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") (List.find (fun (j,_,_) -> j=i) metasenv) ) open_goals)) | _ -> () diff --git a/helm/software/matita/matitac.ml b/helm/software/matita/matitac.ml index fc1a95e16..31b304333 100644 --- a/helm/software/matita/matitac.ml +++ b/helm/software/matita/matitac.ml @@ -52,9 +52,11 @@ let out_preamble och (path, lines) = (* from matitacLib *) -let pp_ast_statement = +let pp_ast_statement st = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st (**) diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 17e83c976..8bb0dab4c 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -35,9 +35,12 @@ let out = ref ignore let set_callback f = out := f -let pp_ast_statement = - GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) +let pp_ast_statement st = + GrafiteAstPp.pp_statement + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st (** {2 Initialization} *) @@ -142,9 +145,13 @@ let rec interactive_loop () = | GrafiteEngine.Macro (floc, f) -> begin match f (get_macro_context !grafite_status) with | _, GrafiteAst.Inline (_, style, suri, prefix) -> - let str = ApplyTransformation.txt_of_inline_macro style suri prefix in - !out str; - interactive_loop () + let str = + ApplyTransformation.txt_of_inline_macro style suri prefix + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + in + !out str; + interactive_loop () | _ -> let x, y = HExtlib.loc_of_floc floc in HLog.error (sprintf "A macro has been found in a script at %d-%d" x y); @@ -255,7 +262,10 @@ let rec compiler_loop fname big_bang mode buf = | GrafiteEngine.Macro (floc, f) -> begin match f (get_macro_context !grafite_status) with | _, GrafiteAst.Inline (_, style, suri, prefix) -> - let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + let str = + ApplyTransformation.txt_of_inline_macro style suri prefix + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") in !out str; compiler_loop fname big_bang mode buf | _ ->