paste_unicode_as_tex is now false by default; moreover the flag is used

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index e446b67f5503c9b00b5886ac379244643e43130a..69e92518d601bfd6aadf8ef49c05af6e1da5d0c5 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -548,8 +548,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 +564,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 +575,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 +589,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 +602,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 +623,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"