user choice.
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 =
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
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)
* 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
* @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
| `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
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, [] -> ""
| 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
(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"
| 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
^ 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
*)
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)
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 ->
('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) ->
string
val pp_executable:
+ map_unicode_to_tex:bool ->
term_pp:('term -> string) ->
lazy_term_pp:('lazy_term -> string) ->
obj_pp:('obj -> string) ->
obj_pp:('obj -> string) ->
('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
GrafiteAst.statement ->
+ map_unicode_to_tex:bool ->
string
val pp_punctuation_tactical:
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_")
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 = [
(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)
=
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
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 (
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
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
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
?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
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 ->
(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 ->
(* 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
(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
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
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
"\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
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
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 =
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;
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 *)
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
(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))
| _ -> ()
(* 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
(**)
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} *)
| 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);
| 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
| _ ->
projects / helm.git / commitdiff