From 9d2f0cf4764f3fe9c85bcb8f6b06a426d99cfa44 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jul 2007 10:19:28 +0000
Subject: [PATCH] paste_unicode_as_tex is now false by default; moreover the
 flag is used everywhere (but in patterns, I do not know why)

---
 helm/software/matita/matita.glade    |  2 +-
 helm/software/matita/matitaGui.ml    |  2 +-
 helm/software/matita/matitaScript.ml | 10 +++++++---
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index e50642a61..72ba3db8c 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -910,7 +910,7 @@
                                 <property name="visible">True</property>
                                 <property name="label" translatable="yes">Paste Unicode as TeX</property>
                                 <property name="use_underline">True</property>
-                                <property name="active">True</property>
+                                <property name="active">False</property>
                               </widget>
                             </child>
                             <child>
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 94cb736b8..8ffa5fc91 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -1026,7 +1026,7 @@ class gui () =
         ~callback:(fun enabled ->
           Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
       if not (Helm_registry.has "matita.paste_unicode_as_tex") then
-        Helm_registry.set_bool "matita.paste_unicode_as_tex" true;
+        Helm_registry.set_bool "matita.paste_unicode_as_tex" false;
       main#unicodeAsTexMenuItem#set_active
         (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)
diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index d86299a0c..69e92518d 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -564,7 +564,8 @@ 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:how_many_lambdas
                 80 GrafiteAst.Declarative "" obj
@@ -588,7 +589,8 @@ 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:how_many_lambdas
                     80 (GrafiteAst.Procedural None) "" obj)) 
@@ -602,7 +604,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
   | TA.Inline (_,style,suri,prefix) ->
        let str = 
          ApplyTransformation.txt_of_inline_macro
-           ~map_unicode_to_tex:false style suri prefix 
+          ~map_unicode_to_tex:(Helm_registry.get_bool
+            "matita.paste_unicode_as_tex")
+          style suri prefix 
        in
        [], str, String.length parsed_text
                                 
-- 
2.39.2