]> matita.cs.unibo.it Git - helm.git/commitdiff
map_unicode_to_tex is no longer optional and it always refers to the current
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jul 2007 12:07:44 +0000 (12:07 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jul 2007 12:07:44 +0000 (12:07 +0000)
user choice.

16 files changed:
helm/software/components/binaries/transcript/grafite.ml
helm/software/components/content_pres/boxPp.ml
helm/software/components/content_pres/boxPp.mli
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite/grafiteAstPp.mli
helm/software/components/grafite_parser/test_parser.ml
helm/software/components/tptp_grafite/tptp2grafite.ml
helm/software/matita/applyTransformation.ml
helm/software/matita/applyTransformation.mli
helm/software/matita/matita.ml
helm/software/matita/matitaGui.ml
helm/software/matita/matitaMathView.ml
helm/software/matita/matitaScript.ml
helm/software/matita/matitaWiki.ml
helm/software/matita/matitac.ml
helm/software/matita/matitacLib.ml

index 1b8c640f87b180be16a3263d05345ede09eb7967..93bd922ef3f0294631cbbfa35cff6f8385941559 100644 (file)
@@ -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 =
index 5719f2b69203912cb5a1983c48d16f849f43f075..0c18475489b076db0fc5aa1feeb262ec83e21ca9 100644 (file)
@@ -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)
 
index 66ae8ec95ea7f15f048bc64abbadb26d9f7f76a2..291c59a2ae1439f3cb22e43efa6f66b71b6a87c0 100644 (file)
@@ -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
 
index 4828d037957a72e291de454bd361fd75e9726e55..6dc488816f304193c834271b1273f51033f49e01 100644 (file)
@@ -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
index 35ade2b2399ddb6f19fb259f72b577637929fa9f..647d38bbe22a35cb93f1f60ac8f134876e7c4186 100644 (file)
@@ -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:
index 7e316879bc3415b56d5d74a056ad231ec48f877d..76c402c196c757327525aa96e10b552230f10711 100644 (file)
@@ -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_")
index a7f3a85238fcf527172074b8266caf6396e1291b..54a523cccb81ef237b19846172e08a49f6aea5fa 100644 (file)
@@ -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 = [
index 5d81d922496e28be36697bb59b77dd74af9f94f1..19a40960774ff0ad6a4c6bbc00d28e58bf692321 100644 (file)
@@ -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 -> 
index 9307f1e18ef2aef63c9efe87537c722393a59e42..7156d986706b90262b0480951a43b328a85ecb1c 100644 (file)
@@ -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
index 5873b22514e252da8579d6a890150ce9c8eb46ec..58d404888d7bde1e178185eaf21833651518689b 100644 (file)
@@ -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
index 8ffa5fc914e77f522f1b9849b1f19f1bfcda4268..95d0a76310ebea5d645935ee81ea0b1914791ad7 100644 (file)
@@ -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
index 53443128756e529af348db08471d9d49490eec09..5c0bc953440814feedad53cfc395253fe35b49fc 100644 (file)
@@ -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 =
index 69e92518d601bfd6aadf8ef49c05af6e1da5d0c5..fca45c02628132a700ef92bcf3fd913da19e40f1 100644 (file)
@@ -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
index bbe8d2ed7247f60132ffa0f97e4c7e298959efc9..3c5607bd7df9ff1bf458d61f5f0dac65a3aea604 100644 (file)
@@ -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))
           | _ -> ()
index fc1a95e1606aba56cb321cc95a6b6d3289a63cb1..31b304333fd34e3446fe27953666273b33b5d062 100644 (file)
@@ -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
 
 (**)
 
index 17e83c976baf2d4268b80a2a5b25bca4d3a5dced..8bb0dab4c2a1dd12af444535b0f10cf81e8a8376 100644 (file)
@@ -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
        | _ ->