Added toggle for enabling/disabling the conversion from multibyte unicode

characters to TeX when converting CIC terms to textual formulae. The toggle is
under the Edit menu (rational: it's near the paste commands, maybe it should be
added to the GtkSourceView contextual menu too). The toggle governs the
matita.paste_unicode_as_tex boolean registry value. The txt_of_* rendering
functions have been changed to accept a new optional boolean parameter.

diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml
index b9bb9fbbd5badc06ef55a36ca418471731559db2..ca51c0ed3e46d8c14730301bd7640bfb598d6a7e 100644 (file)
--- 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 choose_action size markup =
+let render_to_strings ?(map_unicode_to_tex = true) choose_action size markup =
   let max_size = max_int in
   let rec aux_box =
     function
@@ -193,14 +193,17 @@ let render_to_strings choose_action size markup =
     | Pres.Mgliph (_, s) -> fixed_rendering s
     | Pres.Mo (_, s) ->
         let s =
-         if String.length s = 1 && Char.code s.[0] < 128 then
-          s
-         else
-          match Utf8Macro.tex_of_unicode s with
-             Some s -> s ^ " "
-           | None -> s
+          if map_unicode_to_tex then begin
+            if String.length s = 1 && Char.code s.[0] < 128 then
+              s
+            else
+              match Utf8Macro.tex_of_unicode s with
+              | Some s -> s ^ " "
+              | None -> s
+          end else
+            s
         in
-         fixed_rendering s
+        fixed_rendering s
     | Pres.Mspace _ -> fixed_rendering string_space
     | Pres.Mrow (attrs, children) ->
         let children' = List.map aux_mpres children in
@@ -237,6 +240,7 @@ let render_to_strings choose_action size markup =
   in
   snd (aux_mpres markup size)
 
-let render_to_string choose_action size markup =
-  String.concat "\n" (render_to_strings 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)
 

diff --git a/helm/software/components/content_pres/boxPp.mli b/helm/software/components/content_pres/boxPp.mli
index fe05e24d9e8af9da1bc5a22f14c82cb62d4e43ab..66ae8ec95ea7f15f048bc64abbadb26d9f7f76a2 100644 (file)
--- a/helm/software/components/content_pres/boxPp.mli
+++ b/helm/software/components/content_pres/boxPp.mli
@@ -23,15 +23,21 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** @return rows list of rows *)
+  (**
+   * @param map_unicode_to_tex if true converts multibye unicode sequences to
+   *  TeX-like macros (when possible). Default: true
+   * @return rows list of rows *)
 val render_to_strings: 
+  ?map_unicode_to_tex:bool ->
   (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> 
   int -> CicNotationPres.markup -> string list
 
   (** helper function
+   * @param map_unicode_to_tex as above
    * @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 ->
   (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> 
   int -> CicNotationPres.markup -> string
 

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 47e8dd23162b6d038d36334f3d6715f6bbbdd997..499c1705be978b97c7f9634ead475190e817e208 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -70,7 +70,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 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)
   =
@@ -81,10 +81,10 @@ let txt_of_cic_sequent size metasenv sequent =
    CicNotationPres.mpres_of_box
     (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
   in
-  BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size
-   pres_sequent
+  BoxPp.render_to_string ?map_unicode_to_tex
+    (function x::_ -> x | _ -> assert false) size pres_sequent
 
-let txt_of_cic_sequent_conclusion 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
@@ -92,11 +92,12 @@ let txt_of_cic_sequent_conclusion 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 (function x::_ -> x | _ -> assert false) size t
+  BoxPp.render_to_string ?map_unicode_to_tex
+    (function x::_ -> x | _ -> assert false) size t
 
-let txt_of_cic_term 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 size metasenv fake_sequent 
+  txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv fake_sequent 
 ;;
 
 ignore (
@@ -139,7 +140,7 @@ ignore (
 let remove_closed_substs s =
     Pcre.replace ~pat:"{...}" ~templ:"" s
 
-let term2pres 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
@@ -151,10 +152,10 @@ let term2pres 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 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 n style prefix obj =
+let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
   let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = 
      try Cic2acic.acic_object_of_cic_object obj
      with e -> 
@@ -166,7 +167,9 @@ let txt_of_cic_object n style prefix obj =
         let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
         let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
         remove_closed_substs ("\n\n" ^
-          BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
+          BoxPp.render_to_string ?map_unicode_to_tex
+            (function _::x::_ -> x | _ -> assert false) n
+            (CicNotationPres.mpres_of_box bobj)
        )
      | GrafiteAst.Procedural depth ->
         let term_pp = term2pres (n - 8) ids_to_inner_sorts in

diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli
index 8e0b19361779f3e52401fe329eac38bcb87d2129..2718d6401d37edafdf55dfdc5a057b1bfb3cd8c3 100644 (file)
--- a/helm/software/matita/applyTransformation.mli
+++ b/helm/software/matita/applyTransformation.mli
@@ -56,15 +56,20 @@ val mml_of_cic_object:
        (Cic.id, Cic2acic.anntypes) Hashtbl.t))  (* ids_to_inner_types *)
 
 val txt_of_cic_term: 
-  int -> Cic.metasenv -> Cic.context -> Cic.term -> string 
+  ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->
+    string 
 val txt_of_cic_sequent: 
-  int -> Cic.metasenv -> Cic.conjecture -> string
+  ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture ->
+    string
 val txt_of_cic_sequent_conclusion: 
-  int -> Cic.metasenv -> Cic.conjecture -> string
+  ?map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture ->
+    string
 
 (* columns, rendering style, name prefix, object *)
 val txt_of_cic_object: 
-   int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string
+  ?map_unicode_to_tex:bool -> int -> GrafiteAst.presentation_style -> string ->
+  Cic.obj ->
+    string
 
 (* presentation_style, uri or baseuri, name prefix *)
 val txt_of_inline_macro:

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 4b3378513d32d4ccc4b77d5e3483e73d6c37777e..6d11b4fa1b7c06f57b11879db7a8787dc1a8e703 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1081,7 +1081,7 @@
                              <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1013">
+                               <widget class="GtkImage" id="image1047">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-new</property>
                                  <property name="icon_size">1</property>
@@ -1102,7 +1102,7 @@
                              <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1014">
+                               <widget class="GtkImage" id="image1048">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-open</property>
                                  <property name="icon_size">1</property>
@@ -1123,7 +1123,7 @@
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1015">
+                               <widget class="GtkImage" id="image1049">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save</property>
                                  <property name="icon_size">1</property>
@@ -1144,7 +1144,7 @@
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1016">
+                               <widget class="GtkImage" id="image1050">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save-as</property>
                                  <property name="icon_size">1</property>
@@ -1165,7 +1165,7 @@
                              <accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1017">
+                               <widget class="GtkImage" id="image1051">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-execute</property>
                                  <property name="icon_size">1</property>
@@ -1192,7 +1192,7 @@
                              <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1018">
+                               <widget class="GtkImage" id="image1052">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-quit</property>
                                  <property name="icon_size">1</property>
@@ -1227,7 +1227,7 @@
                              <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1019">
+                               <widget class="GtkImage" id="image1053">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-undo</property>
                                  <property name="icon_size">1</property>
@@ -1249,7 +1249,7 @@
                              <accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1020">
+                               <widget class="GtkImage" id="image1054">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-redo</property>
                                  <property name="icon_size">1</property>
@@ -1276,7 +1276,7 @@
                              <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1021">
+                               <widget class="GtkImage" id="image1055">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-cut</property>
                                  <property name="icon_size">1</property>
@@ -1297,7 +1297,7 @@
                              <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1022">
+                               <widget class="GtkImage" id="image1056">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-copy</property>
                                  <property name="icon_size">1</property>
@@ -1318,7 +1318,7 @@
                              <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1023">
+                               <widget class="GtkImage" id="image1057">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-paste</property>
                                  <property name="icon_size">1</property>
@@ -1339,6 +1339,15 @@
                            </widget>
                          </child>
 
+                         <child>
+                           <widget class="GtkCheckMenuItem" id="unicodeAsTexMenuItem">
+                             <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>
+                           </widget>
+                         </child>
+
                          <child>
                            <widget class="GtkImageMenuItem" id="deleteMenuItem">
                              <property name="visible">True</property>
@@ -1346,7 +1355,7 @@
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1024">
+                               <widget class="GtkImage" id="image1058">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-delete</property>
                                  <property name="icon_size">1</property>
@@ -1387,7 +1396,7 @@
                              <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1025">
+                               <widget class="GtkImage" id="image1059">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-find-and-replace</property>
                                  <property name="icon_size">1</property>
@@ -1555,7 +1564,7 @@
                              <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1026">
+                               <widget class="GtkImage" id="image1060">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-in</property>
                                  <property name="icon_size">1</property>
@@ -1576,7 +1585,7 @@
                              <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1027">
+                               <widget class="GtkImage" id="image1061">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-out</property>
                                  <property name="icon_size">1</property>
@@ -1597,7 +1606,7 @@
                              <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1028">
+                               <widget class="GtkImage" id="image1062">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-100</property>
                                  <property name="icon_size">1</property>
@@ -1674,7 +1683,7 @@
                              <accelerator key="F1" modifiers="0" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1029">
+                               <widget class="GtkImage" id="image1063">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-help</property>
                                  <property name="icon_size">1</property>
@@ -1694,7 +1703,7 @@
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image1030">
+                               <widget class="GtkImage" id="image1064">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-about</property>
                                  <property name="icon_size">1</property>

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index f40efe867ea0f19068fd6dc7b31908212e5633fe..a9faa592e8de974b5ce3192a81eacf22f556ac0c 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -1012,11 +1012,10 @@ class gui () =
         not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
       then 
         main#tacticsBarMenuItem#set_active false;
-      MatitaGtkMisc.toggle_callback 
+      MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
         ~callback:(function 
           | true -> main#toplevel#fullscreen () 
-          | false -> main#toplevel#unfullscreen ())
-        ~check:main#fullscreenMenuItem;
+          | false -> main#toplevel#unfullscreen ());
       main#fullscreenMenuItem#set_active false;
       MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
         ~callback:(function
@@ -1027,6 +1026,13 @@ class gui () =
               CicNotation.set_active_notations []);
       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
         ~callback:(fun enabled -> Acic2content.hide_coercions := enabled);
+      MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
+        ~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;
+      main#unicodeAsTexMenuItem#set_active
+        (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index c32c00f203c12c4fa99dad0730cdd3b79335bae0..4252014bd83115bfae8ad9927dfd88cabcef0967 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -452,7 +452,9 @@ object (self)
     let markup = CicNotationPres.render ids_to_uris pped_ast in
     BoxPp.render_to_string text_width markup
     *)
-    ApplyTransformation.txt_of_cic_sequent_conclusion 
+    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
       text_width metasenv cic_sequent
 
   method private pattern_of term context unsh_sequent =